Xmas Experiment: Isabelle Mini Clone in Prolog

[Jan Burse]

Dear All,

Just as a little xmas experiment an isabelle clone. There
is no guarantee that I managed to get everything right.
But I have followed the idea of a degenerate pure type system.

So instead of having a pure type system where we have
lambda expressions lx:A.B and product types px:A.B, there
is only abstraction x:A\B. This leads to some modified
and omitted rules. Where the original pure type system
has the following two rules among others:


G, x:A |- t:B G |- (px:A.B):s
----------------------------------- (abs)
G |- (lx:A.t) : (px:A.B)

G, x:A |- B:s2 G |- A:s1
----------------------------- (prod)
G |- (px:A.B):s3

The degenerate type system has the following single
rule among others, I guess this also implies that
x:A\B is non empty:


G, x:A |- t:B
----------------------- (abs')
G |- (x:A\t) : (x:A\B)


-- Missing -- (prod')

Implication A->B is simply x:A\B where x does not
occur in B. One problem with the degenerate type system
is that we cannot type implication successfully. Assume
with have a constant exF that should represent the
ex falso quodlibet rule. We can define the type of
such a constant as:

:- axiom exF::a:prop\(bot -> a).

If we want to instantiate the rule with a formula
we can use application. So for example instantiating
p for a can be done as follows, whereby we must first
state that p is a property.

:- axiom p::prop.

?- type p.
prop

?- type exF(p).
bot->p

So good so far. But what if we want to instantiate
p->q for a. Can this be also done? Here the lack of
a prod' rule is visible. The instantiation doesn't
work anymore. We get the following:

:- axiom q::prop.

?- type q.
prop

?- type p->q.
p->prop

?- type exF((p->q)).
No

Now a little trick helps here. We will introduce a
new constant => and see to it that it reflects ->
and that it is typable correctly. So we first define
this constant as follows:

:- op(1050, xfy, =>).

:- axiom (=>)::prop -> prop -> prop.

:- axiom q:prop.

?- type p=>q.
prop

?- type exF((p=>q)).
bot->p=>q

How we reflect => logically depends on the calculus
we want to implement. The -> can be used to realize
the rules of the calculus and to logically produce
=>. For example if we want to realize natural deduction
we can use the following two rules:

G |- A G |- A=>B
-------------------- (ifE)
G |- B

G, A |- B
----------- (ifI)
G |- A => B

This is done by stating:

:- axiom ifI::a:prop\b:prop\((a -> b) -> (a => b)).

:- axiom ifE::a:prop\b:prop\(a -> (a => b) -> b).

And we can for example do the following exercise, and
prove a=>(a=>b)=>b. The proof object is shown after
the by keyword in the theorem directive:

:- axiom a::prop.

:- axiom b::prop.

:- theorem a=>(a=>b)=>b by ifI(a,((a=>b)=>b),
x:a\ifI((a=>b),b,y:(a=>b)\ifE(a,b,x,y))).
Yes

But we can also realize a sequent calculus, by
using the following two rules:

G |- A G, B |- C
-------------------- (ifL)
G, A=>B |- C

G, A |- B
----------- (ifR)
G |- A => B

This is done by stating:

:- axiom ifR::a:prop\b:prop\((a -> b) -> (a => b)).

:- axiom ifL::a:prop\b:prop\c:prop\(a -> (b -> c) ->
(a => b) -> c).

Lets repeat the previous exercise, and this time
prove a=>(a=>b)=>b in sequent calculus. I hope I
get it right.

:- axiom a::prop.

:- axiom b::prop.

:- theorem a=>(a=>b)=>b by ifR(a,((a=>b)=>b),
x:a\ifR((a=>b),b,y:(a=>b)\ifL(a,b,b,x,z:b\z,y))).
Yes

Home Work: Extend the logic by quantifiers, extend
the type checker by eta and beta conversion, extend
the type checker by higher order unification, extend
the logic by induction, extend the type checker by
holes, extend the type check by tactics, extend the
type checker by calling automatic provers, etc.. etc..

Alternate Home Work: Try something else than eta
and beta conversion, try something else than higher
order unification, try something else than the usual
tactics etc.. etc.. He He

Bye

Source Code: Debruijn Indexes
https://gist.github.com/jburse/d7bcf52782b8887bf123#file-debruijn-p

Source Code: Natural Deduction
https://gist.github.com/jburse/d7bcf52782b8887bf123#file-natural-p

Source Code: Sequent Calculus
https://gist.github.com/jburse/d7bcf52782b8887bf123#file-sequent-p

[Jan Burse]

Dear All,

The universal quantifier is a little bit more tricky. It
is not enough to have a type check. We also need beta
conversion, i.e.:

(x:A\B)t --> B[x/t]

Beta conversion is already implemented in the type checker
when the type of an application is checked. But what we
need is an unbiqueous beta conversion for types, namely
what is usually found as the following rule:

G |- t : A A =_beta B
--------------------------
G |- t : B

We took the following road. We assumed that we can find
a normalization function nf, with the following property
if nf terminates for A and B, then we have

nf(A) = nf(B) ==> A =_beta B

This normalization function nf is implemented as a predicate
norm/3, and is also used during definitions and during type
checking.

The result is that universal quantifiers, both in natural
deduction style and sequent calculus style seem to work.
Their definitions is analogouse to the definition of implication
in both styles. For natural deduction we have:

:- axiom ifI::a:prop\b:prop\((a -> b) -> (a => b)).
:- axiom ifE::a:prop\b:prop\(a -> (a => b) -> b).

:- axiom allI::a:sort\b:(a->prop)\(x:a\b(x) -> #(a,b)).
:- axiom allE::a:sort\b:(a->prop)\(x:a\(#(a,b) -> b(x))).

And for sequent calculus we have:

:- axiom ifR::a:prop\b:prop\((a -> b) -> (a => b)).
:- axiom ifL::a:prop\b:prop\c:prop\(a -> (b -> c) -> (a => b) -> c).

:- axiom allR::a:sort\b:(a->prop)\(x:a\b(x) -> #(a,b)).
:- axiom allL::a:sort\b:(a->prop)\c:prop\(x:a\((b(x) -> c) ->
(#(a,b) -> c))).

The verifier has two new commands. With the "fun" command a
constant can be defined for expansion in normalization. And
with the "value" command a type can be normalized.

Source Code: Debruijn Indexes 2
https://gist.github.com/jburse/55dac6c0949ac2545f8e#file-debruijn2-p

Source Code: Natural Deduction 2
https://gist.github.com/jburse/55dac6c0949ac2545f8e#file-natural2-p

Source Code: Sequent Calculus 2
https://gist.github.com/jburse/55dac6c0949ac2545f8e#file-sequent2-p

Bye

Jan Burse schrieb:

[Jan Burse]

Dear All,

We can also reflect type constructors and not
only formulas. The observation for formulas was:

> So good so far. But what if we want to instantiate
> p->q for a. Can this be also done? Here the lack of
> a prod' rule is visible. The instantiation doesn't
> work anymore. We get the following:
>
> :- axiom q::prop.
>
> ?- type q.
> prop
>
> ?- type p->q.
> p->prop
>
> ?- type exF((p->q)).
> No

The work around was to define a new connective for
implication and a couple of rules that allow reflecting
-> into the new connective. These rules were taking
prop arguments.

Of course we can also reflect type constructors by
a couple of rules. We just need to do the same as for
connectives, but the rules will not take prop arguments
but sort arguments.

We avoid overloading, so we use from now on (=>) for
the function space type constructor and (==>) for the
implication connective. The definitions are:

Type Constructor:

:- op(1050, xfy, =>).

:- axiom (=>)::sort -> sort -> sort.

Formula:
:- op(1050, xfy, ==>).
:- axiom (==>)::prop -> prop -> prop.

When we do the above, we face the following problem.
Although we arrive at the desired result that we can now
form function spaces, and that these function spaces
are considered sorts as well:

:- axiom nat::sort.

?- type nat=>nat.
sort

We cannot anymore compose functions. The application
operator will fail for the new type constructur. Namely
we have:

:- axiom f::nat=>nat.
:- axiom n::nat.

?- type f(n).
No

The work around is here to also reflect the formation rules
for lambda abstraction and application. The native formation
rules are those of the already introduced degenerated
dependent type system. We display here the variant of
(abs') and (app) where x does not occur in B, hence the
use of (->) instead of (:/) in some places:

G, x:A |- t:B

------------------- (abs')
G |- (x:A\t):(A->B)

G |- t:A D |- s:(A->B)
---------------------------- (app)
G, D |- app(s,t):B

The reflected formation rules use two new proof object
constructors funI (function introduction) and funE
(function elimination). These rules produce and consume
the type constructor (=>) instead of (->). They look
as follows:

G, x:A |- t:B

----------------------- (funI)
G |- funI(x:A\t):(A=>B)

G |- t:A D |- s:(A=>B)
--------------------------- (funE)
G, D |- funE(t,s):B

Since => is without binder we dont reflect the full
dependent type system, only the simple type system.
A reflection with a binder would be also possible,
for example by an operator:

prod::a:sort\b:(a->sort)\sort

We would need to express A=>B as prod(A,x:A\B).
But this would complicate matters, and we did not
yet fully explore this reflection. So the realization
of the funI and funE rules and thus some simple
type formation rules in dependent types reads
as follows:

:- axiom funI::a:sort\b:sort\((a -> b) -> (a => b)).
:- axiom funE::a:sort\b:sort\(a -> (a => b) -> b).

With the above rules we have only reflected the formation,
but not yet some logical content. We can also reflect some
logical content of the reflection.

In natural deduction style we relate funI and funE to
native application by the following two rules:

G |- y(x)
-------------------- (lamI)
G |- funE(x,funI(y))

G |- funE(x,funI(y))
-------------------- (lamE)
G |- y(x)

In dependent types this reads as follows:

:- axiom lamI::a:sort\x:a\y:(a->prop)\(y(x) ->
funE(a,prop,x,funI(a,prop,y))).
:- axiom lamE::a:sort\x:a\y:(a->prop)\(funE(a,prop,x,funI(a,prop,y)) ->
y(x)).

In sequent calculus style we relate funI and funE to
native application by the following two rules:


G |- y(x)
-------------------- (lamR)
G |- funE(x,funI(y))

G, y(x) |- b
----------------------- (lamL)
G, funE(x,funI(y)) |- b

In dependent types this reads as follows:

:- axiom lamR::a:sort\x:a\y:(a->prop)\(y(x) ->
funE(a,prop,x,funI(a,prop,y))).
:- axiom lamL::a:sort\x:a\y:(a->prop)\b:prop\((y(x) -> b) ->
(funE(a,prop,x,funI(a,prop,y)) -> b)).

So what can we do with this big apparatus? Well we can
now reuse our quantifier rules and quantify over function
spaces. The quantifier rules assume variables where the
type is some sort. Thanks to the new type constructor (=>)
function spaces will also be sorts, and hence we can
easily quantify over them.

I did an example proof, both in natural style deduction(*) and in
sequent calculus(**). Namely I was proving the *comprehension axiom*
of set theory for the sort nat. The proven formula basically
reads as follows:

exists t forall y (funE(y,t) <=> z(y)) t not in z.

Or in dependent types notation with our operators as follows.
The schematic variable z and its side condition is reflected
by an abstraction over z:

z:(nat->prop)\(nat=>prop)^(t:(nat=>prop)\nat#
(y:nat\(funE(nat,prop,y,t)<=>z(y))))

Home Work: Prove more set theory related stuff, for
example Knaster-Tarski, etc..

(*)
https://gist.github.com/jburse/c2ea5cac7013b900710b#file-natural3-p

(**)
https://gist.github.com/jburse/c2ea5cac7013b900710b#file-sequent3-p

[Jan Burse]

Dear All,

Jan Burse schrieb:

> Home Work: Prove more set theory related stuff, for
> example Knaster-Tarski, etc..

We are not yet at some interesting proofs. Spent the last
weeks to ease the command language of the proof verifier.
Main ideas so far:

Holes: The original code of the so called Mini Isabelle Clone
allows type checking and normalization. We added type
inference via a constraint solver.

The constraint solver is just a Constraint Logic Programming
(CLP)-fication of the original predicates shift/4, subst/4,
typeof/3 and valueof/4. The constraint solver uses some
lemmas already found in this paper:

Residual Theory in λ -calculus
A Formal Development, Gerard Huet, 1998
http://pauillac.inria.fr/~huet/PUBLIC/residuals.pdf

Implicits: We call the new prototype Mini Agda Clone, since
besides holes we also investigated implicits. Implicit
parameters can be denoted by the []. And they are repeated
by name in the patterns.

Let's see what holes and implicits do us help here to arrive
at a mathematical like notation. Lets see how we would define
the subset relation. The full dependent type notation with
function and pattern notation reads as follows:

:- fun ⊆(u:sort)::set(u) -> set(u) -> prop by
⊆(u:sort,a:set(u),b:set(u)) =
(u#(x:u\(funE(u,prop,x,a) ==> funE(u,prop,x,b)))).

With holes we can already drop a lot of type annotations, since
these annotations are inferred. The same thing can be defined
with holes as follows:

:- fun ⊆(u)::set(u) -> set(u) -> prop by
⊆(u,a,b) = (_#(x\(funE(_,_,x,a) ==> funE(_,_,x,b)))).

The ultimate ease is reached when also implicits are present.
We can use implicits for quantifiers and membership, and the
definition itself, and arrive at the following:

:- fun ⊆([u])::set(u) -> set(u) -> prop by
(a ⊆ b) = (∀ x\(x∈a ==> x∈b)).

Unfortunately the constraint solver isn't coded in SICStus
Prolog or some such. We use the Jekejeke Minlog Attribute
Variables and Forward Chaining. Anybody knowing implementations
of such type inference in other CLP frameworks?

*Source Code Raw*
https://gist.github.com/jburse/c2ea5cac7013b900710b

*Source Code Holes (Jekejeke Minlog)*
https://gist.github.com/jburse/1341ffe0d1cc506e49f7

*Source Code Holes & Implicits (Jekejeke Minlog)*
https://gist.github.com/jburse/0ccd12698bfa24ce5c36

[Jan Burse]

Dear All,

This was the home work. And the home work is hard.

Jan Burse schrieb:

> Jan Burse schrieb:
> > Home Work: Prove more set theory related stuff, for
> > example Knaster-Tarski, etc..
>
> We are not yet at some interesting proofs. Spent the last
> weeks to ease the command language of the proof verifier.
> Main ideas so far:
>
> Holes: The original code of the so called Mini Isabelle Clone
>

> Implicits: We call the new prototype Mini Agda Clone, since

We pushed our mini isabelle clone so that we have
now a tactic engine in place. This tactic engine is
based on Prolog Definite Clause Grammars (DCG) to
pass around the proof state and on the term_variables/2
built-in to recalculate the proof state.

The use of DCG and term_variables/2 works quite fine.
The proof state is simply the holes in the proof
object which have not yet been specified. And
since in our prototype holes are simply Prolog
variables the built-in term_variables/2 can
recalculate the proof state. And DCG will pass
around this list of Prolog variables.

The primitives for the tactic engine are directly
written in Prolog. The most basic primitives are:

/**
* rule(N):
* Extendes the first open hole in the current incomplete
* proof by the given nominal term.
*/
rule(X, [X|L], R) :-
term_variables([X|L], R).
/**
* prefer(I):
* Moves the I-th open hole in the current imcomplete proof
* to the front.
*/
prefer(N, L, [X|R]) :-
nth1(N, L, X, R).

When these primitives are used inside a DCG they can be
used to build Prolog terms. Here is an example how the
Prolog term n1(n2(l1,l2),l3) can be built in two
different ways:

?- phrase((rule(n1(_,_)), rule(n2(_,_)), rule(l1), rule(l2), rule(l3)),
[X], L).
X = n1(n2(l1,l2),l3),
L = []

?- phrase((rule(n1(_,_)), prefer(2), rule(l3), rule(n2(_,_)), rule(l1),
rule(l2)), [X], L).
X = n1(n2(l1,l2),l3),
L = []

In the Mini Isabelle Clone the DCG and term_variables/2
are used to build proof objects. Here is an example of
a proof of a==>(a==>b)==>b in Gentzen LK:

?- theorem ex(a,b) :: a==>(a==>b)==>b by rule(ifR((_->_))),
rule(ifR((_->_))), rule(ifL(_,(_->_),x3)), rule(x2), rule(x4).
Yes

But there is not much gain by rule//1 and prefer//1. We
only serialize the building of the proof object. Of course
the Mini Isabelle Clone can give feedback in each step,
so that dead ends are early dedected, but to make a proof
is still tedious.

So we introduce an new primitive command for building
proof objects. Namely listing the premisses of the
currently unresolved sequent:

/**
* pick(V):
* Enumerates the variables identifiying the premisses in the
* first open hold in the current incomplete proof.
*/
pick(Y, [X|L], [X|L]) :-
sys_freeze_var(X, K),
sys_convert(K, A, _),
sys_melt_var(A, H),
member(Y, H).

So if the first open hole is linked to the following
sequent in the constraint solver:

x1:A1, .., xn:An |- A

Then pick(X) will enumerate x1, .., xn in X. We can now
use DCG to define tactics. Here is the tactic right//0
which will apply the invertible right introduction rules
from the Gentzen LK calculus repeatedly and also the id
rule from this calculus:

/* right//0 will apply invertible rules and the identity rule
on the right hand side of the actual sequent, repeatedly.
The identity rule is non-deterministic, the other rules
are deterministic. */
step --> rule(ifR((->))), !.
step --> rule(andR(,)), !.
step --> rule(iffR(_)), !.
step --> pick(Y), rule(Y).

steps --> prefer(_), step, steps.
steps --> [].

right --> prefer(_), step, steps.

And then there is the left//1 tactic which
tries to apply a left introduction rule from the
Gentzen LK calculus:

/* left//1 will apply a not necesseraly invertible rules on
the left hand side of the actual sequent, once. The parameter
identifies the formula that should be picked from the
sequent. */
left(Y) --> rule(ifL(,(->_),Y)).
left(Y) --> rule(andL((>>_),Y)).
left(Y) --> rule(iffL((->),Y)).

With these tactics, that do not implement a full theorem
prover, but nevertheless provide some convenience, we
can proof the same theorem as before already much
simpler:

?- theorem ex(a,b) :: a==>(a==>b)==>b by
right, left(x3), right.
Yes

With all this help, we are now almost in the middle of the
Tarski Knaster theorem. We are currently about to proof
that lfp and gfp are fixpoints and minimal resp. maximal.
We use the following definitions in our Mini Isabelle
Clone language:

:- fun lfp(u) :: (u set - > u set) - > u set by
lfp(f) = ∩ {a\(f(a) ⊆ a)}.

:- fun gfp(u) :: (u set - > u set) - > u set by
gfp(f) = ∪ {a\(a ⊆ f(a))}.

The minimality resp. maximinality proof goes already
through. But it turns out that the proof is not
complete, some constraints are not resolved. I have
analyzed the situation. It is that a redex remains
unresolved, resulting from the unification F(a) =
f(a). This unification results when applying
lemma_5_1 respectively lemma_5_2.

We are not yet sure what to do. The Jekejeke Minlog
interpreter does not allow non-determinisc
attribute variable hooks. So some higher order
matching that would do some Prolog enumeration
cannot be used inside the constraint solver. Maybe
do something in the spirit of label/1 from CLP(FD).

Source Code Fixpoint Proof
https://gist.github.com/jburse/0ccd12698bfa24ce5c36

G+ Post Progress in Proving Tarski Knaster
https://plus.google.com/116887476001511997780/posts/31MjagH4cEz

[Jan Burse]

Among others formalization taken from this source :

Induction principles formalized in the Calculus of Constructions (1988)
Gérard Huet, Programming of Future Generation Computers. Elsevier

yquem.inria.fr/~huet/PUBLIC/induction.pdf

Jan Burse schrieb:

[Jan Burse]

Dear All,

There was a suceess in Proving Tarski Knaster,
via a Prolog written Mini Isabelle Clone.

Small Warning, the current Mini Isabelle Clone
requires besides ISO Prolog the Jekejeke Minlog
extension for Attribute Variables and Forward
Chaining. But I guess other Prolog systems with
constraint frameworks, such as SICStus or SWI-Prolog
would also do, supposedly some work is invested
into porting the stuff.

These are the lessons learnt:

When doing the proofs we were wishing to have much better tactics,
tactics that embody real theorem provers. The proofs are still quite
tedious with the right//0 commands and the left//1 resp. left//2
commands. For the more complex proofs we could even less rely on
right//0 commands, since they would tore appart the definitions we were
using.

During the proofs we made some observations concerning our Mini Isabelle
Clone:

1) Subst Constraint Solving Missing
We had a couple of cases where type inference didn't work, already in
the head of a lemma. A suspended constraint of the form subst(_, k, T,
R) was the problem. We should realize our label idea from CLP(FD) and
generate solutions here. The solution set is finite, since R can only
have finite many sub-occurences of T.

2) Reduce Constraint Solving Missing
We had also a couple of cases where type inference didn't work since
a constraint of the form reduce(_, T, R) was suspended. We should also
realize our label idea here, but the problem is a little bit more
difficult. Without reference to some normal form and/or type information
it is to expect that there are infinitely many candidates.
This might also affect subst, when subst internally combines with
reduce. Which is the case in our prototype.

3) Specifying Implicits Missing
Because we did not yet implement the label idea, we couldn't make all
arguments implicit. This was an advantage since the more complex proofs
need the invention of some terms. We find in our code therefore lemma
specializations such as:

left(lemma_1_1(f(lfp(f)), {a\(f(a) ⊆ a)})).

The corresponding statement in Isabelle/HOL reads as follows and is
actually a specification of an implicit:

lemma_1_1[of "{a. les (f a) a}"]

We should figure out a syntax, so that we will be able later to also
specify implicits if necessary. Maybe something based on the pattern
variables idea as in Isabelle/HOL can be done .

Hope we can settle these issues in the future and may produce a much
better Mini Isabelle Clone soon.

Source Code of Proof & Assistant
http://gist.github.com/jburse/0ccd12698bfa24ce5c36

My Original Isabelle/HOL Code for the Problem
http://gist.github.com/jburse/0bca1b7b549b67d94189

Jan Burse schrieb:

[Jan Burse]

Jan Burse schrieb:

> My Original Isabelle/HOL Code for the Problem
> http://gist.github.com/jburse/0bca1b7b549b67d94189

Oops, this link wurks:
https://gist.github.com/jburse/0bca1b7b549b67d94189

[Jan Burse]

Its as easy as typing the following in the prompt:

?-
['https://gist.githubusercontent.com/jburse/0ccd12698bfa24ce5c36/raw/fixpoint3.p'].

Should also work from within the Android variant of Jekejeke Prolog.
Have to check. Little warning: The Mini Isabelle Clone requires Jekejeke
Runtime 1.0.5 and Jekejeke Minlog 0.7.5. These two will only be released
in a couple of weeks.

Jan Burse schrieb:
> Dear All,
>

[Jan Burse]

Can also be updated by the Jekejeke Prolog make/0
command. What we observed was that gist takes some
time to promote a new version to the tip URL, but
besides that the make/0 works.

Jan Burse schrieb: