Syntax

A lambda expression $e$ is given by the syntax (where the $x$ represent variable names):

$$\begin{align*} e ::=& \ x && \mathrm{Variable} \\ | & \ e\ e && \mathrm{Application} \\ | & \ \lambda x. e && \mathrm{Abstraction} \\ \end{align*}$$

It satisfies the three elements that all programming languages have:

• Primitives: Atoms that can’t be broken down further
• Combination: A way of putting two expressions together
• Abstractions: A way to give a name to a compound expression

with Variables, Applications, and Abstractions, respectively.

External Resources

Introduction

• A Concise and Basic Introduction: http://www.cs.columbia.edu/~aho/cs4115/Lectures/15-04-13.html
• Introduction and Haskell Implementation with Morgensen encoding: https://crypto.stanford.edu/~blynn/lambda/
• This is another introduction which covers data encoding and recursion http://www.inf.fu-berlin.de/inst/ag-ki/rojas_home/documents/tutorials/lambda.pdf

Other

• Lambda Viewer lets you visualize the syntax tree of a lambda expression.
• Data Encoding: http://matt.might.net/articles/church-encodings-demo-in-scheme/
• Recursion: http://matt.might.net/articles/implementation-of-recursive-fixed-point-y-combinator-in-javascript-for-memoization/
• Compiling a subset of Scheme into the lambda calculus http://matt.might.net/articles/compiling-up-to-lambda-calculus/
• Implementing the lambda calculus http://matt.might.net/articles/implementing-a-programming-language/

Definitions

An upright word is to be interpreted as a single symbol. Function application is notated with a space.

The Church encoding is denoted with a subscript $c$ while the Scott encoding is denoted with a subscript $s$.

$$\begin{align*} \mathrm{zero}_c = \mathrm{zero}_s &= \lambda s. \lambda z. z \\ \mathrm{succ}_c &= \lambda n. \lambda s. \lambda z. s\ (n\ s\ z) \\ \mathrm{succ}_s &= \lambda n. \lambda s. \lambda z. s\ n \\ N_c &= \lambda s. \lambda z. \underbrace{ (s \cdots (s }_{N\text{ times}} \ z)\cdots) \\ N_s &= \underbrace{ \lambda s. \lambda z. s \cdots \lambda s. \lambda z. s }_{N\text{ times}}\ \lambda s. \lambda z. z \\ \mathrm{is0}_c = \mathrm{is0}_s &= \lambda n. n\ (\top\ \bot)\ \top = \lambda n. n\ \bot \ \mathrm{not} \ \bot \\ \\ \top &= \lambda t. \lambda f. t \\ \bot &= \lambda t. \lambda f. f = \lambda x. \mathrm{id} \\ \\ \mathrm{nil}_c = \mathrm{nil}_s &= \lambda c. \lambda n. n \\ \mathrm{cons}_c &= \lambda x. \lambda l. \lambda c. \lambda n. c\ x\ (l\ c\ n)\\ \mathrm{cons}_s &= \lambda x. \lambda l. \lambda c. \lambda n. c\ x\ l\\ \\ \mathrm{id} &= \lambda x. x \\ \mathrm{const} &= \lambda x. \lambda y. x \\ \mathrm{flip} &= \lambda f. \lambda x. \lambda y. f\ y\ x \\ \mathrm{if} &= \lambda b. \lambda t. \lambda f. b\ t\!\ f = \lambda b. b \\ \mathrm{not} &= \lambda b. \lambda t. \lambda f. b\!\ f\ t \\ \mathrm{and} &= \lambda p. \lambda q. p\ q\ p \\ \mathrm{or} &= \lambda p. \lambda q. p\ p\ q \\ \end{align*}$$

Observations

$$\begin{align*} 0 &= \bot = \mathrm{nil} \\ 1 &= \lambda s. \lambda z. s\ z = \lambda s. s = \mathrm{id} \\ \top &= \mathrm{const} \\ \mathrm{if} &= 1 = \mathrm{id} \\ \mathrm{not} &= \mathrm{flip} \\ \forall x, \ \bot\ x &= 1 \\ \end{align*}$$

Turing Machine Implementation

We present an explicit universal turing machine implementation in the Lambda Calculus, thus showing that Lambda Calculus is at least as powerful as Turing Machines.

The implementation is the function $U$ which takes a machine $m$ and a string $s$ and computes running $m$ on input $s$.

The result is $\top$ for accept, $\bot$ for reject and infinite recursion for non-halting.

The machine has a set of states $Q$ and a symbol set $\Gamma$. The machine is assumed to be given as $m = (q_0, q_a, q_r, b, \delta)$, where $q_0 : Q$ is the start state, $q_a : Q \to \mathbb{B}$ is a function that returns $\top$ if the input is an accept state and $\bot$ otherwise, $q_r : Q \to \mathbb{B}$ is a function that returns $\top$ if the input is an reject state and $\bot$ otherwise, $b : \Gamma$ is the blank symbol, and $\delta : Q \times \Gamma \to Q \times \Gamma \times \{L, R\}$ is the transition function from the current state and read tape character to the next state, the written tape character, and the head movement (Left or Right).

The input string is assumed to be in the form of a linked list in the Scott encoding (where the list [1,2] is represented as $\lambda c. \lambda n. c 1 (\lambda c. \lambda n. c 2 n)$).

This lambda expression takes as input the machine $m$ and the string $s$ and returns $\top$ if $m(s)$ accepts, returns $\bot$ if $m(s)$ rejects, and never normalizes if $m(s)$ doesn’t halt.

$$\begin{align*} U =\, & \lambda m. \lambda s. m \lambda q_0. \lambda q_a. \lambda q_r. \lambda b. \lambda d.\\ &\quad Y (\lambda f.\\ &\quad \quad \lambda q. \lambda t_a. \lambda t_b.\\ &\quad \quad \quad q_a q \top (\\ &\quad \quad \quad q_r q \bot (\\ &\quad \quad \quad \quad (\lambda u.\\ &\quad \quad \quad \quad \quad t_b (\quad \quad \quad \ \ \!\ d (\lambda p. p q b) (u t_a t_b))\\ &\quad \quad \quad \quad \quad \quad (\lambda g. \lambda t_b. d (\lambda p. p q g) (u t_a t_b))\\ &\quad \quad \quad \quad ) \lambda t_a. \lambda t_b. \lambda q. \lambda g. \lambda h.\\ &\quad \quad \quad \quad \quad h (t_a (f q \bot \lambda c. \lambda n. c g t_b)\\ &\quad \quad \quad \quad \quad \quad \quad \quad (\lambda g'. \lambda t_a. f q t_a \lambda c. \lambda n. c g' \lambda c. \lambda n. g t_b))\\ &\quad \quad \quad \quad \quad \quad (f q (\lambda c. \lambda n. g t_a) t_b)\\ &\quad \quad \quad ))\\ &\quad ) q_0 \bot s \end{align*}$$

Here is an analogous implementation in Haskell