Building Unification

Term building allows the access and construction of arbitrary terms. Since some of the predicates require arguments to be instantiated these predicates are not logically complete. Nevertheless most of the predicates are flexible enough so that they can be called in both directions. Namely they can be called with the modes (+, -), (-, +) and (+, +), whereby + indicates an instantiated argument.

For performance reasons the interpreter performs unification without occurs check. This can result in cyclic structures which are not logically sound in the usual Herbrand model interpretation. The cyclic structures might result in infinitely looping programs or in a looping during term output. For programs that need a logically sound unification a special predicate is provided which does only instantiate variables when the check fails.

The following term building and unification predicates are provided:

X = .. Y: [ISO 8.5.3]
If X is atomic then the predicate succeeds when Y unifies with [X]. If X is the compound F(A1, .., An) then the predicate succeeds when Y unifies with [F, A1, …, An]. If Y is [C] and C is atomic then the predicate succeeds when X unifies with C. If Y is [F, A1, …, An] and F is an atom then the predicate succeeds when X unifies with F(A1, .., An).
functor(X, N, A): [ISO 8.5.1]
If X is atomic then the predicate succeeds when N unifies with X and A unifies with 0. If X is the compound f(A1, .., An) then the predicate succeeds when N unifies with f and A unifies with n. If N is atomic and A is 0 then the predicate succeeds when Y unifies with N. If N is an atom, A is an integer n≥1 and A1, …, An are fresh arguments then the predicate succeeds when Y unifies with N(A1, .., An).
arg(K, X, Y): [ISO 8.5.2]
If K is a positive integer in the range of an arity and X is a callable f(A1, .., An) and then the predicate succeeds when 1≤k≤n and Ak unifies with Y.
set_arg(K, X, Y, Z):
If K is a positive integer in the range of an arity and X is a callable f(A1, .., An) then the predicate succeeds when 1≤k≤n and Z unifies with f(A1, .., Ak-1, Y, Ak+1, .., An).
X = Y: [ISO 8.2.1]
The predicate succeeds when X and Y unify, no occurs check is performed.
unify_with_occurs_check(X, Y): [ISO 8.2.2]
The predicate succeeds when X and Y unify, occurs check is performed.
X \= Y: [ISO 8.2.3]
The predicate succeeds when X and Y do not unify, no occurs check is performed.

The following Prolog flags for term building and unification are provided:

max_arity: [ISO 7.11.2.3]
The legal value is an integer. The value gives the maximum number of arguments in a compound. Default value is 2147483647. The value cannot be changed.

Kommentare