Lambda Module Users' Manual

Purpose

This document provides information on using the predicates exported from the lambda module. It assumes the user has a strong grasp of Prolog logic programming, and, as this users' manual is not an introduction to functional programming and the lambda calculus, it will not dwell on introductory material of either.

The lambda calculus has two simple concepts: lambda-abstraction (where a variable is declared) and application (where one lambda-term is applied to another). As has been demonstrated elsewhere, the lambda calculus is Turing-equivalent: any computable value can be expressed by a lambda expression, including such fundamental concepts as Number, numbers, arithmetic and logic.¹ In fact, pure lambda calculus only has lambda-terms and application (as everything else is derivative), but we are not so dogmatic with this module: here, a lambda-term is a prolog term (lambda/2) where the first argument is the variable declared and the second argument is its applicative use.

Considered practically, the Lambda module is used to construct "functionals": anonymous functions of any arity that return a value of any type (indeed, it is possible for functionals to return other functionals). As the functional programming community has concentrated its research on program transformation, and programs in the functional style are usually lists, lambda-terms shine when assigned to list-processing tasks. In that light, the two most commonly used higher-order functions are map (that transforms a list of elements of type T0 to a list of the same cardinality with elements of type T1) and fold (that transforms ("folds") a list into some accumulated result (the easiest fold implementation is 'sum')).³

:- module(lamdba)

Exported Predicates

The lambda module exports the following predicates:

apply/3
test/2

Exported Operators

This module does not export any operators.

apply/3

Synopsis: apply(+Lambda, +Argument, -Result)

Arguments:

Lambda

<term>

a term of the form lambda(?Var, +Expression),

where:

?Var	<variable>	A variable
+Expression	<term>	A term, normally containing 'Var',⁴ that can be evaluated to a result

Argument

<term>

The term substituted for 'Var' in 'Expression'

Result

<term>

The value returned from evaluating 'Expression'

Description:

Temporarily binds 'Argument' to 'Var' and evaluates 'Expression' to obtain 'Result'.

N.B.:
Since, in practice, lambda-terms are used more than once, binding 'Var' outside of the lambda-term is incorrect. Hence, the modality of 'Var' after calling apply/3 is the same as its modality before apply/3 was called. Or, simply, if 'Var' is unbound before apply/3, it remains unbound after the call.

Backtracking:

As for any called goal.

Examples:

A trivial example is as follows ...

inc --> apply(lambda(X, X + 1)).

... where inc/2 gives an output argument that is the successor to the input argument:

?- inc(3, X), X > 3.

 X = 3+1

After all the above description, however, it turns out that the lambda calculus is only used by the combinatory logic module to translate lambda-terms into equivalent combinators:

phi_equivalent(lambda(X, Function), phi(Y, Z, Apply)) :-
  Apply = lambda:apply(lambda(X, Function), Y, Z).

Here we take a lambda application and translate it to an equivalent phi-term.

test/2

Synopsis:

test(+LambdaPredicate, +Argument)

Arguments:

LambdaPredicate

<term>

a binary-typed lambda term of one of the following forms:

predicate(?Var, +Goal); or
complement(?Var, +Goal)

where:

Var	<variable>	A variable
Goal	<goal>	A (Prolog) goal, normally containing 'Var'⁴

Argument

<term>

The term substituted for 'Var' in 'Goal'

Truth tables:

For LambdaTerm = predicate(?Var, +Goal):

Goal

true fail

true fail

For LambdaTerm = complement(?Var, +Goal):

Goal

true fail

fail true

Description:

Accepts a typed lambda term (of one of the two types enumerated above), and runs 'Goal' to obtain a proof. Basically, test/2 exists to allow one to defer execution of a goal, so that, e.g., one could build a goal over several predicates and from run-time data and lambda expressions.

N.B.:
As for apply/3, lambda variables change their modality only within the lexical scope of the lambda expression. Free variables entering test/2 return to an unbound state after test/2 completes, even if they are temporarily bound within the context of proving test/2.

Backtracking:

standard

Examples:

Using the definition of inc/2 above, the following examples demonstrate test/2.

?- test(predicate(X, (user:inc(X, Y), Y > X)), 5).

 X = _7030,
 Y = _7076

Here, 5 replaces X, giving Y to be 6, which is true for Y > X (6 is, after all, greater than 7).

?- test(complement(X, (user:inc(X, Y), Y > X)), 5).

 no

The same bindings occur, but since this is a complement/2 term, the goal should fail for the test to succeed. As the goal is provable, test/2 fails.

Further Study

The below are reading materials that discuss the lambda calculus in greater depth.

Church, A., The Calculi of Lambda Conversion, Princeton University Press, Princeton, N.J., 1941.⁵ Nicely summerized in http://en.wikipedia.org/wiki/Lambda_calculus
The Über Lambda papers by Guy Steele provide a serial introduction to the lambda calculus -- starting from fundamentals and going all the way, in opposite directions, a) from lambda-terms as logic predicates to b) implementing machine code as lambda-terms; http://library.readscheme.org/page1.html. These papers are, as a set, a wonderful, exciting read -- Both Guy and Paul Graham (his introductory ANSI Common Lisp (1996) and his much better (he really warms up to the topic and tears into it with gusto) On Lisp: Advanced Techniques for Common Lisp (1994) both published by Prentice Hall) really know how to grab and to keep your attention!
For books, the best introduction on the lambda calculus that starts with (*sigh*) factorial and goes all the way to any problem one wishes to solve is, of course, The Structure and Interpretation of Computer Programs (2nd ed), Harold Abelson, Gerald Jay Sussman with Julie Sussman, MIT Press, MA, 1996.
But, seriously, I have a life, and so do you, so something a little less serious, and a little less massive: Let's Talk LISP, Laurent Siklóssy, Prentice Hall, NJ, 1976. Really, I don't understand why this book hasn't received wider attention -- it's one of my top-ten, giving each topic a light treatment and lacing the work with a sublime delight.
Lisp, Lore, and Logic: an Algebraic View of LISP Programming, Foundations, and Applications, W. Richard Stark, Springer-Verlag, NY, 1990, if the historical perspective and consilience tickle your fancy.
and, so what does one do with the Lambda Calculus (besides superceding it with Combinatory Logic, but that's for a different module to discuss)? Algorithms: a Functional Programming Approach, Fethi Rabhi, Guy Lapalme, Addison-Wesley, MA, 1999, first, and, more in detail, An Introduction to Functional Programming Using Haskell , A. J. T. Davie, Cambridge Computer Science Texts, UK, 1992, map out interesting things one can do with the lambda calculus, particularly with normal order (lazy) evaluation, such as infinite lists (very useful, by the way), searching, sorting, backtracking, pattern-matching, map-colouring, etc.
... or a web search on "Lambda Calculus" will get you plenty of introductory, derivative, material to review.

Endnotes

¹	It is a rather ironic observation that, although the formulation of the Turing machine demonstrated that one could construct a computer and write programs for it, it is very rare, indeed, that a programming language is based on a Turing machine. Instead, with very few exceptions (Prolog being a notable one) the lambda calculus is the basis of the syntax and semantics of most programming languages. A software engineer's education does not reflect this: an educated software engineer² has relatively little understanding of the lambda calculus but can discuss Turing machines, including the input/output instructions on the tape, at length.
²	An "educated software engineer" may be oxymoronic for more than one reason; but these kind of debates lead to discuss points that hold no interest for me.
³	Neither map nor fold are covered here, as they are list-processing functions, not functions that transform lambda-terms themselves.
⁴	In the pure lambda calculus (the Lambda-I calculus), 'Expression' or 'Goal' must contain 'Var'. The "impure" variant (the Lambda-K calculus) allows for 'Var' to be absent from 'Expression' or 'Goal'. Purists demand fidelity to the Lambda-I calculus; pragmatists use the Lambda-K calculus, and then there are the wishy-washy lot who use Lambda-K all the time but wish they were using Lambda-I instead (the author falls into this group). This debate is brought into light-hearted focus in [Smu1985], pp. 120, 179-181.As for this module, the user may choose either calculus, as a lambda term is not verified to be pure in any way by this module.
⁵	I find it delightful that in his preface to a related work ("A Set of Postualtes for the Foundation of Logic," Alonzo Church, Annals of Mathematics, ser. 2, vol. 33, 1933), he limits his paper to avoid "the paradoxes connected with the mathematics of the transfinite". A friend published a book on transfinite numbers using set-theory to describe them (Fractals and Hyperspaces, Keith R. Wicks, Lecture Notes in Mathematics #1492, Springer-Verlag, Germany, 1991).

Works Consulted

[Smu1985]

To Mock a Mockingbird and Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic, Raymond Smullyan, Alfred A. Knopf, NY, 1985.

author:	Douglas M. Auclair (dauclair at hotmail dot com)
created:	August 21, 2005
Copyright © 2005, Cotillion Group, Inc. All rights reserved.