<< Prev | - Up - | Next >> |
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
.
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.
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.
declare
<Terms as Predicates>
<Unify Terms>
/*
{Browse {IsUnifiable [ALeft CoRef]}}
{Browse {IsUnifiable [BRight CoRef]}}
{Browse {IsUnifiable [ALeft BRight CoRef]}}
*/
<< Prev | - Up - | Next >> |