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). |

Thus,
`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
runtime error.

?= 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.