Unification and variables

A unification variable stands for a term not yet known; it is assigned at most once, and backtracking undoes the assignment (Logic Programming, Constraints). The flags and builtins around that mechanism follow: inspecting a variable, the pattern fragment, the occur check, and the wildcard.

Unification variable inspection

A rule head does not normally fire on an unassigned variable: an input argument is matched, and matching against a rigid pattern would have to assign the hole (Constraints). To write a rule that does fire on a hole, match it in the head with the uvar keyword. It comes in a few shapes:

• uvar matches any hole;

• uvar as X matches a hole and binds X to the whole term, for the rest of the rule to use:

  even (uvar as X) :- !, declare_constraint (even X) [X].
  

• uvar Hd Args matches an applied hole, binding Hd to the bare variable and Args to the list of arguments it is applied to (the names in scope where it was created, followed by any it is explicitly applied to);

• uvar Hd Args as X is the same, and binds X to the whole applied term.

../code/uvar-pattern.elpi:

% `uvar` as a head pattern fires a rule on an argument that is still an
% unassigned unification variable:
%   uvar              — any hole
%   uvar as X         — ... and bind X to the whole term
%   uvar Hd Args      — an *applied* hole: Hd is the bare variable,
%                       Args the list of arguments it is applied to
%   uvar Hd Args as X — ... and bind X to the whole applied term

pred classify any.
classify (uvar _ [] as X)    :- !, print "unapplied hole:" X.
classify (uvar Hd Args as X) :- !, print "applied hole:" X "-- head" Hd "args" Args.
classify T                   :- print "not a hole:" T.

main :-
  classify Hole_,
  (pi a\ pi b\ classify (Applied_ a b)),
  classify 42.

unapplied hole: X0
applied hole: X1 c0 c1 -- head X1 args [c0, c1]
not a hole: 42

The builtin var is the same decomposition from a rule body, on a term the head did not already take apart with uvar: var V checks that V is unassigned, and var V Hd Args splits an applied one into its head Hd and its argument list Args.

The pattern fragment

Elpi’s unification is decidable and well-behaved as long as it stays within the pattern fragment (Lλ, Miller’s higher-order patterns, Miller, 1991): a unification variable applied only to distinct bound names. Outside of it, unification can have several, or infinitely many, most general solutions. Elpi does not guess: by default it aborts with an error on such a problem. The deprecated -delay-problems-outside-pattern-fragment flag makes it suspend the problem as a constraint instead, the way Teyjus does (Compatibility with Teyjus, Prolog and legacy Elpi).

distinct_names L checks that L is a list of pairwise-distinct bound names, so, given the Args from var above, it tells whether a variable is currently in the pattern fragment:

pred in-pattern-fragment any.
in-pattern-fragment X :- var X _ Args, distinct_names Args, !.
in-pattern-fragment _ :- print "outside the pattern fragment".

A variable’s own arguments, the names in scope when it was created via pi/sigma, are always distinct, so a freshly allocated variable is always in the fragment; it is only later applications, unification, or explicit reuse across scopes that can push a term outside it.

The occur check

Unification performs the occur check by default: assigning a variable to a term that already contains it is rejected, rather than building a cyclic term. Most Prolog systems default the other way, and Elpi’s choice is one of the deliberate departures collected in Compatibility with Teyjus, Prolog and legacy Elpi.

ground_term T checks that T holds no unification variables at all, useful for asserting that a computation has fully finished, for instance before serializing a term.

The occur check can be turned off for one predicate with the :nooc signature attribute. The standard library’s unsound_unif is plain unification with the check removed, and is defined with :nooc and nothing else:

% Unification without occur check. It can create infinite terms.
:nooc
func unsound_unif -> A, A.
unsound_unif X X.

So X = f X fails the occur check, but unsound_unif Y (f Y) succeeds, tying Y into a cyclic term:

../code/nooc.elpi:

% Unification (=) performs the occur check by default; a predicate marked
% :nooc, like the builtin unsound_unif, does not.

data tm.
symb f tm -> tm.

main :-
  ( X = f X, print "should not happen"
  ; print "= rejects X = f X (occur check)" ),
  ( unsound_unif Y (f Y), print "unsound_unif Y (f Y) succeeds"
  ; print "should not happen" ).

= rejects X = f X (occur check)
unsound_unif Y (f Y) succeeds

Code that uses :nooc then has to keep from ever building such a term: ground_term does not terminate on a cyclic term, and neither do most other term traversals.

The wildcard _

_ is a true wildcard, not a variable: every occurrence is independent, so two _ in the same head are never forced to be equal, unlike a repeated named variable:

../code/wildcard.elpi:

% A repeated named variable forces its occurrences to be equal; `_` never
% does, even used more than once in the same head.

pred same int, int.
same X X.                % the repeated X forces the two arguments to be equal

pred any int, int.
any _ _.                 % each _ is an independent wildcard: never forces anything

main :-
  (same 1 2, print "same 1 2 succeeds (unexpected)" ; print "same 1 2 fails, as expected"),
  (any 1 2, print "any 1 2 succeeds, as expected" ; print "any 1 2 fails").

same 1 2 fails, as expected
any 1 2 succeeds, as expected