**The Lambda Calculus: A Brief History**

Over this past weekend I took a lovely journey into the heart of the lambda calculus, and it was quite amazing. My explorations were made within the context of

LFE. Needless to say, this was a romp of pure delight. In fact, it was

*so* much fun and helped to clarify for me so many nooks and crannies of something that I had simply not explored very thoroughly in the past, that I

*had* to share :-)

The work done over the past few days is on its way to becoming part of the

documentation for LFE. However, this is also an excellent opportunity to share some clarity with a wider audience. As such, I will be writing a series of blog posts on λ-calculus from a very hands-on (almost practical!) perspective. There will be some overlap with the LFE documentation, but the medium is different and as such, the delivery will vary (sometimes considerably).

This series of posts will cover the following topics:

- A Brief History
- A Primer for λ-Calculus
- Reduction Explained
- Church Numerals
- Arithmetic
- Logic
- Pairs and Lists
- Combinators

The point of these posts is not to expound upon that which has already been written about endlessly. Rather, the hope is to give a very clear demonstration of what the lambda calculus

*really* is, and to do so with clear examples and concise prose. When the gentle reader is able see the lambda calculus in action, with lines of code that clearly show what is occurring, the mystery will disappear and an intuition for the subject matter will quite naturally begin to arise. This post is the first in the series; I hope you enjoy them as much as I did rediscovering λ-calculus :-)

Let us start at the beginning...

**A Brief History**
The roots of functional programming languages such as Lisp, ML, Erlang, Haskell and others, can be traced to the concept of recursion in general and λ-calculus in particular. In previous posts, I touched upon

how we ended up with the lambda as a symbol for the anonymous function as well as

how recursion came to be a going concern in modern mathematics and then computer science.

In both of those posts we saw

Alonzo Church play a major role, but we didn't really spend time on what is quite probably considered his greatest contribution to computer science, if not mathematics itself: λ-calculus. Keep in mind that the

Peano axioms made use of recursion, that

Giuseppe Peano played a key role in

Bertrand Russell’s development of the

Principia, that Alonzo Church sought to make improvements on the Principia, and λ-calculus eventually arose from these efforts.

Invented in 1928, Alonzo didn't publish λ-calculus until 1932. When an inconsistency was discovered, he revised it in 1933 and republished. Furthermore, in this second paper, Church introduced a means of representing positive integers using lambda notation, now known as Church numerals. With Church and Turing both publishing papers on computability in 1936 (based respectively upon λ-calculus and the concept of

Turing machines), they proposed solutions to the

Entscheidungsproblem. Though

Gödel preferred Turing's approach,

Rosser suggested that they were equivalent definitions in 1939. A few years later,

Kleene proposed the

Church Thesis (1943) and then later formally demonstrated the equivalence between his teacher's and Turing's approaches giving the combination the name of the

Church-Turing Thesis (1952, in his

__Introduction to Metamathematics__). Within eight years,

John McCarthy published his now-famous paper describing the work that he had started in 1958: "Recursive Functions of Symbolic Expressions and Their Computation by Machine". In this paper, McCarthy outlined his new programming language Lisp, citing Church's 77-page book (1941,

__Calculi of Lambda Conversion__), sending the world off in a whole new direction.

Since that time, there has been on-going research into λ-calculus. Indisputably, λ-calculus has had a tremendous impact on research into computability as well as the practical applications of programming languages. As programmers and software engineers, we feel its impact -- directly and indirectly -- on a regular, almost daily basis.

Syndicated 2013-04-09 05:22:00 (Updated 2013-04-09 05:22:48) from Duncan McGreggor