10.3 Equations

The variable in Oz are logic variable. A logic variable can be understood as placeholder for a value which can be filled in when needed. At run time, a logic variable can either be free, kinded, or determined, depending on how much is known about its value.

Logic variables can be used for writing equations. Solving equations possibly determines their values. Solving equations interpreted over trees can be done by a standard unification algorithm. In Oz, unification for infinite trees is built in.

Suppose for instance, that you want to unify the terms f(X X) and f(g(Y Z) Y) where X,Y,Z are logic variables denoting some possibly infinite tree. In order to do so, it is sufficient to solve the equation f(X X) = f(g(Y Z) Y) which can be done simply by feeding it into the Oz-emulator.

declare  
   X Y Z
in 
   f(X X) = f(g(Y Z) Y)
   {Browse [X Y Z]}

In the Browser, you can observe the result of the unification process. The variable Z is still free; the variables X and Y are bound to a term g(g(g(... Z) Z) Z) which can be solved by an infinite tree depending on the value of Z. Note that the equation X.2 = X.1.2 is valid independently of the choice of Z.

For observing variable assignment into infinite trees in Oz, the Browser provides two extra options for representation, either as graphs or as minimal graphs. The difference between the graph and minimal graph option can be observed at the following example:

declare  
   X Y Z
in 
   X=f(Y X)
   Y=f(Y X)
   {Browse X}

Note that you can rebrowse a term by selecting the field Rebrowse from the Browser's menu Select.

Unification in Oz terminates even though equations interpreted over infinite trees are solved. The reason is that a solved form of the equations which cycles can be stored in the Oz constraint store. However, the programmer has to care about termination, in particular, when applying a recursive procedure to an infinite tree. For instance, the following program does not terminate:

declare  
  L=infty|L  
  {Browse {Length L}}

Browsing infinite trees terminates in Oz. When choosing the tree option for representation then there is a fixed bound which limits the depth up to which an (infinite) tree is displayed.