[ Pobierz całość w formacie PDF ]
.Currying is a higher-order programming techniquethat is explained in Section 3.6.6.Copyright © 2001-3 by P.Van Roy and S.Haridi.All rights reserved.100 Declarative Computation Modelstatement ::= expression ´=´ expression |.expression ::= expression ´==´ expression| expression ´\=´ expression |.binaryOp ::= ´=´ | ´==´ | ´\=´ |.Table 2.11: Equality (unification) and equality test (entailment check)function arguments are evaluated only if their result is needed.Haskell isa lazy functional language.13 Lazy evaluation is a powerful flow controltechnique in functional programming [87].It allows to program with po-tentially infinite data structures without giving explicit bounds.Section 4.5explains this in detail.An eager declarative program can evaluate functionsand then never use them, thus doing superfluous work.A lazy declarativeprogram, on the other hand, does the absolute minimum amount of workto get its result.2.7.2 Unification and entailmentIn Section 2.2 we have seen how to bind dataflow variables to partial valuesand to each other, using the equality (´=´) operation as shown in Table 2.11.In Section 2.3.5 we have seen how to compare values, using the equality test(´==´ and ´\=´) operations.So far, we have seen only the simple cases of theseoperations.Let us now examine the general cases.Binding a variable to a value is a special case of an operation called unification.The unification Term1 = Term2 makes the partial values Term1 and Term2equal, if possible, by adding zero or more bindings to the store.For example, f(XY)=f(1 2) does two bindings: X=1 and Y=2.If the two terms cannot be madeequal, then an exception is raised.Unification exists because of partial values; ifthere would be only complete values then it would have no meaning.Testing whether a variable is equal to a value is a special case of the entailmentcheck and disentailment check operations.The entailment check Term1 == Term2(and its opposite, the disentailment check Term1 \= Term2 ) is a two-argumentboolean function that blocks until it is known whether Term1 and Term2 areequal or not equal.14 Entailment and disentailment checks never do any binding.13To be precise, Haskell is a non-strict language.This is identical to laziness for most practicalpurposes.The difference is explained in Section 4.9.2.14The word  entailment comes from logic.It is a form of logical implication.This is becausethe equality Term1 == Term2 is true if the store, considered as a conjunction of equalities, logically implies Term1 == Term2.Copyright © 2001-3 by P.Van Roy and S.Haridi.All rights reserved.2.7 Advanced topics 101Unification (the = operation)A good way to conceptualize unification is as an operation that adds informationto the single-assignment store.The store is a set of dataflow variables, whereeach variable is either unbound or bound to some other store entity.The store sinformation is just the set of all its bindings.Doing a new binding, for exampleX=Y, will add the information that X and Y are equal.If X and Y are alreadybound when doing X=Y, then some other bindings may be added to the store.Forexample, if the store already has X=foo(A)and Y=foo(25), then doing X=Y willbind A to 25.Unification is a kind of  compiler that is given new informationand  compiles it into the store , taking account the bindings that are alreadythere.To understand how this works, let us look at some possibilities." The simplest cases are bindings to values, e.g.,X=person(name:X1 age:X2),and variable-variable bindings, e.g., X=Y.IfXandYare unbound, then theseoperations each add one binding to the store." Unification is symmetric.For example,person(name:X1 age:X2)=Xmeansthe same as X=person(name:X1 age:X2)." Any two partial values can be unified.For example, unifying the tworecords:person(name:X1 age:X2)person(name:"George" age:25)This binds X1 to "George" and X2 to 25." If the partial values are already equal, then unification does nothing.Forexample, unifying X and Y where the store contains the two records:X=person(name:"George" age:25)Y=person(name:"George" age:25)This does nothing." 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, [ Pobierz caÅ‚ość w formacie PDF ]