Unification in OBJ3

The following OBJ code specifies unification, first without occur check, and then with occur check; the code is executable, and a number of examples are given. This example is taken from Introducing OBJ.

obj LIST[X :: TRIV] is sorts List NeList .
  op nil : -> List .
  subsorts Elt < NeList < List .
  op __ : List List -> List [assoc id: nil] .
  op __ : NeList List -> NeList .
  op __ : NeList NeList -> NeList .
  protecting NAT .
  op |_| : List -> Nat .
  eq | nil | = 0 .
  var E : Elt .   var L : List .
  eq | E L | = 1 + | L | .
  op tail_ : NeList -> List [prec 120] .
  var E : Elt .   var L : List .
  eq tail E L = L .
endo

obj SUBST is sorts Eqn Term .
  protecting QID .
  subsorts Id < Term .
  pr TERMS is (LIST *(sort List to TermList, sort NeList to NeTermList))[Term].
  dfn Op is QID .
  op _[_] : Op TermList -> Term [prec 1] .
  op _=_ : Term Term -> Eqn [comm prec 120] .
  pr SYSTEM is (LIST *(sort List to System, sort NeList to NeSystem, 
     op nil to null, op (__) to (_&_)))[Eqn].
  op {_} : System -> System .   *** scope delimiter
  op _=_ : TermList TermList -> System [comm prec 120] .
  vars T U V : Term .   var Us : NeTermList .
  var S : NeSystem .    var Ts : TermList .
  eq (T Ts = U Us) = (T = U)& (Ts = Us).
  op let_be_in_ : Id Term Term -> Term .
  op let_be_in_ : Id Term TermList -> TermList .
  op let_be_in_ : Id Term Eqn -> Eqn .
  op let_be_in_ : Id Term System -> System .
  vars X Y : Id .     var F : Op .
  eq let X be T in nil = nil .
  eq let X be T in Y = if X == Y then T else Y fi .
  eq let X be T in F[Ts] = F[let X be T in Ts].
  eq let X be T in (U Us) = (let X be T in U)(let X be T in Us).
  eq let X be T in (U = V) = ((let X be T in U) = (let X be T in V)) .
  eq let X be T in null = null .
  eq let X be T in ((U = V)& S) = (let X be T in(U = V))& (let X be T in S).
endo

***> first without occur check
obj UNIFY is using SUBST with SYSTEM and TERMS .
  op unify_ : System -> System [prec 120].
  op fail : -> Eqn .
  var T : Term .            vars Ts Us : TermList .
  vars S S' S'' : System .  var X : Id .
  eq unify S = {{S}} .
  eq S &(T = T)& S' = S & S' .
  eq S & fail & S' = fail .
  eq let X be T in fail = fail .
  eq {null} = null .
  eq {fail} = fail .
  vars F G : Op .   vars X : Id .
  eq {S & (F[Ts] = G[Us])& S'} = if F == G and | Ts | == | Us |
     then {S & (Ts = Us) & S'} else fail fi .
  eq {S & {S' &(X = T)& S''}} = if X == T then {S & {S' & S''}} else
     {(X = T)& (let X be T in S)& {let X be T in (S' & S'')}} fi .
endo
reduce unify 'f['g['X] 'Y] = 'f['g['h['Y]] 'h['Z]].
reduce unify 'f['X 'Y] = 'f['Y 'g['Y]].
reduce unify ('f['g['X] 'Y] = 'f['g['h['Y]] 'h['Z]])& ('h['X] = 'Z).
reduce unify 'f['X 'g['Y]] = 'f['Z 'Z].
reduce unify 'f['X 'g['Y]] = 'f['Z].
reduce unify 'f['Y 'g['Y]] = 'f['h['Z] 'Z].
reduce unify 'f['Y 'a[nil]] = 'f['g['a[nil]] 'Z].

***> now add occur check
obj UNIFY-OCH is using UNIFY .
  op _in_ : Id TermList -> Bool .
  vars X Y : Id .   var F : Op .
  var T : Term .    var Ts : NeTermList .
  eq X in Y = X == Y .
  eq X in F[Ts] = X in Ts .
  eq X in T Ts = X in T or X in Ts .
  cq (X = T) = fail if X in T .
endo
reduce unify 'f['g['X] 'Y] = 'f['g['h['Y]] 'h['Z]].
reduce unify 'f['X 'Y] = 'f['Y 'g['Y]].
reduce unify ('f['g['X] 'Y] = 'f['g['h['Y]] 'h['Z]])& ('h['X] = 'Z).
reduce unify 'f['X 'g['Y]] = 'f['Z 'Z].
reduce unify 'f['X 'g['Y]] = 'f['Z].
***> reduce unify 'f['Y 'g['Y]] = 'f['h['Z] 'Z].
***> this blows up!
reduce unify 'f['Y 'a[nil]] = 'f['g['a[nil]] 'Z].

Click here to see the OBJ3 output from this example.

Notice that LIST is a generic module, also called a parameterized module in OBJ; it can be thought of as a template that creates new modules, by instantiating the formal parameter X with some actual parameter, which could be just a sort, as in the expression LIST[Eqn], or could be a whole module, as in the expression LIST[LIST[INT]]. (The details of how this works are rather complex, but are not needed for this example; see Introducing OBJ if you really want to know. OBJ generic modules are similar to those of Ada, but much more general; in fact, the Ada notion was inspired by the one used in OBJ.)

Another OBJ construction used in the above is renaming, which allows you to change the names of sorts and the syntax of operations in modules, as in the expression LIST *(sort List to System), which renames the sort List to be System. In the example above, the syntax for the concatenation operation on lists is also renamed using this construction. Notice that the parameter instantiation is done after the renaming, although it could also have been done in the other order.

Back to CSE 230 homepage