<< Prev | - Up - | Next >> |
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:
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.
/*
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.
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.
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.
declare
<UnifBinTree>
<Property time>
<Time>
<TimeUnif>
<< Prev | - Up - | Next >> |