Previous Up Next

13  Limitations of the interpreter

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.

13.1  Lλ and non-Lλ unification problems

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

13.2  Restriction on the occurrences of logic variables

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.


Previous Up Next