As we all know, Lisp is based on the Lambda Calculus. In this issue, we will open the lambda can of worms, especially as it relates to programming languages.

 

 

Lambda Calculus consists of three parts (with their Lisp equivalents):

Beta reduction is the step of replacing the arguments of a function with their value inside the body of the function.

 

I am only informally acquainted with lambda calculus, so this has been a learning experience for me.

 

Have fun!

This is the best tutorial on the lambda calculus I could find. It covers the history, recursion, reduction, and simple types.

The seminal paper where John McCarthy shows how a lambda calculus could be interpreted by a computer by defining a function apply which performs beta-reduction.

Using a subset of Scheme (basically the lambda calculus with conditionals), Guy Steele and Gerald Sussman shows that many imperative constructs can be easily implemented, including GOTO statements and assignment. This (almost) provides a transformational proof that the lambda calculus is Turing complete.

Steele and Sussman are at it again, basically proposing that lambda application is a GOTO which communicates data to and from the code gone to, and lambda abstraction is a declarative renaming operation. They use this model to show how an efficient Lisp compiler can be constructed.

Church Numerals are a way to represent the natural numbers as lambda expressions. They are impractical for most uses but are important to show that the lambda calculus is capable of representing arithmetic. In this brief blog post, Brian Carper explores Church Numerals in

Clojure.

There is a compact implementation of the Simply Typed Lambda Calculus in the core.logic README.

Be sure to ready Kazimir Majorinc's notes on how Lambda Calculus differs from Lisp.