Unify

tuprolog.unify ¶

Unification of logic terms.

Unification is the basic operation of logic programming: given two terms, it looks for a way of binding their variables so that the two terms become syntactically equal. For instance, f(X, b) and f(a, Y) unify by binding X to a and Y to b, while f(X) and g(X) do not unify, as their functors differ. Prolog uses unification to pass arguments (a goal is unified with the heads of the clauses defining it), to return results, and to deconstruct data.

The bindings unification finds are represented by a tuprolog.core.Substitution: a unifier (Substitution.Unifier) when unification succeeds, or the failed substitution (Substitution.Fail) when it does not. Among all the substitutions making two terms equal, unification computes the most general unifier (MGU), i.e. the one binding variables only as much as needed: any other unifier is an instance of it.

The occurs check forbids binding a variable to a term containing it (e.g. X to f(X)), which would otherwise denote an infinite term. It is enabled by default here: disabling it (as most Prolog systems do in =/2) is faster, but unsound whenever such cyclic bindings may arise.

This package offers:

mgu, unify and match: unification through the default strategy, returning respectively the MGU, the unified term, or whether the terms unify;
Unificator: the type of unification strategies, created by strict_unificator, naive_unificator (comparing numbers by value) and unificator / cached_unificator (memoizing recent results);
tuprolog.unify.exception: the exceptions signalling unification failures.

Examples:

>>> from tuprolog.core import atom, struct, var
>>> X, Y = var("X"), var("Y")
>>> unifier = mgu(struct("f", X, "b"), struct("f", "a", Y))
>>> unifier[X], unifier[Y]
(a, b)
>>> unify(struct("f", X, "b"), struct("f", "a", Y))
f(a, b)
>>> match(struct("f", X), struct("g", X))
False

See Also

tuprolog.core.Substitution, the type of unifiers; 2P-Kt's unification API.

Unificator `module-attribute` ¶

Unificator = _unify.Unificator

A unification strategy, i.e. an object unifying pairs of terms.

Unificators report failures as values, not exceptions: unifying terms that do not unify gives the failed substitution (or None, or False). Strategies differ in how they compare non-variable terms (tuprolog.unify.strict_unificator and tuprolog.unify.naive_unificator), and may be decorated with caching (tuprolog.unify.cached_unificator). Every operation enables the occurs check unless its last argument (occur_check_enabled) is False.

Members

mgu(term1, term2[, occur_check_enabled]): the most general unifier of the terms, or the failed substitution.
match(term1, term2[, occur_check_enabled]): whether the terms unify.
unify(term1, term2[, occur_check_enabled]): term1 with the most general unifier applied to it, or None.
merge(substitution1, substitution2[, occur_check_enabled]): the union of two substitutions, unifying the terms they bind the same variables to (the failed substitution if they disagree).
context: the bindings assumed to hold before unification starts.
Unificator.DEFAULT_CACHE_CAPACITY: the default size of cached unificators' caches (32).

Examples:

>>> from tuprolog.core import atom, substitution, var
>>> X = var("X")
>>> u = Unificator.strict()
>>> u.mgu(X, atom("a"))[X]
a
>>> u.merge(substitution({X: atom("a")}), substitution({X: atom("b")})).is_failed
True

Note

Wraps 2P-Kt's it.unibo.tuprolog.unify.Unificator interface.

DEFAULT_UNIFICATOR `module-attribute` ¶

DEFAULT_UNIFICATOR = Unificator.getDefault()

The default Unificator: a strict one, without caching, used by tuprolog.unify.mgu, tuprolog.unify.unify and tuprolog.unify.match.

strict_unificator ¶

strict_unificator(
    context: Substitution | None = None,
) -> Unificator

Creates a strict unification strategy.

A strict unificator deems two non-variable terms equal when they are identical, numbers included: the integer 1 and the real 1.0 do not unify.

Parameters:

Name	Type	Description	Default
`context`	`Substitution \| None`	The bindings assumed to hold before any unification starts: every result is computed as if they were merged into it. None (the default) means no bindings.	`None`

Returns:

Type	Description
`Unificator`	The strict unificator, without caching.

Examples:

>>> from tuprolog.core import integer, real
>>> strict_unificator().match(integer(1), real(1.0))
False

Note

Wraps 2P-Kt's Unificator.strict.

naive_unificator ¶

naive_unificator(
    context: Substitution | None = None,
) -> Unificator

Creates a naive unification strategy, which compares numbers by value.

Unlike strict_unificator's strategy, a naive unificator deems two numbers equal when their values are, regardless of their representation: the integer 1 and the real 1.0 unify.

Parameters:

Name	Type	Description	Default
`context`	`Substitution \| None`	The bindings assumed to hold before any unification starts. None (the default) means no bindings.	`None`

Returns:

Type	Description
`Unificator`	The naive unificator, without caching.

Examples:

>>> from tuprolog.core import integer, real
>>> naive_unificator().match(integer(1), real(1.0))
True

Note

Wraps 2P-Kt's Unificator.naive.

cached_unificator ¶

cached_unificator(
    unificator: Unificator,
    cache_size: int = DEFAULT_CACHE_CAPACITY,
) -> Unificator

Decorates a unificator so that it memoizes its most recent results.

The results of mgu and merge (hence of match and unify too) are stored in a least-recently-used cache, sparing their computation when the same terms are unified again. Caching an already cached unificator re-wraps the underlying one, with the new capacity.

Parameters:

Name	Type	Description	Default
`unificator`	`Unificator`	The unificator to decorate.	required
`cache_size`	`int`	The maximum amount of results the cache stores (32 by default).	`DEFAULT_CACHE_CAPACITY`

Returns:

Type	Description
`Unificator`	The cached unificator, behaving as `unificator` does.

Examples:

>>> from tuprolog.core import atom, var
>>> cached = cached_unificator(strict_unificator(), cache_size=8)
>>> cached.match(var("X"), atom("a"))
True

Note

Wraps 2P-Kt's Unificator.cached.

unificator ¶

unificator(
    context: Substitution | None = None,
) -> Unificator

Creates the recommended unification strategy: a cached, strict unificator.

Parameters:

Name	Type	Description	Default
`context`	`Substitution \| None`	The bindings assumed to hold before any unification starts: unifications conflicting with them fail. None (the default) means no bindings.	`None`

Returns:

Type	Description
`Unificator`	A `cached_unificator` decorating a `strict_unificator`.

Examples:

>>> from tuprolog.core import atom, substitution, var
>>> X = var("X")
>>> u = unificator(substitution({X: atom("a")}))
>>> u.match(X, atom("a")), u.match(X, atom("b"))
(True, False)

mgu ¶

mgu(
    x: Term, y: Term, occur_check: bool = True
) -> Substitution

Computes the most general unifier of two terms, through the default unificator.

Parameters:

Name	Type	Description	Default
`x`	`Term`	The first term. When the two terms have distinct roles, it is the subject (e.g. a goal, or a value), and `y` the reference (e.g. a clause head, or a pattern).	required
`y`	`Term`	The second term.	required
`occur_check`	`bool`	Whether variables may not be bound to terms containing them (True by default): disabling it is faster, but lets unification build cyclic bindings.	`True`

Returns:

Type	Description
`Substitution`	The most general unifier (a `tuprolog.core.Substitution.Unifier`, empty if the terms are
`Substitution`	already equal), or the failed substitution (`Substitution.Fail`, whose `is_failed` is
`Substitution`	True) if the terms do not unify.

Examples:

>>> from tuprolog.core import struct, var
>>> X, Y = var("X"), var("Y")
>>> unifier = mgu(struct("f", X, "b"), struct("f", "a", Y))
>>> unifier[X], unifier[Y]
(a, b)
>>> mgu(X, struct("f", X)).is_failed
True
>>> mgu(X, struct("f", X), occur_check=False).is_failed
False

See Also

unify, match, and Unificator.mgu.

unify ¶

unify(x: Term, y: Term, occur_check: bool = True) -> Term

Unifies two terms through the default unificator, returning the unified term.

Parameters:

Name	Type	Description	Default
`x`	`Term`	The first term, to which the unifier is applied.	required
`y`	`Term`	The second term.	required
`occur_check`	`bool`	Whether variables may not be bound to terms containing them (True by default).	`True`

Returns:

Type	Description
`Term`	`x`, with the most general unifier of `x` and `y` applied to it, or None if the terms do
`Term`	not unify.

Examples:

>>> from tuprolog.core import atom, struct, var
>>> unify(struct("f", var("X"), "b"), struct("f", "a", var("Y")))
f(a, b)
>>> print(unify(atom("a"), atom("b")))
None

See Also

mgu, match, and Unificator.unify.

match ¶

match(x: Term, y: Term, occur_check: bool = True) -> bool

Tells whether two terms unify, through the default unificator.

Parameters:

Name	Type	Description	Default
`x`	`Term`	The first term.	required
`y`	`Term`	The second term.	required
`occur_check`	`bool`	Whether variables may not be bound to terms containing them (True by default).	`True`

Returns:

Type	Description
`bool`	True if the terms unify, i.e. if `mgu` would not fail, False otherwise.

Examples:

>>> from tuprolog.core import atom, struct, var
>>> match(struct("f", var("X")), struct("f", "a"))
True
>>> match(atom("a"), atom("b"))
False

See Also

mgu, unify, and Unificator.match.

Unify

tuprolog.unify ¶

Unificator module-attribute ¶

DEFAULT_UNIFICATOR module-attribute ¶

strict_unificator ¶

naive_unificator ¶

cached_unificator ¶

unificator ¶

mgu ¶

unify ¶

match ¶

Unificator `module-attribute` ¶

DEFAULT_UNIFICATOR `module-attribute` ¶