^FP^ ^index^

Towards a Denotational Semantics for
<A HREF="http://www.cs.monash.edu.au/~lloyd/tildeFP/LambdaLog"> LFP </A>
= Logic + Functional Programming, Coded in Lazy ML.

Technical Report 94/204

Lloyd Allison,
Department of Computer Science,
Monash University, Australia 3168.

September 1994

Keywords and Phrases: backtracking, denotational semantics, functional programming FP, lazy, Lazy ML, LML, logic programming LP, logic variable, non-determinism.



The typical logic language and functional language are superficially very different in syntax, but have many similarities from the points of view of theory and of usage. This report describes an executable denotational semantics of `LFP', a toy, lazy functional programming language to which have been added logic-variables and an extended list-comprehension with constraints. The semantics are coded in Lazy ML (LML) and can be executed. The semantics are simple and have certain limitations. As always, the exercise of writing such semantics reveals the bones of the language being defined, and the source of any difficulties, but not always the solutions. These semantics are a first step and will provide a basis for further experiments on LFP. It is assumed that the reader is familiar with LML (Augustsson and Johnsson, 1989) or a similar functional language.

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.

FP: Functional Programming / Lambda-Calculus.

This section describes the syntax and semantics of a toy, lazy functional language `FP'. It is a straightforward exercise and forms the basis of later discussions. The syntax FP is given below. It includes some syntactic sugar over and above the bare lambda-calculus to make it easier to write "real" programs. The main additions are local declarations, possibly recursive, and prefix and infix operators. The programmer specifies no types, and type checking is performed "dynamically" as an FP program is executed.

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 )


The next step is to extend the toy functional language to LFP = FP + logic-variables, including logic-variables and the ability to search for values of these logic-variables that satisfy boolean constraints. The following is a simple syntax for a `logic-expression':

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

eg. append nil (1::(2::nil)) is equal to (1::(2::nil)) etc.

Extended Semantics: LFP.

The denotational semantics of FP must be extended to take account of logic-variables. This is non-trivial because the value of a logic-variable is initially unknown, may become known during evaluation, and may change during evaluation if there are multiple solutions to a logic-expression.

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

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.)


The denotational semantics described above for FP and for LFP have both been implemented in Lazy ML. The semantics for LFP will execute simple logic + functional programs such as append-in-reverse:
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))

giving the required result:

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 )

gives the result:

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)))

gives the result:

where it should give the result:


A limitation of the semantics for LFP concerns nested logic-expressions. The nesting can be static or the dynamic result of function calls. The following example would ideally compute all prefixes of the list (1::(2::nil)), ie. (nil :: (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 denotational semantics for FP and for LFP have been coded in Lazy ML and can be executed. The complete programs can be found via URLs given below. Continuation-style parsers (Allison, 1988) for FP and LFP are included to complete the interpreters. The semantics for LFP have limitations and are a first step, a basis for further investigations of logic + functional programming.

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. Some applications of continuations, Comp. Jrnl. 31(1) 9-11 1988.

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