10.7 Exercises

• Consider the following representation of terms:

  term ::= var | f(term ... term)

  where a variable var is represented by an integer. Write a function Decompose:term->var*[basic] that decomposes a term into a pair of a variable denoting the root of the term and a list of basic constraints where the latter have the following abstract syntax:

  basic ::= eq(var var) | eq(var f(var ... var))

  for example f(1 g(a 1 2)) should decompose into:

  3#[eq(3 f(1 4)) eq(4 g(5 1 2)) eq(5 a)]

• Write a function Substitute:var*[basic]->term that takes a pair of a variable and a list of basic constraints and returns the corresponding term representation. Apply the function to

  1#[eq(1 f(2 2))
   eq(2 f(3 3))
   eq(3 f(4 4))
   eq(4 f(5 5))
   eq(5 f(6 6))
   eq(6 f(7 7))
   eq(7 f(8 8))
   eq(8 f(9 9))]

  Then to

  1#[eq(1 f(2 2 2 2 2))
   eq(2 f(3 3 3 3 3))
   eq(3 f(4 4 4 4 4))
   eq(4 f(5 5 5 5 5))
   eq(5 f(6 6 6 6 6))
   eq(6 f(7 7 7 7 7))
   eq(7 f(8 8 8 8 8))
   eq(8 f(9 9 9 9 9))]

  If it gets very slow, can you identify the cause of the inefficiency and modify your implementation to avoid it?

• Write a function Unify:term->bool that test wether two terms are unifiable. Suppose that terms are represented as above. Hint: Replace integers by Oz variables in a first step and use exception handling to catch failure.

• Feature unification: Give a closure algorithm that unifies record descriptions rec ::= f(f_1:rec ... f_n:rec) | var where all atoms f_1 ... f_n are pairwise distinct (on paper). Hint: adapt the unification algorithm presented in the lecture and reproduced below.

• Write a function Unify:rec->bool that tests whether two records are unifiable. Suppose again that variables are represented by integers.

• Zusatzaufgabe: A solved form is a set of equation var_1=term_1 ... var_n=term_n where all variables var_1 ... var_n are pairwise distinct. Test whether there exists a finite solution sol:var->term that satisfies all equations. Hint: there exists a finite solution if and only if the solved form is acyclic (when considered as a graph whose nodes are the variables).

• Zusatzaufgabe: implement unification using the algorithm of the lecture.

Unification Algorithm

Here are the rules for computing the solved form of a conjunction of basic constraints. In the following, S and B are conjunctions of basic constraints. The algorithm is presented as a rewriting algorithm: it starts with true:B and terminates with S:true or S:false. When it terminates with S:true, S is the solved form of the input basic constraint B. When it terminates with S:false, the original B is unsatisfiable.

We say that X is bound S if S contains a basic constraint with X on the left-side of the equation. The algorith maintains the following invariant for S:B: if S contains an equation X=Y, then X does not occur in B, nor in S except in equation X=Y. We write B[X/Y] for the resulting of replacing every occurence of X in B by Y.

S : true & B  ->  S : B
S : X=X  & B  ->  S : B
S : X=Y  & B    where X and Y are distinct identifiers
      if X not bound in S
                  -> S[X/Y] & X=Y : B[X/Y]
 else if Y not bound in S
                  -> S[Y/X] & Y=X : B[Y/X]
 else X=f(X1...Xn) in S and Y=g(Y1...Ym) in S
      if f!=g or n!=m
                  -> S : false
      else        -> S[X/Y] & X=Y : (X1=Y1 & ... & Xn=Yn & B)[X/Y]
S : X=f(X1...Xn) & B
  if X=g(Z1...Zm) in S
      if f!=g or n!=m
                  -> S : false
      else        -> S : X1=Z1 & ... Xn=Zn & B
  else            -> S & X=f(X1...Xn) : B