Logic variable raising over support causes non-intuitive failures

[chaudhuri]

Consider this .thm:

Kind i type.
Type f i -> i.

Theorem works : exists E, nabla (x : i), E x = f x.
intros. search.

It works because E is replaced with ?1, and then we have to solve ?1 n1 = f n1, which succeeds.

However, suppose we write it as:

Theorem fails : nabla (x : i), exists E, E x = f x.
intros. search.

This fails because E is replaced with ?1 n1, where n1 came from the nabla introduction. (In the current implementation, exists-right raises the logic variable over its support, or we would not be able to solve exists X, X = n1, for instance.) Then we try to solve ?1 n1 n1 = f n1 which is not in the pattern/nominal fragment and fails. However, this is not an unprovable theorem because we can finish the proof with:

intros. witness f. search.

You might argue that writing nabla x, exists E, E x is just inviting trouble because E is already implicitly dependent on x. However, the failed search gives no indication that the failure was caused because of this unusual quantifier order and dependency.

I am not sure if this is a bug or not, since it is a quirk of the Abella implementation. (Note that G does not have logic variables, so we can't look to it for guidance.)

It was reported by Beniamino Accattoli.

Ping @thatdalemiller and @agacek in case you have any insight.

[ThatDaleMiller]

One should note that there are two different proofs of the "fails" theorem (based on two different unifiers). For example, a second proof is given by

Theorem fails : nabla (x : i), exists E, E x = f x.
intros. witness (x\ f n1). search.

I think that it is a mistake (at least, misleading) for the search command to declare a failure just become is ran into non-pattern unification problems. In this case, one might ask that the search command produce a warning stating something like "I've completed the proof except for the following unification problems." Systems like lambda Prolog do this: if there are non-pattern disagreement pairs left, those pairs are printed. For example, tjsim does the following:

[toplevel] ?-  (pi n\ F n n = n + n).

The answer substitution:
F = F

The remaining disagreement pairs list:
<F <constant> <constant>, <constant> + <constant>>

More solutions (y/n)? y

no (more) solutions

[toplevel] ?- 

The message printed out is not very clear, but it hints at the problem. Maybe the search command can output something along these lines.

It is often the case that the proposed theorem that leads to such non-pattern unification problems is not the theorem people were really wanting to write. Thus, the advice to switch the scope of the quantifiers is good advice. However, the full logic is rich and non-pattern unification problems must be addressed more fully.

[chaudhuri]

Not sure I understand the tjsim output. Why is F = F a solution and not F = +?

Anyway, the issue here is not so much the non-pattern-ness but that the treatment of logic variables is forcing a non-pattern problem when one could be avoided. I don't yet know of a way to be complete without raising logic variables over the support -- at least not without adding a special case to the unification engine.

[chaudhuri]

Perhaps @gnadathur97 and @yvting could weigh in as well?

[yvting]

I don't think this is a bug. The way the following theorem is stated

Theorem fails : nabla (x : i), exists E, E x = f x.

implies that E may depend on x. Raising E over x is necessary to capture this dependency. Otherwise, the soundness of Abella may be broken.

Sometimes Abella is just not clever enough to find a proof for something that is provable. This is OK since we do not aim for completeness. It will be helpful though that search can produce information indicating why the proof search fails, as Dale suggested.

Another thing to note is that for logical variables we only need to find some instances for them, instead of all possible instances, to solve the unification problem. Maybe pattern unification is too restrictive for finding the instantiation of logical variables. But I don't know if there are any alternative approaches.

[ThatDaleMiller]

To reply to Kaustuv: The response from tjsim is interpreted as follows:

The unifier is (F = F) (which says nothing) if the constraint, (x\ F x x) = (x\ x + x) is solvable. There are four unifiers for this unification problem: namely, instantiate F with one of the following (u\v\ u + u), (u\v\ v + u), (u\v\ u + v), (u\v\ v + v) The current version of Teyjus chooses not to enumerate these but preserves them as constraints.

Similarly, the theorem nabla (x : i), exists E, E x = f x is raised to yield the following equivalent problem exists E, nabla (x : i), E x x = f x which is equivalent to exists E, (x\ E x x) = (x\ f x) This formula has four different proofs. The only way to avoid non-pattern unification is to start with a different theorem. While it is probably the case that the people who reported this issue in the first place wrote the wrong theorem, it is, in fact, the case that the formulas displayed above are legitimate theorems and Abella should, in principle, be able to deal with them as well.

[chaudhuri]

Indeed, that's all I mean. Raising logic variables over the support is conservative (and correct), but it may rule out solutions that we may otherwise find with pattern unification.

One possibility is that for every exists-right, we try first with raising, and if it fails we try again without raising. Or, perhaps we retry only when the unification failure was caused because of non-patternness.

[chaudhuri]

Note that raising always does not necessarily reduce non-determinism in search either. A simple example: exists x, x = n1. Unless I'm badly misunderstanding something, there is only one proof of this in G.

If we transform this into the unification problem ?1 n1 = n1 then there are the two solutions ?1 <- x\ x and ?1 <- x\ n1 as Dale originally pointed out. The first of these corresponds to a "proof" that is not realizable with ground existential witnesses in G.

[yvting]

As far as I know unification in Abella assumes that solutions do not contain nominal constants. As a result, ?1 <- x\ n1 cannot be a solution of the unification problem. In other words, it is necessary to make the dependency of eigen or logic variables on nominal constants explicit in the unification problems.

[chaudhuri]

Ah, OK, never mind about raising always being possibly more non-deterministic then. The heuristic of not raising sometimes still remains on the table.

Having thought about it for a whole 15 minutes, though, I am not sure implementing this kind of retry heuristic makes a lot of practical sense, particularly when the support gets big. The heuristic basically describes a technique where instead of just iterating over permutations of nominal constants to solve pattern/nominal problems, we iterate over partial permutations (i.e., permutations + pruning), which can be costly.

[ThatDaleMiller]

Going back to Kaustuv's comment about raising and nondeterminism:

Note that raising always does not necessarily reduce non-determinism in search either. A simple example: exists x, x = n1. Unless I'm badly misunderstanding something, there is only one proof of this in G.

If we transform this into the unification problem ?1 n1 = n1 then there are the two solutions ?1 <- x\ x and ?1 <- x\ n1 as Dale originally pointed out. The first of these corresponds to a "proof" that is not realizable with ground existential witnesses in G.

As Yuting points out, there are not two solutions just one. One way to see this is the following. We start with exists x, x = n1. which is better written as nabla n1 exists x, x = n1. Apply raising yields the following theorem (notice that raising never changes the number of solutions to a unification problem) exists h nabla n1 , (h n1) = n1. This latter problem is effectively the same as exists h, (n1\ h n1) = (n1\n1). and this has the unique solution h -> (w\w) which yields the expected proof for the original theorem.

Returning to the original theorem that promoted this thread: I think that we put too much importance in pattern unification. I think that Abella should be making more allowances for non-pattern unification. Treating them as constraints would be a start. This will complicate the user interactions a bit.

[chaudhuri]

Abella already treats non-pattern problems as constraints.

Exposing the remaining constraints from searching for exists E, E n1 = n1 would require exposing logic variables to the user, which Abella currently does not do. Since logic variables are nameless and completely dependent on the execution environment, there is no sense in persisting them in the proof text.

If we are all absolutely committed to treating this as a non-pattern unification problem, then I would say that there is nothing to be done from the Abella implementation side. Users will just have to be better educated.

[ThatDaleMiller]

I see the point. I would suggest treating this as a non-pattern unification problem which means that search cannot do anything with it. The lesson is that search is more limited than one might think. The user will have to enter the proof more explicitly (providing the witness, in this case).

[chaudhuri]

Closing this since no changes seem reasonable at this time.