12.3 Constraints as Predicates

Oz provides ``constraints as values'' in a way which can be paraphrased as ``constraints as predicates''. In this section, we first give the general idea and then apply it: We show how to testing the unifiability of a set of terms with variables such that failure cannot raise a programming error.

For instance, the following predicate imposes a coreference constraint on its argument.

proc{$ X} Y in X=f(Y Y) end

This predicate expresses the set of all trees X with the property of having two equal subtrees at first and second position. When applying this procedure to an argument Z then the constraint Z=f(Y Y) is told to the Oz constraint store.

Predicates are values in Oz and can thus be bound to variables. Encapsulated search in Oz can resolve a predicate and return a list of its solutions. Each solution is a constraint which can be returned as a predicate again.

In the following, we use constraints as predicates in order to check whether a set of terms is unifiable. A term may contain variables but we assume that variables in distinct terms are distinct. A term t with free variables X1,...,Xn is encoded by a predicate proc{$ X} X1 ... Xn in X=t end.

<Terms as Predicates>=

proc{CoRef  X} Y in X=f(Y Y) end 
proc{ALeft  X} X=f(a _) end 
proc{BRight X} X=f(_ b) end

The procedure Search.allP inputs a unary predicate and returns a list of unary predicates each of which represents a solution to the input predicate. If a predicate encapsulates a constraint then a solution of it is a predicate which encapsulates a solved form of the constraint.

<Unify Terms>=

fun{Unify Ts}
   {Search.allP  
    proc{$ X}
       {ForAll Ts proc{$ T} {T X} end}
    end   
    1 _}
end 
fun{IsUnifiable Ts}
   case {Unify Ts}
   of nil then false 
   else true 
   end 
end

We can now run the tester for unifiability. Note that our test does not raise a programming error even if unification fails.

<Checking Unifiability>=

declare  
<Terms as Predicates> 
<Unify Terms> 
/*
{Browse {IsUnifiable [ALeft CoRef]}}
{Browse {IsUnifiable [BRight CoRef]}}
{Browse {IsUnifiable [ALeft BRight CoRef]}}
*/