Previous Up Next

8  Unification

A subset of λProlog, called Lλ, was presented in [Mil91] where it was shown that an implementation of proof search could be written in which only a small subset of higher-order unification was required. Furthermore, that subset was decidable, unary, and did not need typing information. This subset of unification was called Lλ-unification in [Mil91] but is now more commonly referred to as higher-order pattern unification [Nip93, NL05]. In that subset, variables in functional position are applied to distinct variables which must be bound in the scope of the binding of the functional variable.

For instance,

exists Xforall y zX y z = y

can be solved, but

exists Xforall yX y y = y

can’t, as it violates the first constraint (so that X can take at least two values, x1x2x1 and x1x2x2), and

forall yexists Xforall zX y z = y

can’t either, as it violates the second constraint and therefore could be rewritten

exists X'forall y z, (X' yy z = y

Bedwyr uses an extension of this higher-order pattern unification which handles ∇.

Previous Up Next