Lambda-Prolog differs from Prolog in three major ways:
x\(x+1), including unification of abstractions.
=>) and explicit quantification operators (
pimeaning "for all" and
sigmameaning "there exists").
x\ (x + 1) % the successor function; cf Haskell's \x -> (x + 1) a\b\ (a + b) % the make-adder function ((a\b\(a + b)) 1) % another version of the successor function ((a\b\(a + b)) 1 2) % answers 3
[1, 2, 3] (1 '.' 2 '.' 3 '.' ) % same thing, using explicit "cons" operator '.' % and nil ''; cf Haskell's 1:2:3:
kind product3 type -> type -> type -> type. % these will be type tuple3 A -> B -> C -> (product3 A B C). % explained later (tuple3 3 2.5 (x\(x+1))) % tuple of (int, float, (int -> int))
listis a type-function of one argument;
Value-functions are declared using
type is_two int -> o. is_two X :- X = 2. % returns true iff X is equal to 2.Named types and type-functions are declared using
kind int type. kind list type -> type.Thus Lambda-Prolog makes the notion of type-function explicit, paralleling that of value-function. However, type-functions can only take regular types as arguments, not other type-functions. This makes Lambda-Prolog's type system weaker than Sather's.
a\([a, a]) demonstrates a polymorphic
function: given a value of any type, it returns a list of that type.
As in Haskell, the types of polymorphic functions use variables to be
automatically filled in at point-of-call. Also like Haskell,
Lambda-Prolog can infer this polymorphic type automatically.
However, Lambda-Prolog provides no "partial-polymorphism" feature like Haskell's type-classes. Hence Lambda-Prolog does not support overloading. This has serious ramifications on naming, e.g.
+and assign with
$+and assign with
is_twoused a variable for its argument. If the definition were
is_two x :- x = 2.then this function is only defined on the symbol x, where it returns
false. Capitalization is really just syntactic sugar for a variable declaration, though Prolog does not allow variable declaration to be explicit.
Lambda-Prolog, however, can express variable declarations explicitly,
via lambdas and quantifiers. Since lambdas explicitly declare their
arguments, the names of their arguments need not be capitalized. For
example, we could define
pi x\ (is_two x :- x = 2).Which reads: "for all x, (is_two x) is true if x equals 2."
length :: [a] -> int length  = 0 length (h:t) = 1 + length t sign :: int -> int sign x | x < 0 = -1 sign x | x == 0 = 0 sign x | x > 0 = 1Prolog allows the same, and much more. In fact, Prolog's pattern matching mechanism subsumes conditionals and return values so completely that the latter features are not even offered in the language.
Prolog uses a bigger, brawnier form of pattern matching, called "unification", which is bidirectional. Unification tries to find the simplest variable binding, on either side, required to bring two expressions together. Examples:
|Expression||Unified with||Produces binding|
|2||X||X : 2|
|X||2||X : 2|
|[1,2,3]||[H|T]||H : 1, T : [2,3]|
|[1,2,1]||[X,Y,X]||X : 1, Y : 2|
|[X, 2]||[2, X]||X : 2|
|[X, 3]||[2, X]||fail|
[X,Y,Z] :- X = Z. It is helpful to interpret this as exactly equivalent to
length :: [a] -> Int -> Bool length  0 = True length (h:t) (y+1) | (length t y) = True -- n+k sugar, and a guard length _ _ = False -- catch-all sign :: Int -> Int -> Bool sign x (-1) | (x < 0) = True sign x 0 | (x == 0) = True sign x 1 | (x > 0) = True sign _ _ = FalseFor example,
length [1,2,3] 3returns
sign 1 (-1)returns
False. This is rather restrictive, since all predicates will let us do in Haskell is check a result, not generate one. But not so in Prolog.
Here are the same predicates, in Lambda-Prolog:
type length (list A) -> int -> o. % Bool is "o" length  0. % "= True" is automatic length [H|T] (Y+1) :- length T Y. % use ":-" for a guard % "[H|T]" instead of "(h:t)" % catch-all is automatic type sign int -> int -> o. sign X (-1) :- X < 0. sign X 0 :- X = 0. sign X 1 :- X > 0.Again,
length [1,2,3] 3returns
sign 1 (-1)returns
false. Note that the only significant syntactical difference is the implicit "
= True" after every line, and the implicit catch-all false. Because of this, the only functions we can define in Prolog are predicates. Seems rather limiting, indeed.
sign X 0 :- X = 0.As reasoned above, the guarded expression
X 0 :- X = 0is the same as
0 0. Unifying, say,
0 Zwith this expression will bind Z to 0, according to the rules given above. Thus the call
sign 0 Zwill bind Z to 0 in the caller. Similarly,
sign 4 Z % binds Z to 1 sign (-1) Z % binds Z to -1 length  Z % binds Z to 0 length  Z % binds Z to 0+1, i.e 1 length [1,2] Z % binds Z to 0+1+1, i.e. 2For example, here is what happens in the second-to-last case:
length  Zwith
length [H|T] (Y+1). Result is
H : 1, T : , Z : Y+1.
length T Y, i.e.
length  Y. This yields
Y : 0.
Y : 0and
Z : Y+1yields
Z : 0+1.
sign Z 1? It would appear that any positive integer could be returned for Z. However, if the guard were more complicated, like
f X, this would involve finding a Z for which f is true, which is impossible in general. So the answer is that Prolog knows how to solve some fs, like equality, but not others. Evaluating
sign Z 0will bind Z to 0 but
sign Z 1will fail.
A little kludgy and not very general, but it works. Variants of Prolog generally focus on this problem, by extending the range of fs the language can handle. For example, CLP can handle inequalities. However, these variants add no new syntax; they only give meaning to what were already syntactically well-formed expressions. The challenge in logic programming seems to be catching up with the syntax.
The tricky part here is "goes back". Bindings resulting from unification can be unwound. Side-effects, however, like writing to the screen, cannot. Thus Prolog, like Haskell, shuns side-effects, though for a different reason. In Prolog it is the only way to make backtracking sane. The only common "effects" in Prolog are variable bindings.
Logic languages thus use names in the style of placeholders, not
commands or tags (as defined in the linguistics lecture). A name is an
environment slot, which gets filled in by unification and emptied by
backtracking. Names are bound only by constraints, like "the number
X such that
sign X 0 is true". Names do not
denote exactly one thing, as would commands, nor can they be
re-assigned at will, as can tags.
Nondeterminism allows simple expression of generate-and-test algorithms. For example, placing 8 queens on a chessboard such that they are not attacking eachother. (This is a standard example in every Prolog text.)
sign Z 1. This is not because there are multiple solutions; we now know that Prolog can return multiple solutions. The reason is just that the particular interpreter used in Standard Prolog and Lambda-Prolog doesn't know how to handle inequalities.
type append (list A) -> (list A) -> (list A) -> o. append  X X. append [E|X] Y [E|Z] :- append X Y Z. append   Z. % binds Z to [1,2] append X  [1,2]. % binds X to  append X Y [1,2]. % three solutions: % X : , Y : [1,2] % X : , Y :  % X : [1,2], Y :  append  Y Z. % Z : [1|Y] (Y remains unbound) append X  Z. % infinite number of solutions: % X : , Z :  % X : [a], Z : [a,2] % X : [a,b], Z : [a,b,2] % etc.This unique feature stems from Prolog's use of predicates, which define relations, rather than functions.
However, as pointed out above, there is some confusion about when a function is multi-way, because some interpreters can do more than others. Since there is no indication from the syntax that a guard is unsolvable, it is easy to inadvertently write one-way functions.
|Expression||Unified with||Produces binding|
|x\x||x\(F x)||F : x\x|
|1||(F 1)||F : x\1 or x\x|
|z\z||z\(F (x\x) z)||F : s\x\x or s\x\(s x) or s\x\(s (s x)) or ...|
A => Bwe assume
Aand then prove
Aplays the role of a local declaration, in effect until
Here is another implementation of list append, using a local declaration:
% match is an auxiliary function which eats the longest common prefix % of X and Z type match (list A) -> (list A) -> o. match [E|X] [E|Z] :- match X Z. type append (list A) -> (list A) -> (list A) -> o. append X Y Z :- (match  Y => match X Z).The definition of
appendreads: "show that
match X Zis true, given that
match  Yis true." The result is that
matchwill eat the common prefix of X and Z, until X is exhausted. At that point, Y will be unified with the remainder of Z. It is not possible to make the declaration
match  Yglobal because Y is the argument to
It is also possible to put the entire definition of
match an "invisible"
helper function. That is,
type match (list A) -> (list A) -> o. match [E|X] [E|Z] :- match X Z. type append (list A) -> (list A) -> (list A) -> o. append X Y Z :- (pi \e\x\z(match [e|x] [e|z] :- match x z)) => (match  Y => match X Z).Now there are two local declarations:
pi \e\x\z(match [e|x] [e|z] :- match x z) match  YThe first is an explicitly quantified version of the previous global declaration. (Global declarations are implicitly quantified, local declarations are not.)
However, these declarations are not local in the sense of an Algol
block, because any predicate which is called will see that assertion.
That is, if
match called the global predicate
foo would be able to call
append exits and retracts the
local assertions. In this sense, the declarations are local, but
dynamically scoped. This gives up the encapsulation that would be
possible with true Algol blocks, as we will explore in the treasure hunt.
type two int. two = 2 type succ int -> int. succ = \x -> x + 1But Prolog only allows the definition of predicates. So to get the same effect we must use a one-argument predicate:
two 2. succ (x\(x+1)).To get the value of
succwe must bind it to a variable:
succ X, two Y, print (X Y). % prints 3This is neither comfortable nor readable. And since Lambda-Prolog has no type-predicates, we cannot use this mechanism to declare type synonyms:
type string type. % invalid predicate type string (list int). % Lambda-Prolog rejects this(In all fairness, Haskell can't declare type synonyms with '=' either; it needs a special
To get a local name, we can use implication to define a local one-argument predicate. But as we noted above, these predicates are dynamically scoped, so our name will be visible to callees.
However, while many tasks can be viewed as equation manipulation, such as expert systems and natural language processing, for others it is an unnatural fit. For example, we have even more of a rift between the language and its implementation than we had in Haskell. While the interpreter has extremely powerful mechanisms for unification and nondeterminism, neither of these are exposed in the language, so that they may be enhanced or applied to alternative uses. This is in addition to the tragedies of Haskell: no access to the type-graph or naming environments.
The non-generality of pure unification in Prolog shows through in the
additions required by Lambda-Prolog. General-purpose programming
requires a notion of function and local scope; this is evident just
from looking at the implementation of Prolog. But while imperative
languages have always had these features, logic languages rejected
them, out of ideology. We hope that this discussion demonstrated that
unification is not in opposition to functional programming,
but augments it. For example,
unify could just be a
function which returns a binding. Hence Prolog could have started as
an extension to Algol. Then functions and local scope would not have
to be re-invented. Thus is it partially exhilirating but partially
unfortunate that combining features from different ideologies
(e.g. object-oriented, functional, and logic programming) is a current