Lambda Calculus.

Clojure Gazette

Issue 1.17 - July 28, 2012

editorial

Exploring the connection between lambda calculus and programming

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 toprogramming languages.

A brief introduction:

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

1. variables (symbols)
2. lambda abstraction (defining a function)
3. lambda application (applying a function)

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

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

Have fun!

Eric Normand

PS I love to hear from readers. Just reply to this email to get in touch!
PPS Tell your friends about the Clojure Gazette.

tutorial introduction

An short introduction to the Lambda Calculus

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

video lecture

Untyped lambda-calculus, inference rules, environment, ...

Slides and audio from a University of Washington Programming Languages course. There's a lot of material in this lecture.

strong foundations

Recursive Functions of Symbolic Expressions and Their Computation by Machine

The seminal paper where John McCarthy shows how a lambda calculuscould be interpreted by a computer by defining a function apply whichperforms beta-reduction.

completness

Lambda: The Ultimate Imperative

Using a subset of Scheme (basically the lambda calculus withconditionals), Guy Steele and Gerald Sussman shows that manyimperative constructs can be easily implemented, including GOTOstate ments and assignment. This (almost) provides a transformationalproof that the lambda calculus is Turing complete.

lambda as goto

Lambda: The Ultimate Declarative

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

church numerals

Church Numerals in Clojure

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

Clojure.

type inference

core.logic

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

lisp is not exactly lambda calculus

Some Differences Between Lambda Calculus and Lisp

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