Writing an specifying a lambda Prolog interpreter

[Enrico Tassi]

Dear list, I'd like to prove some properties about the execution of
lambda Prolog programs accepted by a static checker.

The plan was to write the specification for the interpreter and the
static checker as a mod file (that is a lambda Prolog intereter in
lambda Prolog), and do proofs in Abella.

I've some troubles giving a type to the binder for clause parameters
(the same problem applies to pi as well, but for clause parameters it
is easier to motivate). This type works for me:

type param (A -> clause) -> clause.
type body term -> clause.

and I think I need A there since even in "hello world"

of (lam F) (arr S T) :- ...
of (app H A) T :- ...

the arity of F and, say, H are different and I'd like to use the same
"param" term constructor to write

param f\ param s\ param t\ body ...
param h\ param a\ param t\ body ...


Abella accepts the .sig and .mod but when I use the case tactic I get

Error: Cannot fully infer the type of the program clause: ...

Indeed, in my specification I've a clause like this one

backchain (param Clause) Goal NewGoal :-
backchain (Clause FRESH) Goal NewGoal.

where the type of FRESH is impossible to know, but it must exist since
the clauses are well typed (in the sense of the reasoning logic I
guess). Is there a way to make it work?

Best,
--
Enrico Tassi

[Yuting Wang]

Dear Enrico,

Currently, the kind of polymorphism supported by Abella is schematic (http://abella-prover.org/schm-poly/index.html) in the sense that type variables parameterizing over theorems are _placeholders_ for ground types. When constructing proofs for polymorphic theorems, Abella does not inspect, introduce or remove type variables. A resulting (schematic) proof contains exactly the same set of type variables parameterizing over the theorem. It represents an actual proof for a monomorphic theorem under any instantiation of type variables with ground types.

Type variables can parameterize over a collection of definitional clauses (called a definition block). In this case, they are again placeholders. 

Type variables can also parameterize over a single clause. Such a clause in a definition block represents an infinite collection of clauses under the instantiation of type variables in the block. Here, type variables are no longer interpreted as __schematic__ placeholders.

In your example, the clause in lambda Prolog 

backchain (param Clause) Goal NewGoal :-
    backchain (Clause FRESH) Goal NewGoal.

is translated to the following definitional clause in a definition block (where prog has the type o -> o -> prop. it takes the head and body of  the lambda Prolog clause as arguments):

    prog (backchain (param Clause) Goal NewGoal) (backchain (Clause FRESH) Goal NewGoal)

This clause is parameterized by a type variable A (in the type of param) and hence represents an infinite collection of clauses obtained by instantiating A with ground types. Since we use prog to capture the possible clauses in lambda Prolog, this interpretation exactly captures the ad-hoc polymorphism in lambda Prolog by which a polymorphic lambda Prolog clause represents an infinite collection of lambda Prolog clauses with ground types.

However, when we do case analysis against such a clause, if we cannot fully infer (fix) A to a known type, then we cannot construct a schematic proof. Because we are left with an infinite number of cases resulting from the possible instantiation of A, each of whose proof may have a vastly different structure. Continuing the above example, we need to derive 

   (backchain ((Clause:nat -> clause) (FRESH:nat)) Goal NewGoal)

   (backchain ((Clause:(nat -> nat) -> clause) (FRESH:(nat -> nat))) Goal NewGoal)

   (backchain ((Clause:bool -> clause) (FRESH:bool)) Goal NewGoal)

   (backchain ((Clause:(bool -> nat) -> clause) (FRESH:(bool -> nat))) Goal NewGoal)

   ......

The proof for each of the above case may have a different structure.

That is why you get the error message   "Error: Cannot fully infer the type of the program clause: ... "

I am not aware of an immediate solution with your current formalization of static checker in lambda Prolog. Maybe there is a way to change the specification so that Abella is able to reason about it schematically. A more detailed description of your program might be helpful to identify such a solution.

Best,

Yuting

[Enrico Tassi]

Many thanks for your detailed answer!

> A more detailed description of your program
> might be helpful to identify such a solution.

What I'm trying to do is to specify lambda Prolog itself, and
I've a lot of freedom, in the sense of deep/shallow embedding.

I'm attaching two versions of the interpreter.

The former uses the substitution provided by the specification
language, and there I'm afraid I need the A -> term quantification.

The latter implements substitution via copy, and contains an explicit
step of normalization. Still, I'm using the unification variables of
the specification language to model the ones of the object language,
and this requires some features that are not part of LP (and Abella).
Given I'm using Elpi, I could suspend copy on flexible terms and
add some CHR rules to make things work as expected. I did not think
about it enough to say that this part of the program is irrelevant and


Of course I could give up this path and specify unification as well,
but this seems much more work. After all, I want to prove that
something bad does not happen *during* runtime, so I have to write
a runtime, where existential variables do have a syntax. But the idea
of not having to specify HO unification was very tantalizing.

Best,
--
Enrico Tassi

[Dale Miller]

Dear Enrico,

Some comments on your project.

What I'm trying to do is to specify lambda Prolog itself, and
I've a lot of freedom, in the sense of deep/shallow embedding.

One problem I can see is that lambda Prolog "itself" is not really a formal system with deep properties.  The intuitionistic theory of STT (Church 1940) has deep properties.  But lambda Prolog, in particular, with its polymorphic typing and its implementation of pattern unification (and not full unification), differs from STT.

 

I'm attaching two versions of the interpreter.

If I was to try this project, I would certainly elaborate more on your interp2.elpi approach.   This avoids polymorphism entirely.   The cost is that you now have parts of your specification that are dependent on the signature of logic programs on which you are working.  Fortunately, that dependency is mostly factored through the specification of the copy predicate.  However, you will also need to have forall and exists constructors of higher-arity (even if you keep to only second-order quantification).  In particular, you will probably need also

type forall2 (term -> term -> term) -> term.
type exists2 (term -> term -> term) -> term.

etc

Given I'm using Elpi, I could suspend copy on flexible terms and
add some CHR rules to make things work as expected.

The suspend and CHR rules of Elpi will likely be critical for getting this project to work.

Is there a way to use CHR rules and suspension in Elpi to deal with the "occur-check" problem:  that is, the following query should fail:

 ?- copy (app X Y) X.

The naive execution of this goal will lead to a cycle.  The unification problem (app X Y) = X will, however, fail because of the occur check.  Can Elpi manage that via suspensions and CHR?

Of course I could give up this path and specify unification as well,
but this seems much more work. 

Yes, going that way would be very unfortunate! Best -Dale

[Yuting Wang]

Hi,

It took me a while to understand the ELPI code. 

It looks like that in the first specification, the "app" and "lam" constructors are only for the construction of object-level specifications (w.r.t. the formalization of the lambda Prolog interpreter). Normalization is taken care of by the meta-language. In the second specification, the "app" and "lam" constructors are also used directly to represent lambda terms in the formalization of the lambda Prolog interpreter. Normalization is carried out by copy which defines beta-reduction on terms represented using "app" and "lam".

I agree with Dale that the second approach is more feasible. I think forall2 and exists2 can be avoided by the following trick:

  - Define the types of "forall" and "exists" to be "term -> term". The previously defined "forall T" will now be encoded as "forall (lam T)". Same for "exists".

  - Change the definition of the clauses for "forall" and "exists" to use deep encoding of lambda applications

     run1 (forall F) GS P :- pi x\ copy x x => run [app F x|GS] P.

     run1 (exists F) GS P :- sigma X\ run [app F X|GS] P.

     backchain (forall F) G New :- !, backchain (app F New_) G New.

     beta-reduction of the deeply encoded lambda abstraction will be taken care of by copy.

Finally, my guess is that if you drop the postponing and constraint solving part, you should be able to encode the interpreter in lambda Prolog and reason about it in Abella. In reasoning you are free to postpone your goals if they are not immediately solvable. It is just that you cannot run the intepreter in lambda Prolog because it lacks the constraint solving mechanisms.

Best,

Yuting

--
You received this message because you are subscribed to the Google Groups "Abella" group.
To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/abella-theorem-prover/CAGbLtfjqyErGqzjvWww25gqY-z5djNP8mLz%2BnP4%3DukpmSEiH2A%40mail.gmail.com.