eunify

eunify implements E-unification for SWI-Prolog. Set the free algebra free with eunify today.

The core predicate is eunify, implemented as

eunify(Alg, X = Y) =>
    cata(Alg, X, Z),
    cata(Alg, Y, Z).

It uses cata to recursively evaluate both X and Y to Z using Alg.

eunify is backend-agnostic (it's easy to add your own), and currently provides two backends:

Backend	Module	Use Case
CLP(FD)	library(eunify/clpfd)	Large problems
Naive	library(eunify/naive)	Small problems

Each backend module exports pairs_to_alg/2 to compile an algebra and apply_alg/3 to wrap it in a callable. For example, the natural numbers modulo 2 are described by the following algebra:

CLP(FD)

Naive

?- use_module(library(eunify/clpfd)). true. ?- pairs_to_alg([z-0, s(0)-1, s(1)-0], _Alg), rb_visit(_Alg, Alg). Alg = [s/1-i_o_state([_A], _B, []), z/0-i_o_state([], 0, [])], clpfd:in(_C, ..(0, 1)), clpfd: #<==>(#\/(_C, _D), 1), clpfd: #<==>(#/\(_E, _F), _C), clpfd:in(_E, ..(0, 1)), clpfd: #<==>(#=(_A, 1), _E), clpfd: #<==>(#=(_A, 0), _G), clpfd:in(_F, ..(0, 1)), clpfd: #<==>(#=(_B, 0), _F), clpfd: #<==>(#=(_B, 1), _H), clpfd:in(_D, ..(0, 1)), clpfd: #<==>(#/\(_G, _H), _D), clpfd:in(_G, ..(0, 1)), clpfd:in(_H, ..(0, 1)).

?- use_module(library(eunify/naive)). true. ?- pairs_to_alg([z-0, s(0)-1, s(1)-0], _Alg), rb_visit(_Alg, Alg). Alg = [s/1-[[0]-1, [1]-0], z/0-[[]-0]].

The CLP(FD) backend compiles each operation's cases into a single i_o_state(InVars, OutVar, State) term. The cases are compiled into a single CLP(FD) constraint on InVars and OutVar. z/0 becomes i_o_state([], 0, []) (zero inputs, output is 0, stateless), and s/1 becomes i_o_state([_A], _B, []) (input is _A, output is _B, stateless), where _A and _B are constrained by (_A #= 0 #/\ _B #= 1) #\/ (_A #= 1 #/\ _B #= 0) in which the two cases are apparent. CLP(FD) spaghettifies this into an unreadable but equivalent mess. The naive backend just keeps the raw Inputs-Output cases in a per-operation list.

Both backends accept algebras that contain variables. The CLP(FD) backend uses copy_term to apply operations to arguments without binding the parameters themselves, but we want variables in the algebra to be treated as globally-scoped existential variables, so it uses the state slot of i_o_state to bind these variables between the operation's definitional skeleton and its application.

CLP(FD)	Naive
?- pairs_to_alg([x-X, y-Y, f(0,1)-1], _Alg), rb_visit(_Alg, Alg). Alg = [f/2-i_o_state([0, 1], 1, []), x/0-i_o_state([], X, [X]), y/0-i_o_state([], Y, [Y])], clpfd:in(X, ..(inf, sup)), clpfd:in(Y, ..(inf, sup)).	?- pairs_to_alg([x-X, y-Y, f(0,1)-1], _Alg), rb_visit(_Alg, Alg). Alg = [f/2-[[0, 1]-1], x/0-[[]-X], y/0-[[]-Y]].

E-unification then determines values for X and Y, grounding the algebra:

CLP(FD)	Naive
?- pairs_to_alg([x-X, y-Y, f(0,1)-1], _Alg), rb_visit(_Alg, Alg), eunify(apply_alg(_Alg), f(x, y) = ?(Z)). X = 0, Y = Z, Z = 1, Alg = [f/2-i_o_state([0, 1], 1, []), x/0-i_o_state([], 0, [0]), y/0-i_o_state([], 1, [1])].	?- pairs_to_alg([x-X, y-Y, f(0,1)-1], _Alg), rb_visit(_Alg, Alg), eunify(apply_alg(_Alg), f(x, y) = ?(Z)). X = 0, Y = Z, Z = 1, Alg = [f/2-[[0, 1]-1], x/0-[[]-0], y/0-[[]-1]].

A technical note: the operations in the algebra can be nondeterministic (f(0) might not map to anything while f(1) might map to both 2 and 3). For example, the following succeeds under either backend because f(a, a) can evaluate to f(0, 1) and hence to 1:

?- pairs_to_alg([a-0, a-1, f(0,1)-1], _Alg),
   eunify(apply_alg(_Alg), f(a, a) = ?(1)).

Install

?- pack_install(eunify).