Unificator

Unifies pairs of Terms, computing the most general unifier (MGU) that makes them syntactically equal, if any exists.

A Unificator does not perform I/O or throw on failure: unification outcomes are represented as values, namely Substitutions. A successful unification yields a Substitution.Unifier (possibly empty, i.e. Substitution.empty); a failed one yields the Substitution.Fail singleton returned by Substitution.failed. match and unify are convenience operations built on top of mgu.

Two orthogonal choices distinguish concrete unification strategies, both obtainable from this interface's companion object:

• how two non-variable terms are deemed equal while building unification equations (e.g. strict compares with plain Term.equals, while naive additionally compares numeric terms by value); and

• whether occurs-check is enabled, controlled per-call via the occurCheckEnabled parameter of mgu, match and unify (true by default). Occurs-check prevents a variable from being bound to a term that contains that same variable (which would otherwise produce an infinite/cyclic term); disabling it trades soundness for speed, which is safe only when the caller already knows the operands cannot give rise to such a cycle.

When the operands have distinct semantic roles, the subject term (such as a goal, query, actual value, or sought item) should be passed first, and the reference term (such as a pattern, rule head, expected value, or stored candidate) second. Calls whose operands have no such roles may retain their natural or mathematical order.

Although unifiability is symmetric, the substitutions and unified terms returned by mgu and unify can retain operand orientation. Reordering their arguments is therefore a behavioral change and requires appropriate tests.

val unificator = Unificator.default
val x = Var.of("X")
val substitution = unificator.mgu(x, Atom.of("a")) // {X -> a}
unificator.match(x, Atom.of("a")) // true
unificator.unify(x, Atom.of("a")) // a

To customize how terms are compared, or to observe/alter the equation-solving process, extend AbstractUnificator instead of implementing this interface directly.

Inheritors