[ Pobierz całość w formacie PDF ]
." If the partial values are incompatible then they cannot be unified.Forexample, unifying the two records:person(name:X1 age:26)person(name:"George" age:25)The records have different values for their age fields, namely 25 and 26,so they cannot be unified.This unification will raise a failure exception,which can be caught by a try statement.The unification might or mightnot bind X1 to "George"; it depends on exactly when it finds out thatthere is an incompatibility.Another way to get a unification failure is byexecuting the statement fail.Copyright © 2001-3 by P.Van Roy and S.Haridi.All rights reserved. 102 Declarative Computation ModelX=f(a:X b:_)X f a bX=f(a:X b:X)X f a bX=YY=f(a:_ b:Y)Y f a bFigure 2.22: Unification of cyclic structures" Unification is symmetric in the arguments.For example, unifying the tworecords:person(name:"George" age:X2)person(name:X1 age:25)This binds X1 to "George" and X2 to 25, just like before." Unification can create cyclic structures, i.e., structures that refer to them-selves.For example, the unification X=person(grandfather:X).Thiscreates a record whose grandfather field refers to itself.This situationhappens in some crazy time-travel stories." Unification can bind cyclic structures.For example, let s create two cyclicstructures, in X and Y, by doing X=f(a:X b:_) and Y=f(a:_ b:Y).Now,doing the unification X=Y creates a structure with two cycles, which we canwrite as X=f(a:X b:X).This example is illustrated in Figure 2.22.The unification algorithmLet us give a precise definition of unification.We will define the operationunify(x, y) that unifies two partial values x and y in the store Ã.Unificationis a basic operation of logic programming.When used in the context of unifica-tion, store variables are called logic variables.Logic programming, which is alsocalled relational programming, is discussed in Chapter 9.The store The store consists of a set of k variables, x1,., xk, that are parti-tioned as follows:Copyright © 2001-3 by P.Van Roy and S.Haridi.All rights reserved. 2.7 Advanced topics 103" Sets of unbound variables that are equal (also called equivalence sets ofvariables).The variables in each set are equal to each other but not to anyother variables." Variables bound to a number, record, or procedure (also called determinedvariables).An example is the store {x1 = foo(a:x2), x2 =25, x3 = x4 = x5, x6, x7 = x8}that has eight variables.It has three equivalence sets, namely {x3, x4, x5}, {x6},and {x7, x8}.It has two determined variables, namely x1 and x2.The primitive bind operation We define unification in terms of a primitivebind operation on the store Ã.The operation binds all variables in an equivalenceset:" bind(ES, v ) binds all variables in the equivalence set ES to the number orrecord v.For example, the operation bind({x7, x8},foo(a:x2)) modifiesthe example store so that x7 and x8 are no longer in an equivalence set butboth become bound to foo(a:x2)." bind(ES1, ES2) merges the equivalence set ES1 with the equivalence setES2.For example, the operation bind({x3, x4, x5}, {x6}) modifies the ex-ample store so that x3, x4, x5, and x6 are in a single equivalence set, namely{x3, x4, x5, x6}.The algorithm We now define the operation unify(x, y) as follows:1.If x is in the equivalence set ESx and y is in the equivalence set ESy, thendo bind(ESx, ESy).If x and y are in the same equivalence set, this is thesame as doing nothing.2.If x is in the equivalence set ESx and y is determined, then do bind(ESx, y).3.If y is in the equivalence set ESy and x is determined, then do bind(ESy, x).4.If x is bound to l(l1 : x1,., ln : xn) and y is bound to l (l1 : y1,., lm : ym)with l = l or {l1,., ln} = {l1,., lm}, then raise a failure exception.5.If x is bound to l(l1 : x1,., ln : xn) and y is bound to l(l1 : y1,., ln : yn),then for i from 1 to n do unify(xi, yi).Handling cycles The above algorithm does not handle unification of partialvalues with cycles.For example, assume the store contains x = f(a:x) andy = f(a:y).Calling unify(x, y) results in the recursive call unify(x, y), whichis identical to the original call.The algorithm loops forever! Yet it is clearthat x and y have exactly the same structure: what the unification should do isCopyright © 2001-3 by P.Van Roy and S.Haridi.All rights reserved. 104 Declarative Computation Modeladd exactly zero bindings to the store and then terminate.How can we fix thisproblem?A simple fix is to make sure that unify(x, y) is called at most once for eachpossible pair of two variables (x, y).Since any attempt to call it again will notdo anything new, it can return immediately.With k variables in the store, thismeans at most k2 unify calls, so the algorithm is guaranteed to terminate.Inpractice, the number of unify calls is much less than this.We can implementthe fix with a table that stores all called pairs.This gives the new algorithmunify (x, y):" Let M be a new, empty table." Call unify (x, y).This needs the definition of unify (x, y):" If (x, y) " M then we are done." Otherwise, insert (x, y) inM and then do the original algorithm for unify(x, y),in which the recursive calls to unify are replaced by calls to unify.This algorithm can be written in the declarative model by passing M as two extraarguments to unify.A table that remembers previous calls so that they can beavoided in the future is called a memoization table.Displaying cyclic structuresWe have seen that unification can create cyclic structures.To display these inthe browser, it has to be configured right.In the browser sOptionsmenu, picktheRepresentationentry and choose theGraphmode.There are three displaymodes, namelyTree(the default),Graph, andMinimal Graph.Treedoes nottake sharing or cycles into account.Graphcorrectly handles sharing and cycles bydisplaying a graph.Minimal Graphshows the smallest graph that is consistentwith the data.We give some examples.Consider the following two unifications:local X Y Z inf(X b)=f(a Y)f(Z a)=Z{Browse [X Y Z]}endThis shows the list [a b R14=f(R14 a)] in the browser, if the browser is setup to show theGraphrepresentation.The term R14=f(R14 a) is the textualrepresentation of a cyclic graph.The variable name R14 is introduced by thebrowser; different versions of Mozart might introduce different variable names.As a second example, feed the following unification when the browser is set upforGraph, as before:Copyright © 2001-3 by P.Van Roy and S.Haridi.All rights reserved. 2.7 Advanced topics 105declare X Y Z ina(X c(Z) Z)=a(b(Y) Y d(X)){Browse X#Y#Z}Now set up the browser for theMinimal Graphmode and display the term again.How do you explain the difference?Entailment and disentailment checks (the == and \= operations)The entailment check X==Y is a boolean function that tests whether X and Y areequal or not.The opposite check, X\=Y, is called a disentailment check.Bothchecks use essentially the same algorithm
[ Pobierz całość w formacie PDF ]