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** X, **forall** y z, X y z **=** y

can be solved, but

**exists** X, **forall** y, X y y **=** y

can’t, as it violates the first constraint (so that
`X`

can
take at least two values,
`x1\ x2\ x1`

and
`x1\ x2\ x2`

), and

**forall** y, **exists** X, **forall** z, X y z **=** y

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

**exists** X', **forall** y z, (X' y) y z **=** y

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