substitution in equality

[htzh]

Is there a way to establish an equivalence relation (other than the structural one "=") that respects substitution? If I specify:

eq (F X) (F Y) :- eq X Y.

and then try to prove Theorem eq_congr: forall F X Y, {eq X Y} -> {eq (F X) (F Y)}., after intros, search times out.

[htzh]

I dug a little deeper. Unification seems to behave differently based on the context:

Abella < Query ((F : i -> i) X) = (F X).          
No more solutions.                                

Abella < Query forall (F : i -> i), (F X) = (F X).
Found solution:                                   
X = ?27                                           

No more solutions.

search timeout was red herring (actually due to symmetry or transitivity clause of eq), but due to the high order unification issue search fails even if substitution congruence is the only clause for eq.

[htzh]

Meanwhile elpi seems to have both unification working:

goal> (F X) = (F X).
Success:
  F = X0
  X = X1

goal> pi F\ (F X) = (F X).                          
Success:                  
  X = X0

[chaudhuri]

When you say eq (F X) (F Y) :- eq X Y, the head of the clause uses non-pattern terms which are outside the fragment of HHω that Abella supports. Abella only supports pattern terms, which roughly means that capitalized variables can only be applied to distinct bound variables.

The way to do something like this would be to say:

eq X Y :- factor_context X Y S T, eq S T.

and then define factor_context X Y S T to remove a common shared portion from X and Y yielding S and T respectively. How you define factor_context is up to you, but usually it reifies some structural recursion inherent in your terms.

The two queries are different because in the first case you are again asking for a solution to a non-pattern equation (however trivial), which Abella doesn't handle.

[htzh]

Thanks for the explanation! I understand eq (F X) (F Y) :- eq X Y would not work in general as synthesizing the context F embodies much of the work in a prover. However I would like to understand what the limitation is if I have an equality theory (say specifying group operations) and attempt to perform rewrites modulo the equalities. That is how do I avoid writing all the instances by hand like:

eq (neg X) (neg Y) :- eq X Y.
eq (plus X Y) (plus M N) :- eq X M, eq Y N.

etc.

I am exploring using Lambda Prolog in specifying math theories as opposed to type (meta-)theories. I would love to hear any insight you may have.

[chaudhuri]

This is a question for the Lambda Prolog experts, I think.

Ping @thatdalemiller, @gnadathur97 .

[gnadathur97]

I dug a little deeper. Unification seems to behave differently based on the context:

Abella < Query ((F : i -> i) X) = (F X).          
No more solutions.                                

Abella < Query forall (F : i -> i), (F X) = (F X).
Found solution:                                   
X = ?27                                           

No more solutions.

search timeout was red herring (actually due to symmetry or transitivity clause of eq), but due to the high order unification issue search fails even if substitution congruence is the only clause for eq.

It seems to me that the response you are getting in the first case is actually incorrect or at least misleading. "No more solutions" should signify that there are no solutions, whereas there clearly are solutions. The response you should get should be more like "Can't solve the unification problem" or something similar. The reason for this is what Kaustuv seems to be saying: the problem lies outside higher-order pattern fragment and the unification procedure used by Abella works only on (a slight extension of) the higher-order pattern class. It might be easy to pull your example back into the category of unification problems that are dealt with, essentially by checking for identity of terms even when they do not belong to the pattern class. In this sense, the example you are presenting here is different from what you had shown in the first example.

The explicit quantification over F makes the second query/example significantly different. The unification problem that has to be solved becomes akin to solving (c X) = (c X) for a constant c. This problem is essentially a first-order unification problem, something that is definitely contained within the higher-order pattern fragment.

[gnadathur97]

Thanks for the explanation! I understand eq (F X) (F Y) :- eq X Y would not work in general as synthesizing the context F embodies much of the work in a prover. However I would like to understand what the limitation is if I have an equality theory (say specifying group operations) and attempt to perform rewrites modulo the equalities. That is how do I avoid writing all the instances by hand like:

eq (neg X) (neg Y) :- eq X Y.
eq (plus X Y) (plus M N) :- eq X M, eq Y N.

etc.

I am exploring using Lambda Prolog in specifying math theories as opposed to type (meta-)theories. I would love to hear any insight you may have.

If I understand the problem you want to solve, I don't think there is a solution to it that is different from the one you have described. You seem to be wanting to harness the primitive equality to match the common parts of terms in a uniform way before comparing the embedded parts using a defined version of equality (given by the eq predicate). I do not see a way to do this. The solution you have described uses a defined predicate for the entire computation. The other alternative would be to use the primitive equality, but then the terms would have to be equal up to lambda conversion.

[htzh]

@gnadathur97 Professor Nadathur, thanks for your responses! Suppose for a moment that I could convince Abella of the following:

Theorem eq_congr: forall F X Y, {eq X Y} -> {eq (F X) (F Y)}.

then I should be able to apply it to a hypothesis like H1: {eq a b} to obtain H2: {forall F, eq (F a) (F b)}, which I can instantiate to H3: {eq (f a) (f b)}. So it is interesting that application of such an axiom is not problematic in principle but the difficulty lies in specifying such an axiom using Lambda Prolog.

Is it possible for a user to directly introduce such an axiom into Abella? Or I may not be understanding correctly how Abella works.