6
$\begingroup$

Let's define the integer ADT.

It has, as generators, the constant 0 (a generator) and the succ operation. Moreover, it also contains the add operation defined by the (usual) axioms

add (0, x) = x (where x is a variable of type integer)
add (succ(x), y) = succ(add(x,y)).

Let's assume that I have two terms: add(x, succ(succ(succ(succ(0))))) and succ(succ(succ(succ(succ(succ(0)))))).

Is there an algorithm that finds all the substitutions allowing the first term to be rewritten to the second term?

Thanks in advance, Ayroles

$\endgroup$
9
$\begingroup$

You could encode these into Horn Clauses (= Prolog) and use resolution (= Prolog's implementation technique).

More explicitly, your Prolog code file will look like the following:

add( 0,    N, N ).
add( succ(N), M, succ(Sum) ) :- add( N, M, Sum ).

Asking the following query at the command prompt in a prolog interpreter will give you an answer for X:

add( X, succ(succ(succ(succ(0)))), succ(succ(succ(succ(succ(succ(0))))))).

Which is:

X = succ(succ(0)) .

Using tracing within the Prolog interpreter will give you the series of substitutions used.

Fill all the gaps in yourself, and you will learn a lot.

$\endgroup$
8
$\begingroup$

The answer to your question is yes. Unification modulo an ACU (associative, commutative, unital) operator is decidable. See Baader and Snyder's chapter "Unification Theory" in the Handbook of Automated Reasoning.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy