In Clojure We Trust

A piece of intertube about the Clojure programming language, algorithms and Emacs.

Lambda Calculus, a Suprisingly Powerful Language

I’m reading the book Types and Programming Languages from Benjamin C. Pierce from time to time at the moment. The chapter explaining the untyped lambda calculus gave me more than one occasion to pause and think. The lambda calculus, invented in the 30s, is a formal system for expressing computation with functions and can also been seen as a programming language. A very simple one, yet a surprisingly very powerful one. A language where all computations are done with functions, thus the first functional programming language in the history of mankind. It plays an important role in the field of research but also as a theoretical foundation for implementing functional languages such as Haskell, OCaml, Scheme, Clojure etc.

The lambda calculus is composed of three elements (or in programming language theory jargon, of three terms):

  • variables, of the form x
  • abstractions, of the form λx.t
  • applications, of the form t s

An abstraction can almost be seen like a function in “classic” programming languages. An application “applies” its arguments to an abstraction. There is nothing more. There are no booleans, numbers, strings, conditional statements etc. Functions accept only one argument. Yet, everything can be computed with the lambda calculus.

A variable x is bound if it occurs in the abstraction of the body t of an abstraction λx.t. It is is free if it appears if it is not bound by an enclosing abstraction on x. For example in (λx.x) x the first x is bound, the second one is free. A term with no free variables is called a combinator. 1

The simplest combinator is the identity function. It returns its argument unchanged:

id = λx. x

There are different strategies when choosing on how arguments are evaluated before applying them to functions. That is, there are different strategies to reduce the terms. The most common one is call-by-value. Under this strategy a function can be applied only when its right-hand side has been reduce to a value. A value is a term that cannot be further reduced.

Thus (λx.x x) (λx.x) y reduces to (λx.x) (λx.x) y in the first evaluation step then to (λx.x) y then to y. Functions with multiple arguments can be simulated by having a function returning another function: λx.λy.x y, for example. This is familiar to functional programmers as currying.

What really impress me is that every computation are possible with such a simple language. I will give a few examples from the book, some are answers from exercises, so I you indent to read it I would suggest to stop your reading here.

Boolean values can be encoded as functions like this:

tru = λt. λf. t

fls = λt. λf. f

Tru is a function that discards the value of its second argument and returns the value of its first argument. Fls is a function that discards the value of its first arguments and returns the value of its second argument. They are used as a representation of the True and False booleans.

The test combinator can be defined like this:

test = λl. λm. λn. l m n

If the first argument of test is tru the expression will reduce to m, if it is fls it will reduce to n. For example test tru x y evaluates to tru x y which evaluates to x. Awesome, it is almost like a if statement!

Numbers can be encoded too. The Church numerals 2 are defined like this:

c0 = λs. λz. z

c1 = λs. λz. s z

c2 = λs. λz. s (s z)

and so on and so on. Functions such as scc (successor) and plus can also be defined.

scc = λn. λs. λz. s (n s z)

plus = λm. λn. λs. λz. m s (n s z)

Data structures such as pairs can also be encoded:

pair = λf. λs. λb. b f s

fst = λp. p tru

snd = λp. p fls

Take a paper and a pen and evaluate fst (pair v w). It evaluates to v, as expected.

Lists can also be encoded. The list [x, y, z] can be encoded as the abstraction λc. λn. c x (c y (c z n)). That is a fold (also known as a reduce) is used to encode the list.

The usual functions to manipulate lists can be defined:

nil = λc. λn. n

isnil = λl. l (λh. λt. fls) tru

cons = λh. λt. λc. λn. c h (t c n)

head = λl. l (λh.λt.h) fls

tail = λl. fst (l (λx. λp. pair (snd p) (cons x (snd p))) (pair nil nil))

It is also possible to encode lists with pairs.

A mechanism similar to recursion can be defined by having functions reducing their arguments to a form similar to the function itself. For example this combinator:

(λx. x x) (λx. x x) reduces to himself.

More advanced tricks allow to define the equivalent of recursive functions such as the canonical definition of factorial.

Lambda calculus is a very simple but amazingly powerful language. It is also striking to make the comparison with some programming languages such as Java that could not even pass simply a function around before the most recent versions.

Congratulation for reading until there! Given all the shortcuts I took to explain, if you understood everything, well done.

Footnotes:

1

I’m paraphrasing the book here and also a lot below!

2

Alonzo Church invended the lambda calculus.

Comments