10.4 Efficiency

First-order unification for infinite trees can be implemented in quasi-linear time. The implementation in Oz is quadratic in worst case and linear for mostly all important cases.

A classical example where Robinson's original unification algorithm has exponential runtime is the following:

<UnifBinTree>=

proc{UnifBinTree X N}
   if N==0 then X=a
   else 
      Y
   in 
      X = f(Y Y)
      {UnifBinTree Y N-1}
   end 
end 
/*
declare X = {UnifBinTree $ 1000000}{Browse done}
*/

If you browse X then you have to wait for a while since X is a bound to the complete infinite binary tree. Even when the display depth is restricted to 15 (as by default in Oz) then the Browser output has size O(2^15).

Next we wish to measure the time that unification needs.

<Property time>=

/*
declare {Browse {Property.get time}}
*/

There are many time measures explained in the documentation. We now write a procedure that measures the run time of a procedure P without arguments.

<Time>=

fun{Time P}  
   T1 = {Property.get time}.user
   {P}   
   T2 = {Property.get time}.user
in 
   T2-T1
end

Next, we measure the time for building a representation of the complete binary tree of depth N.

<TimeUnif>=

fun{TimeUnif N}  
   {Time proc{$} {UnifBinTree _ N} end}
end 
 
/*
{Browse {TimeUnif  10000}}
{Browse {TimeUnif 100000}}
{Browse {TimeUnif 200000}}
{Browse {TimeUnif 400000}}
*/

For administrative reasons, we collect all the chunks presented so far into a chunk.

<Test TimeUnif>=

declare 
<UnifBinTree> 
<Property time> 
<Time> 
<TimeUnif>