Contents:
The motivation for the design of LFP is that while Prolog is very useful for search problems, the largest part of the typical (logic-)program is nevertheless deterministic. Hence the default in LFP is for the deterministic execution of functional programs with an extended list-comprehension available for the programmer who wishes to "contract-in" to a non-deterministic or backtracking search.
Many people have worked on combining logic-programming and functional programming, to the extent that Bellia and Levy could survey the matter in 1986. LFP resembles the languages discussed by Darlington et al (1985, 1992) and Cheng and Yun-Zheng (1992). Jagadeesan et al (1992) have given abstract semantics for functional programming with logic-variables. Reddy (1985) gave operational semantics. Paulson and Smith (1989) have also examined the logic + functional programming area. This long effort demonstrates the importance and the difficulty of the exercise.
Exp ::= Ide | Num | Boolean | nil |
lambda Ide.Exp | -- abstraction
let [rec] Dec in Exp | -- declarations
Exp Exp | -- application
(Exp) |
if Exp then Exp else Exp | -- conditional
UnOpr Exp | -- unary oprs
Exp BinOpr Exp -- binary operators
Dec ::= Ide=Exp | Dec, Dec
UnOpr ::= + | - | not | hd | tl | null
BinOpr ::= + | - | * | / |
= | <> | < | <= | > | >= |
and | or |
:: -- cons
The semantic types - values `Val' and environments `Env' - are given next. In this exercise Val consists of integers, Booleans, lists and functions. A `Wrong' value is also included for error conditions. An environment `rho:Env' maps identifiers onto their values. The initial environment `rho0' is empty - no identifiers are declared.
let rec
type Val = IntVal Int + -- Int
BoolVal Bool + -- Bool
ListVal Val Val + NilVal + -- Lists
FnVal (Val -> Val) + -- abstraction
Wrong String -- error
and type Env == Ide -> Val -- rho :Env, maps names to their values
and rho0 x = Wrong("undeclared: " @ x) -- empty, initial environment
Note that a function-value `FnVal' is a mapping, an LML function, from values (parameters) to values (results), Val->Val. Strictly speaking, if f:Val->Val and fv=(FnVal f) then fv:Val, giving f and fv different LML types. However I often take the liberty of "confusing" f with fv in what follows and call them both values.
An `update' function is useful to modify existing functions (really to create new, modified functions), particularly environments.
and update f x v y = if x=y then v else f y
The semantics of expressions are defined by `E'. E is defined "by cases", running through the syntactic options for expressions - identifiers, numbers, and so on.
in let rec
-- E : Exp -> Env -> Val
E (Ident x) rho = rho x ||
E (Num n) _ = IntVal n ||
E (Boolean b) _ = BoolVal b ||
E NIL _ = NilVal ||
E (Block isRec Local Body) rho = E Body (D isRec Local rho) ||
E (Apply Fn Actual) rho = let FnVal f = E Fn rho in f (E Actual rho) ||
E (LambdaExp x Body) rho = let f v = E Body (update rho x v) in FnVal f ||
E (IfExp Se Te Fe) rho =
E (case E Se rho in BoolVal true: Te || BoolVal false: Fe end) rho ||
E (UExp Opr Argh) rho = U Opr (E Argh rho) ||
E (BExp Opr A1 A2) rho = B Opr (E A1 rho) (E A2 rho)
For example, the meaning of a conditional expression `IfExp', given an environment rho, is either the meaning of the true branch `Te', or of the false branch `Fe', depending as the switch `Se' evaluates to true or false. These semantics form a lazy interpreter for FP because LML itself is lazy. The semantics do no explicit type checking; for example they rely on LML to catch the error if Se should not evaluate to a Boolean.
The semantics of declarations, `Dec', are given by `D' and `DD'.
-- D : Bool -> Dec -> Env -> Env
and D isRec L oldRho =
let rec
newRho = DD L (if isRec then newRho else oldRho) oldRho
and DD (Decs d1 ds) useRho grow = DD d1 useRho (DD ds useRho grow) ||
DD (Bind x e) useRho grow = update grow x (E e useRho)
in newRho
DD makes an updated environment containing new names, such as `x'. Note that the right-hand sides of recursive (isRec) declarations refer to the new environment being defined, and that non-recursive declarations refer to the old environment. There is a close similarity between the binding of names in declarations and parameter passing, as is to be expected.
Unary operators are defined by `U' which is straightforward.
and U plusSy (IntVal n) = IntVal n ||
U minusSy (IntVal n) = IntVal (-n) ||
U notSy (BoolVal b) = BoolVal (~b) ||
U nullSy (ListVal _ _) = BoolVal false ||
U nullSy NilVal = BoolVal true ||
U hdSy (ListVal h t) = h ||
U tlSy (ListVal h t) = t
Binary operators are defined by `B'.
and B consSy h t = ListVal h t ||
B opr (IntVal m) (IntVal n) =
case opr in plusSy : IntVal( m+n ) ||
minusSy : IntVal( m-n ) ||
timesSy : IntVal( m*n ) ||
divSy : IntVal( m%n ) ||
eqSy : BoolVal( m = n) ||
neSy : BoolVal( m ~= n )||
leSy : BoolVal( m <= n )||
ltSy : BoolVal( m < n ) ||
geSy : BoolVal( m >= n )||
gtSy : BoolVal( m > n )
end ||
B opr (BoolVal p) (BoolVal q) =
case opr in orSy : BoolVal( p|q ) ||
andSy : BoolVal( p & q )
end
Exp ::= list Ide st Exp | ... plus as before ...
The expression declares an identifier to be a logic-variable. The keyword `st' stands for `such that'. The idea is to extend the list-comprehensions found in languages such as LML to include logic-variables; see Darlington et al (1985). The logic-expression returns a list of solutions. There might be zero, one, two, several or infinitely many solutions for the identifier that make the constraint expression true. The restriction to a single logic-variable is in the interests of simplicity and is no real limitation because the variable can become bound to structures containing multiple variables. Further, each result can be incorporated in an expression if the well known `map' function is applied to the result list.
An example of a logic-expression is -
list lv st ListEq (append (hd lv) (tl lv))
(1 :: (2 :: nil))
The aim of the example is to find all pairs `lv' such that the result of appending the first element of the pair `hd lv' and the second element `tl lv' is equal to the list `(1::(2::nil))'. The result should be the list of three pairs:
(( nil :: (1::(2::nil)) ) :: -- solution 1 ( (1::nil) :: (2::nil) ) :: -- solution 2 ( (1::(2::nil)) :: nil ) :: -- solution 3 nil)
eg. append nil (1::(2::nil)) is equal to (1::(2::nil)) etc.
Informally, the idea is to try to evaluate the constraint in the logic-expression. If it evaluates to true then the logic-variable is evaluated to give one solution. If the constraint is false there is no solution - for that path of evaluation. However, an unground logic-variable may be encountered during the evaluation of the constraint. Suppose it is a list logic-variable, appearing in the expression null(L), say. A list can either be `nil' or `H::T' for some H and T. The approach is to try two paths of evaluation - one with L bound to nil and the other with L bound to H::T. Each path may give zero or more solutions and the results are appended to form the complete list of solutions.
The discussion above implies that the meaning of an expression can no longer just be of type Env->Val but must also depend on something, say a `Store', that gives values to logic-variables. A logic-variable is modelled by an address or location, `Locn' - 1, 2, 3, .... A free-location counter is needed to control the allocation of locations. A computational `State' consists of a pair - a free location counter and a store. Now, an unground variable can be encountered in the middle of evaluating an expression and at that point new paths of evaluation can be formed. In other words, the logic-variable's `kontinuation' can be invoked more than once with slightly different stores. This leads us to a continuation-semantics. (Continuations are also used in combinatorial search problems - Wadler (1985), Allison (1990).) The term `Kont' or kontinuation is used for expression-continuations, as is traditional in denotational semantics (Milne and Strachey, 1976). A kontinuation `k' takes a value and a state and produces the final answer or value of the program.
let rec
type Val = IntVal Int + -- Int
BoolVal Bool + -- Bool
ListVal Val Val + NilVal + -- Lists
FnVal (Val->Kont->State->Val) + -- Abstractions
Thunk (Kont->State->Val) + -- params, bindings
LogicVar Locn + -- see Store
unground + -- unground LogicVar's value
Wrong String -- error
and type Env == Ide -> Val -- rho :Env, maps Identifiers to their values
and rho0 x = Wrong("undeclared: " @ x) -- empty, initial environment
and type Locn == Int -- "addresses" of logic variables
and type Store == Locn -> Val -- gives Vals of logic vars if known
and s0 addr = unground
and type State = st Locn Store -- freeCounter # Store
and st0 = st 0 s0
and type Kont == Val -> State -> Val -- Expression Kontinuations
and k0 = Copy 0
Note that a function-value takes a value (parameter), a kontinuation (return address) and a state to produce an answer. Thunks are used for parameters and for values bound in declarations; their use preserves laziness in LFP.
Deref and copy are two useful functions. Deref finds the value of a logic-variable if it is ground to a value, and also puts the value of a thunk in weak-head normal form. It is applied to the parameters of strict operators.
and deref (LogicVar n) k (st f s) =
let v = s n
in case v in unground : k (LogicVar n) (st f s) ||
LogicVar m: deref (LogicVar m) k (st f s) ||
v : deref v k (st f s)
end ||
deref (Thunk t) k s = let k2 v = deref v k in t k2 s ||
deref v k s = k v s
Copy replaces instances of (local) logic-variables in a value with their values. It is applied to the results of logic-expressions to enforce the scope rules on logic-variables.
and Copy f (LogicVar n) s =
let k (LogicVar n) s & (n>=f) = unground || -- a "local" unground one
k (LogicVar n) s = LogicVar n || -- non-local unground
k v s = Copy f v s -- ground to v
in deref (LogicVar n) k s ||
Copy f (ListVal h t) s = ListVal (Copy f h s) (Copy f t s) ||
Copy f (Thunk t) s = t (Copy f) s ||
Copy f v _ = v
and append NilVal L = L ||
append (ListVal h t) L = ListVal h (append t L)
and update f x v y = if x=y then v else f y -- esp' f is Store or Env
The meanings of expressions are given by a very much changed `E'. E takes an expression, an environment to give values to identifiers, a kontinuation which uses the value of the expression, and a state for logic-variables, and returns a value. For example, the meaning of a number n, given an environment rho, a kontinuation k (the rest of the program) and a state s, is to pass n and s to k.
in let rec
-- E : Exp -> Env -> Kont -> State -> Val
E (Ident x) rho k s = deref (rho x) k s ||
E (Num n) _ k s = k(IntVal n) s ||
E (Boolean b) _ k s = k(BoolVal b) s ||
E NIL _ k s = k(NilVal) s ||
The meaning of a logic-expression given rho, k and s, is to evaluate the constraint `C' with rho and a new kontinuation `k2'. K2 expects a boolean value as the result of C. If this value is true, k2 evaluates the logic-variable `x' in the current state and puts the resulting value `v' in the solution list, except that Copy is applied to v to remove any local logic-variables as their scope is limited to the logic-expression. If the boolean is false the solution list is `nil' - no solution. Whatever the solution list, it is passed to the logic-expression's continuation k. These semantics imply that the only result or effect of a logic-expression is to return solution values for its logic-variable. This is a limitation and its consequences are discussed later, but meanwhile note that the state `st3' below is not given to k.
E (LogicExp x C) rho k (st f s) = -- list of x s.t. constraint C
let rho2 = update rho x (LogicVar f)
and st2 = st (f+1) s
in let k2 (BoolVal b) st3 =
if b then
let k3 v s = ListVal (Copy f v st3) NilVal
in E (Ident x) rho2 k3 st3 -- one soln
else NilVal -- no solution
in k( E C rho2 k2 st2 ) (st f s) ||
The remaining cases for `E' follow the traditional continuation-semantics style straightforwardly.
E (Block isRec Local Body) rho k s = E Body (D isRec Local rho) k s ||
E (Apply Fn Actual) rho k s =
let k2 (FnVal f) s = f (Thunk(E Actual rho)) k s in E Fn rho k2 s ||
E (LambdaExp x Body) rho k s =
let f v = E Body (update rho x v) in k (FnVal f) s ||
E (IfExp Se Te Fe) rho k s =
let k2 (BoolVal b) = E (if b then Te else Fe) rho k
in E Se rho k2 s ||
E (UExp Opr Argh) rho k s =
let k2 v = let k3 v = U Opr v k
in deref v k3
in E Argh rho k2 s ||
E (BExp consSy A1 A2) rho k s =
B consSy (Thunk(E A1 rho)) (Thunk(E A2 rho)) k s || -- cons lazy
E (BExp Opr A1 A2) rho k s =
let k1 v1 =
let k1b v1 =
let k2 v2 =
let k2b v2 = B Opr v1 v2 k
in deref v2 k2b
in E A2 rho k2
in deref v1 k1b
in E A1 rho k1 s
For example, to evaluate a conditional expression, evaluate the switch expression `Se' with a kontinuation `k2' that uses the switch's result to evaluate either the true of false path.
The semantics above do not perform short-cut evaluation of the binary operators `and' and `or' but this could be done trivially.
The previous treatment of declarations can be used almost without change, perhaps surprisingly.
-- D : Bool -> Dec -> Env -> Env
and D isRec L oldRho =
let rec
newRho = DD L (if isRec then newRho else oldRho) oldRho
and DD (Decs d1 ds) useRho grow = DD d1 useRho (DD ds useRho grow) ||
DD (Bind x e) useRho grow =
let eVal = Thunk(E e useRho)
in update grow x eVal
in newRho
Unary operators are defined by a much changed `U'. The function `setHT' is used later in connection with list logic-variables.
and setHT n (st f s) = -- bind H::T to n where H, T new logic vars
let H=LogicVar f and T=LogicVar(f+1) -- new Locns
in st (f+2) (update s n (ListVal H T)) -- n := H::T
and U plusSy (IntVal n) k s = k(IntVal n) s ||
U minusSy (IntVal n) k s = k(IntVal (-n)) s ||
U notSy (BoolVal b) k s = k(BoolVal (~b)) s ||
U nullSy (ListVal _ _) k s = k(BoolVal false) s ||
U nullSy NilVal k s = k(BoolVal true) s ||
The most significant addition is in the treatment of logic-variables (below). At these points two evaluation paths may be spawned, for example one with a list logic-variable bound to `nil' and one with it bound to `H::T' where H and T are two new logic-variables. This ordering gives an initial preference to short lists. The results from both paths are appended together. (Given these semantics, the result-values are appended but the state from one path does not affect the other path; see the discussion later.)
U nullSy (LogicVar n) k (st f s) =
append (k (BoolVal true) (st f (update s n NilVal))) -- nil or ...
(k (BoolVal false) (setHT n (st f s))) || -- ... not nil
An interesting question concerns the operators `hd' and `tl' applied to an unground logic-variable. The best decision seems to be to bind the variable to `H::T' as the only other choice `nil' would lead to an error.
U hdSy (ListVal h t) k s = k h s ||
U tlSy (ListVal h t) k s = k t s ||
U hdSy (LogicVar n) k (st f s) = k (LogicVar f) (setHT n (st f s)) ||
U tlSy (LogicVar n) k (st f s) = k (LogicVar (f+1)) (setHT n (st f s))
Binary operators are defined by `B'. The most significant case defines equality `='. (Relational operators in FP and LFP apply only to scalar values.) An unground logic-variable `n' being compared for equality with any value `v' can be bound to v in the store and the value `true', together with the updated store, passed to the kontinuation k. An addition, the value `false' can be passed on a second evaluation path and all results appended together.
Strictly speaking an extra constraint, that the logic-variable must now be not-equal to v, should be propagated forward on the second path and tested when more information about n comes to hand. This constraint could be associated with the variable in the store, eg. as a parameter of the `unground' constructor, but this has not been implemented. This is a special case of negation, which is a special case of inequality, which does not cover logic-variables fully in these semantics. To do the job properly requires a general constraint solver which it could be argued is orthogonal to these semantics.
and B eqSy (LogicVar n) v k (st f s) = -- Unification
append (k(BoolVal true )(st f (update s n v)))
(k(BoolVal false)(st f s)) ||
B eqSy v (LogicVar n) k s = B eqSy (LogicVar n) v k s || -- switch
The other cases of B are easily converted into the continuation-style, although noting the above inadequacy with respect to inequalities.
B consSy h t k s = k (ListVal h t) s ||
B opr (IntVal m) (IntVal n) k s =
case opr in plusSy : k(IntVal( m+n )) s ||
minusSy : k(IntVal( m-n )) s ||
timesSy : k(IntVal( m*n )) s ||
divSy : k(IntVal( m%n )) s ||
eqSy : k(BoolVal( m = n)) s ||
neSy : k(BoolVal( m ~= n)) s ||
leSy : k(BoolVal( m <= n )) s||
ltSy : k(BoolVal( m < n )) s ||
geSy : k(BoolVal( m >= n )) s||
gtSy : k(BoolVal( m > n )) s
end ||
B opr (BoolVal p) (BoolVal q) k s =
case opr in orSy : k(BoolVal( p|q )) s ||
andSy : k(BoolVal( p & q )) s
end
A further omission in the above semantics concerns Boolean logic-variables. The natural solution is to append the results from two evaluation paths, with the logic-variable `b' bound to true and to false respectively. There is no succinct way to determine that the logic-variable is Boolean as the semantics stand, except by running through all the special cases such as `not b' etc.. A solution is to make type-information available to the semantics. This could be done either by adding type information to the LFP language or by making `E' pass the required type of the expression value through the chain of recursive calls. Note that the type of list variables is invariable implied in the way in which they are used - `null l', `hd l' or `tl l'. As it stands, the LFP programmer can get around the omission by the cludge of programming `b=true' instead of `b'. Numerical logic-variables should be handled by a solver; at present only equality is defined. (They could be implemented as lists of digits but this is hardly practical.)
let rec
append = lambda a. lambda b.
if null a then b
else (hd a) :: (append (tl a) b),
ListEq = lambda x. lambda y.
if null x then null y
else if null y then false
else (hd x = hd y) and (ListEq tl x tl y)
in list lv st ListEq (append (hd lv) (tl lv))
(1 :: (2 :: nil))
((Nil::(1::(2::Nil)))::(((1::Nil)::(2::Nil))::(((1::(2::Nil))::Nil)::Nil)))
It may be that the constraint does not fully determine the values of the logic-variable, in which case the result may not be completely ground:
let rec length =
lambda x. if null x then 0 else 1+length(tl x)
in hd( list x st 2 = length x )
(unground::(unground::Nil))
Note that any attempt to compute with the tail of the logic-expression above will result in an infinite loop.
The inadequate treatment of negation sometimes leads to too many solutions being produced, for example:
let rec member = lambda e. lambda l. if null l then false else if e = hd l then true else member e tl l in list x st member x (1::(2::(1::nil)))
(1::(2::(1::Nil)))
(1::(2::nil))
list x st not null(list y st ListEq (append x y) (1::(2::nil)))
It can be read as, find all x such that there exists at least one y such that append x y is equal to (1::(2::nil)). Under the present semantics the solution `unground' is returned which is poor although technically it is not incorrect. The example is a special case of the general form:
list x st P(list y st Q(x,y))
The problem is that the inner logic-expression
grounds the outer logic variable `x'.
To define this correctly, the state(s) that result from the
inner logic-expression must be passed back to the outer
logic-expression instead of being discarded as
noted previously -
the result of a logic-expression must include the side-effect
of grounding (outer) logic-variables as well as the solution list.
Further, the inner logic-expression could have several,
even infinitely many, solutions for `y' for each x.
The values of y are dependent on the value of x.
This means that the state must also be "threaded" through
all evaluation paths of a logic-expression.
In this way all paths could use x's current value and indeed
several paths could contribute parts of the value.
This could perhaps be accomplished by modifying the semantics
of logic-expressions and the clauses for logic-variables.
However it seems to conflict with the desire to have
lazy-evaluation of solution lists:
If a logic-expression has infinitely many solutions
then a final state will never be determined,
yet a single solution alone is sufficient to show
not null(list y st ...).
Lazy-evaluation of solution lists is also desirable because many
useful queries have infinitely many solutions and others
lead to non-terminating computations if an attempt is made to
evaluate all solutions.
As a further example, the following program should give the empty solution list:
list x st not null(x) and
not null(list y st ListEq (append x y) (1::(2::nil))) and
not null(list z st ListEq (append x z) (2::(2::nil)))
The current semantics give an incorrect answer here. The logic-expression for `y' grounds `x' to (1::nil), say, which would prevent any solution being found for `z' - if the state were a part of the result of logic-expressions.
In summary, the semantics presented only give the correct results for LFP programs in general if each logic-expression grounds only its own local logic-variable; it may "read" other logic-variables but not ground them.
The LFP semantics above give a cursory treatment of negation and inequations. However just as there is a range of logic-programming systems: negation by failure (the original Prolog), delay of negation (eg. MuProlog, L. Naish, 1983), constraint logic-programming (eg. CLP(R), J. Jaffar et al, 1992), so there must be a corresponding range of treatments of negation in logic + functional programming. The denotational semantics make it clear where a generalised solver should be included.
The semantics also limit a logic-expression to grounding its own "local" logic-variable although it may use other ones.
L. Allison. Continuations implement generators and streams, Comp. Jrnl. 33(5) 460-465 1990.
L. Augustsson and T. Johnsson. The Chalmers lazy-ML compiler, Comp. Jrnl. 32(2) 127-141 1989.
M. Bellia and G. Levi. The relation between logic and functional languages: a survey, Jrnl. of Logic Programming 3 217-236 1986.
G. Cheng and Z. Yun-Zheng. A functional + logic programming language in interpretation-compilation implementation, Jrnl. of Lisp and Symbolic Computing 5(3) 133-156 1992.
J. Darlington, A. J. Field and H. Pull. The unification of functional and logic languages, in Logic Programming: Functions, Relations and Equations, D. DeGroot and G. Lindstrom (eds), 37-70, Prentice Hall 1985.
J. Darlington, Yi-ke Guo and H. Pull. A new perspective on integrating functional and logic languages, Dept. of Computing, Imperial College, London, 1992.
J. Jaffar, S. Michaylov, P. J. Stuckey and R. H. C. Yap. The CLP(R) language and system, TOPLAS 14(3) 1992.
R. Jagadeesan, P. Panangaden and K. K. Pingali. A fully abstract semantics for a functional language with logic variables, Proc. 4th IEEE Symp. on Logic in Computer Science 294-303 1989.
R. Milne and C. Strachey. A Theory of Programming Language Semantics (2 vols). Chapman and Hall 1976.
L. Naish. Mu-Prolog 3.0 reference manual, Dept. of Computer Science, University of Melbourne, 1983.
L. C. Paulson and A. W. Smith. Logic programming, functional programming and inductive definitions, in Extensions of Logic Programming, P. Schroeder-Heister (ed), Springer-Verlag LNCS 475 283-309 1989.
U. Reddy. Narrowing as the operational semantics of functional languages, Proc IEEE Logic Programming Conf. 138-151 1985.
P. Wadler.
How to replace failure by a list of successes,
Functional Programming Languages and Computer Architecture,
Springer-Verlag LNCS 201 113-128 1985.
Present address: DCS Glasgow ('94)
L. Allison, A Functional Programming Page, URL=http://www.cs.monash.edu.au/~lloyd/tildeFP/, Monash University 1994.
L. Allison, A Logic Programming Page, URL=http://www.cs.monash.edu.au/~lloyd/tildeLogic/, Monash University 1994.
NB. URL=http://www.csse.monash.edu.au/~lloyd/tildeFP/ etc. after 2000.
Created with "vi (RIX)", charset=iso-8859-1