NotInProlog("application head: ...")

[htzh]

I get this exception when an Elpi_ast.Lam term is at the head of an application. Why is this disallowed? In the test file llam.elpi there seems to be plenty of examples of lambda expression as head. What is the magic there?

[htzh]

The following produces an exception:

main :-
  (eq\F\        pi x\ pi y\ eq (F y x) x) (x\y\x = y) F, F = (a\b\b).

But the following succeeds:

test P T :-
  P (x\y\x = y) F, F = T.
main :-
  test (eq\F\        pi x\ pi y\ eq (F y x) x) (a\b\b).

Is there a reason for the difference?

[gares]

The data type of terms cannot represent arbitrary applications: https://github.com/LPCIC/elpi/blob/master/src/elpi_data.ml#L54 It can only represent an applied constant or an applied unification variable. In a sense "apparent beta redexes" are not part of the syntax. Of course assigning a unification variable can produce a redex that that eagerly reduced. The reason is an implementation choice.

Note that you don't need a predicate, you can just say F = (x\...), F t.

May I aske how you ended up in this situation? (I don't think it is natural to write beta redexes by hand, are you generating code?)

[gares]

You can also write macro @f x :- ... . main :- @f t by the way, since macro expansion beta reduces for you.

[htzh]

Thanks for the explanation! I was trying to understand the unification patterns in lambda Prolog. In the process I encountered the exception produced by apparent beta redexes. I don't need them and your explanation helps a lot in my understanding of the behavior here.

My interest is in exploring using lambda Prolog for developing math theories. I am trying to understand if I partially specify an equivalence relation such as:

eq (plus one one) two.
eq (plus (neg X) Y) zero :- eq X Y.

how do I then obtain an equivalence closure (that is the smallest reflexive, symmetric and transitive relationship containing the spec)?

Even more challenging, how can I specify congruence over equality (in essence, eq (F X) (F Y) :- eq X Y.) without having to hand instantiate the context F for every possible construction? (It is during this experimentation that I encountered the exception but now I see that the exception is due to my lack of understanding of the implementation.) If you have any insight in using ELPI for rewriting modulo equality I would love to hear.

[htzh]

When I said "obtain the equivalence closure" I only meant in the weak sense that if a relation is in the closure then it is obtainable (as in using some tactic) so the specification itself may contain non-terminating path. Similarly for rewriting modulo equality I also meant the rewriting to be directed through tactics (requiring the context F to be partially specified when invoking a tactic, for example). I understand the general problem is not decidable but I am interested in how far one could go with ELPI.

As I understand it these are typically locked up in proof assistants which come combined with particular foundational theories (say CIC). I find it tantalizing that tools like ELPI may allow one to explore a particular theory using customized inference rules, unencumbered with the complications of proof assistants. I am hoping this may allow one more flexibility to explore a particular space in larger steps, with less concern for foundational issues. In any case if correctness is a concern then one can produce a skeleton proof plan through the exploration and use regular proof assistants to fill in the gaps.

For sure this is much beyond the scope of understanding why an exception was produced :-) However as you inquired about what I was working on I am hoping that you may provide insights in the suitability of ELPI for the things I am interested in.

[gares]

wrt closing your relation, you could do it like this:

eq1 (plus one one) two.
eq1 (plus (opp X) Y) zero :- eq X Y.
eq X X :- !.
eq A B :- eq1 A A1, !, eq A1 B.
eq A B :- eq1 B B1, !, eq A B1.

Untested. The idea is to see eq1 as doing 1 step, and eq as rewriting both terms to their normal form.

The contextual closure is painful because you are use Elpi's application to model the object language application. You could write something along these lines:

eq1 (app [plus,one,one]) zero
...
eqCtx (app [A,B,C]) (app [A,B1,C)) :- eq1 B B1.

Note that the context rule is for any binary symbol A, not just plus.

Hope it helps

[htzh]

Thanks for the reply! I believe the transitive closure code you wrote would not work in general due to the cut. The cut is saying take a step and commit to it. If the step later leads to dead ends then fail. But the first step may be in the wrong direction. I think the closure problem is generally hard if one is not starting from a confluent and terminating relationship (which implies unique normal forms). I just learned this from Term Rewriting and All That which is dedicated to the topic we are discussing (section 2.1 gives a very good intro).

I think you are right that if I want a more general solution I will need to abandon using Elpi's application. The list idea is interesting. It goes back to plain Prolog. By the way does Elpi require list to be parameterized on a single type? (I read that Elpi does not care about types.) In the list example are you suggesting everything be in a single base type like tm?

I will close the issue soon as my original question was well answered.

[gares]

I think the closure problem is generally hard if one is not starting from a confluent and terminating relationship

yes, I was assuming that. EDIT: if you are going to saturate your rewrite system, then I suggest your don't only give a syntax to application nodes, but to "rewrite rules" themselves, so that you can change their orientation, size their LHR/RHS, and so on.

In the list example are you suggesting everything be in a single base type like tm

yes, but depending on your object language you can play with this, you could say that app takes a function symbol and a list of sub terms, if these two terms are very different in nature in your language.

I read that Elpi does not care about types

the interpreter would run fine, but the elpi-checker thing would complain. You may want to pass -no-TC to disable the checker. I don't think it is a good idea to ignore type errors. It is OK for a quick experiment.

[htzh]

Thanks for all your help! I will close the issue now. I think I will take a closer look at coq-elpi to get a better feel of how elpi can be used. I will start with your papers and see how much I can understand :-)