The strategy used by Bedwyr for attempting proofs is not complete. That strategy involves using two provers (prover-0 and prover-1), tabling, and depth-first search. Many of the incompleteness that one encounters in traditional logic programming languages, such as Prolog and λProlog, resulting from depth-first search certainly reappear in Bedwyr. We mention two additional sources of incompleteness in the proof search engine of Bedwyr.
Bedwyr allows for unrestricted applications of variables to argument but it is only willing to solve Lλ-unification problems. As a result, Bedwyr will occasionally complain that it needs to solve a “not LLambda unification problem” and stop searching for a proof.
To illustrate this aspect of Bedwyr’s incompleteness, consider the problem of specifying the instantiation of a first-order quantifier. In particular, consider the specification
|Kind tm, fm type. Type all (tm -> fm) -> fm. Type p tm -> fm. Type a tm. Define instan : fm -> tm -> fm -> prop by instan X T (B T) := X = (all B).|
instan relates a universally quantified formula and a term
to the result of instantiating that quantifier with that term. It is the
case, however, that a unification problem containing
(B T) does
not belong to the Lλ subset. As a result, the following query results in a
|?= instan (all x\ p x) a (p X). At line 1, byte 28: Not LLambda unification encountered: a. ?=|
In some situations, a specification can be written so that the problematic
unification is delayed to a point where the unification problem is within the
Lλ restriction. In this particular case, if the definition of
instan is rewritten with the logically equivalent clause
|Define instan : fm -> tm -> fm -> prop by instan X T Y := X = (all B) /\ Y = (B T).|
this same query now returns an appropriate solution.
|?= instan (all x\ p x) a (p X). Solution found: X = a More [y] ? No more solutions. ?=|
An improvement to Bedwyr would be for it to automatically delay unification problems that are outside the Lλ-subset: delaying “difficult” unification problems in the hope that future instantiations and β-reduction will make them “simple” is employed in such systems as Twelf and the second version of the Teyjus implementation of λProlog [GHN+08].
As we have already noted, in the current implementation of Bedwyr there are restrictions on negative occurrences of logic variables – i.e. to the left of an implication. This restriction arises from the fact that we do not have a satisfactory and comprehensive understanding of unification in the prover-1 that incorporates such variables. As a result, Bedwyr is incomplete since it generates a run-time error in these cases. Consider the following two queries.
|?= nabla f, exists X, X = 42 -> false. At line 1, byte 35: Logic variable encountered on the left: H. ?= nabla f, exists X, f X = 42 -> false. Yes. More [y] ? No more solutions. ?=|
The first query is certainly meaningful and is provable if there is a term different from 42 (say, 43): in Bedwyr, this query generates a run-time error since it requires dealing with a prover-1 existential variable within prover-0 unification. The second query illustrates that some instances of prover-0 unification can tolerate the occurrences of prover-1 existential variables.
Sometimes, one can change a specification to avoid this runtime error. A simple example is provided by the following two queries.
|?= exists X, (X = 42 -> false) /\ X = 17. At line 1, byte 38: Logic variable encountered on the left: H. ?= exists X, X = 17 /\ (X = 42 -> false). Yes. More [y] ? No more solutions. ?=|
Such reordering of goals is something a future version of Bedwyr might attempt to do automatically.