Terms and unification¶

Everything a logic program manipulates is a term: atoms (symbolic constants such as bart), numbers, variables (placeholders such as X), and compound terms (a functor applied to arguments, such as parent(homer, bart)). This notebook builds, parses, inspects and converts terms, then unifies them, i.e. finds the values of variables making two terms equal.

See also: Build and parse terms, Terms and variables.

Importing tuprolog starts the Java virtual machine running 2P-Kt (once per process, a second or two).

In [1]:

from tuprolog.core import atom, integer, real, struct, to_python, to_term, var

atom("bart"), integer(42), real(3.14), var("X")

from tuprolog.core import atom, integer, real, struct, to_python, to_term, var atom("bart"), integer(42), real(3.14), var("X")

Out[1]:

(bart, 42, 3.14, X_0)

Compound terms are built with struct, which converts Python values (strings become atoms, numbers numbers):

In [2]:

term = struct("parent", "homer", "bart")
term, term.functor, term.arity, list(term.args)

term = struct("parent", "homer", "bart") term, term.functor, term.arity, list(term.args)

Out[2]:

(parent(homer, bart), 'parent', 2, [homer, bart])

Terms can also be parsed from Prolog syntax:

In [3]:

from tuprolog.core.parsing import parse_term

t = parse_term("point(X, [1, 2 | Tail], 'hello world')")
t[0], t[1], t[2], t.is_ground

from tuprolog.core.parsing import parse_term t = parse_term("point(X, [1, 2 | Tail], 'hello world')") t[0], t[1], t[2], t.is_ground

Out[3]:

(X_1, [1, 2 | Tail_0], 'hello world', False)

Each variable gets a unique suffix when printed (X_0, X_1, ...): two var("X") calls create two distinct variables. Reuse the same object to refer to the same variable.

In [4]:

X = var("X")
struct("same", X, X), struct("different", var("Y"), var("Y"))

X = var("X") struct("same", X, X), struct("different", var("Y"), var("Y"))

Out[4]:

(same(X_2, X_2), different(Y_0, Y_1))

Python values convert to terms and back:

In [5]:

term = to_term([1, 2.5, "a", (True, "b")])
term, to_python(term)

term = to_term([1, 2.5, "a", (True, "b")]) term, to_python(term)

Out[5]:

([1, 2.5, a, (true, b)], [1, 2.5, 'a', (True, 'b')])

Unification¶

Two terms unify if some substitution of their variables makes them equal. The most general such substitution (the most general unifier, mgu) is what Prolog computes whenever it matches a goal against a clause.

In [6]:

from tuprolog.unify import match, mgu, unify

left, right = parse_term("point(X, 2)"), parse_term("point(1, Y)")
mgu(left, right)

from tuprolog.unify import match, mgu, unify left, right = parse_term("point(X, 2)"), parse_term("point(1, Y)") mgu(left, right)

Out[6]:

{X_1=1, Y_2=2}

In [7]:

unify(left, right), match(parse_term("f(a)"), parse_term("f(b)"))

unify(left, right), match(parse_term("f(a)"), parse_term("f(b)"))

Out[7]:

(point(1, 2), False)

A substitution can be applied to any term containing its variables:

In [8]:

X, Y = var("X"), var("Y")
from tuprolog.core import substitution

sigma = substitution({X: 1, Y: "two"})
struct("pair", X, Y).apply(sigma)

X, Y = var("X"), var("Y") from tuprolog.core import substitution sigma = substitution({X: 1, Y: "two"}) struct("pair", X, Y).apply(sigma)

Out[8]:

pair(1, two)

When terms cannot be unified, the result is the failed substitution:

In [9]:

failure = mgu(parse_term("f(a)"), parse_term("f(b)"))
failure, failure.is_failed

failure = mgu(parse_term("f(a)"), parse_term("f(b)")) failure, failure.is_failed

Out[9]:

({Failed Substitution}, True)