Lecture notes on Lambda Calculus Part 2: Church Numerals and Computability
Table of Contents
- 1. Introduction
- 2. Lambda Calculus Syntax
- 3. An embedding of $λ$-calculus in Scheme
- 4. Currying
- 5. Modeling data in \(\lambda\) calculus
- 6. Booleans and Conditional
- 7. Church Numerals
- 8. Pairs
- 9. Predecessor and Saturated Subtraction
- 10. Universality of lambda calculus
- 11. References and online resources
1 Introduction
The \(\lambda\) calculus, is a minimalist programming language of great theoretical as well as practical importance. While Turing machines may be thought of inspiring models of computer hardware, the \(\lambda\) calculus is model for software, or programs. By the Church-Turing thesis of effective computability, both \(\lambda\) calculus and Turing machines are canonical models of effective computation. The \(\lambda\) calculus is also the basis for the design of many modern day programming languages.
1.1 Syntax
2 Lambda Calculus Syntax
At a syntactic level, \(\lambda\) calculus is a system of manipulating expressions. Reduction is a relation on expressions.
At the semantic level, however, the purpose of studying \(\lambda\) expressions is to build a theory of functions to encode both data and computation.
Note that we are dealing with a hierarchy of three different
domains. At the top, we have the domain of expressions in
the lambda calculus. The meaning of these expressions is
given by mathematical functions. These functions in turn,
are used are used to encode data, like numbers, booleans.
Functions may be viewed as black boxes. Thus the function \(x\mapsto x+1\) may be seen as a black box. If you input \(5\) as an argument to it will return \(6\).
2.0.1 Notation
We use tt font when we write lambda expressions. We use
mathematical italicized font when referring to the meaning
of lambda expressions as black box functions. Finally,
the data encoded by these black boxes will also be written
in the italicized font.
For example, the lambda expression (lambda (x) (lambda
(y) x)) denotes the black box function \(\lambda\ x.\
\lambda y.\ x\). This function, in turn, encodes the data
element \(\id{true}\), a member of the set \(\id{BOOLEAN}\).
3 An embedding of $λ$-calculus in Scheme
It is this view that we will exploit simulate \(\lambda\) calculus in Scheme. So (closed) \(\lambda\) expressions will evaluate to closures, which are black boxes.
Note that $λ$-calculus is already built into Scheme! However, \(\lambda\) calculus is quite a bit more frugal: functions take exactly one formal parameter, and correspondingly, applications take a single argument. But we know how to create multiple argument functions from functions that take a single argument: currying.
4 Currying
(define :
(lambda (f x . xs)
(cond
[(null? xs) (f x)]
[else (apply : (f x) xs)])))
(define-syntax lambda:
(syntax-rules ()
[(lambda: (x) body) (lambda (x) body)]
[(lambda: (x y ...) body)
(lambda (x) (lambda: (y ...) body))]))
(define-syntax define:
(syntax-rules ()
[(define: (f x y ...) body) (define f (lambda: (x y ...) body))]))
5 Modeling data in \(\lambda\) calculus
Computation involves programs manipulating data. If we wish to model computation in the $λ$-calculus, we would need to model, from scratch, things we take for granted in a high level programming languages: numbers, booleans, pairs for data, and conditionals, selectors, function abstraction and application, recursion, etc. .
In order to distinguish the language which we are studying and the meanings of expressions in that language that exist in a ``value'' domain, we will use different fonts to represent expressions and their meanings.
For example, the expression (lambda (x) x) denotes the
function \(\lambda x.\ x\).
6 Booleans and Conditional
6.1 True and False
The primordial data elements true and false are defined
as the following \(\lambda\) expressions.
(define: (true x y) x) (define: (false x y) y) (check-equal? (: true 2 5) 2) (check-equal? (: false 2 5) 5) (check-equal? (: true 'love-me 'love-me-not) 'love-me) (define (show-bool b) (: b #t #f))
Notice that true is short hand for (lambda: (x y) x)
which itself is a short hand for (lambda (x) (lambda (y)
x)). (You may want to appreciate the mileage we are
deriving from the compact define: notation.) The
meaning of true, however, is the function (a black box)
\(\id{TRUE}\) that takes an argument \(x\) and returns a
function (another black box) that takes an argument \(y\) and
returns \(x\).
One way of thinking about \(\id{TRUE}\) and \(\id{FALSE}\) is that they are selectors: the former selects its first argument, while the latter selects the second argument, whatever those arguments are:
6.2 If-then-else
A conditional takes three arguments (curried of course!). The first is a boolean (either true or false). The result is applying the first argument, a boolean, to the other two.
(define: (ifte x y z) (: x y z)) (check-equal? (: ifte true 2 5) 2) (check-equal? (: ifte false 2 5) 5)
6.3 Other boolean operators
and, or, not and xor may follow easily:
(define: (not a) (: ifte a false true)) (define: (and a b) (: ifte a b false)) (define: (or a b) (: ifte a true b)) (define: (xor a b) (: ifte a (not b) b)) (check-equal? (: (not true) 3 5) 5) (check-equal? (: (: and true false) 3 5) 5) (check-equal? (: (: or true false) 3 5) 3) (check-equal? (: (: or false false) 3 5) 5) (check-equal? (: (: xor false true) 3 5) 3)
7 Church Numerals
We next consider an encoding of natural numbers via black boxes:
7.1 Zero
z encodes the number \(0\).
(define: (z f x) x)
One way thinking about it that \(\id{ZERO}\) is that when supplied arguments \(f\) and \(x\) \(\id{ZERO}\) computes the value \(f^0(x)\).
This suggests that the number \(n\) may be encoded as the blackbox function \(n\) which is \(\lambda\ f.\ \lambda\ x. f^{n}(x)\)
7.2 Successor
(define: (s n f x) (f (: n f x))) (define zero z) (define one (s zero)) (define two (s one)) (define three (s two)) (define (show-nat n) (: n add1 0)) (check-equal? (show-nat zero) 0) (check-equal? (show-nat one) 1) (check-equal? (show-nat two) 2) (check-equal? (: zero add1 5) 5) (check-equal? (: one add1 5) 6) (check-equal? (: two add1 5) 7) (check-equal? (: three add1 5) 8) (check-equal? (: ifte true (: two add1 5) (: zero add1 5)) 7) (check-equal? (: ifte true two zero add1 5) 7) (check-equal? (: ifte false two zero add1 5) 5)
7.3 zero?
(define: (z? n) (: n (lambda (x) false) true))
Note that this denotes the application \(f^n(\id{true})\) where \(f\) is the function \(\lambda\ x.\ \id{false}\). When \(n\) is \(0\), then the result is $\id{true}, otherwise, it is \(\id{false}\).
7.4 Addition
(define: (add m n f x) (: m f (: n f x))) (check-equal? (: add one two add1 5) 8)
7.5 Multiplication
(define: (mul m n f) (m (n f))) (check-equal? (: mul two three add1 5) 11) (check-equal? (: mul zero three add1 5) 5) (check-equal? (: mul one three add1 5) 8)
8 Pairs
(define: (pair a b sel) (: sel a b)) (define: (fst p) (p true)) (define: (snd p) (p false)) (check-true (eq? (fst (: pair one two)) one)) (check-true (eq? (snd (: pair one two)) two))
9 Predecessor and Saturated Subtraction
9.1 next
p is a pair of numbers.
(next (: pair a b)) returns (: pair (s a) a).
(define: (next p) (: pair (s (fst p)) (fst p))) (check-equal? (: fst (: next (: pair z z)) add1 4) 5) (check-equal? (: snd (: next (: pair z z)) add1 4) 4) (check-equal? (: fst (: next (: pair one two)) add1 4) 6) (check-equal? (: snd (: next (: pair one two)) add1 4) 5)
9.2 Predecessor
(: pred zero) is defined to be zero. Recall that if n
denotes the Church numeral \(n\), and f an arbitrary
function \(f\) then (: n f) denotes the function \(f^n\).
Also note that \(\id{next}^{n}\pair{0,0}\) denotes the
function \(\id{next}^f\pair{0,0}\), which yields \(\pair{n,
n-1}\). \(\id{pred}(n) = \id{snd}\pair{n, n-1}\), which equals
\(\id{snd}(\id{next}^n\pair{0,0})\).
(define: (pred n) (snd (: n next (: pair z z)))) (check-equal? (: pred one add1 5) 5) (check-equal? (: pred zero add1 5) 5) (check-equal? (: pred three add1 5) 7)
9.3 Saturated subtraction
Subtracting \(n\) from \(m\) is just taking the predecessor of \(m\) \(n\) times:
(define: (sub m n) (: n pred m))
9.4 Relational operators on numbers
(define: (leq m n) ; m <= n (: z? (: sub m n))) (define: (geq m n) ; m >= n (: z? (: sub n m))) (define: (gt m n) ; m > n (: not (: leq m n))) (define: (lt m n) ; m < n (: not (: geq m n))) (define: (eq m n) ; m = n (: and (leq m n) (leq n m)))
10 Universality of lambda calculus
Once we have recursion and the basic datatypes, it is not hard to see that we can take a Turing machine, and implement it. A Turing machine has a tape (with a finite segment containing symbols), a head (which is a finite state machine) and a tape counter (the position of the head on the tape).
11 References and online resources
- Benjamin Lynn's notes on lambda calculus
- Provides excellent notes motivating lambda calculus and presents a one-line universal machine (but without proof of its universality) in the lambda calculus.
- Manuel Eberl's notes on Untyped Lambda Calculus
- Systematically develops data types in the lambda calculus.
- Functional Bits: Lambda Calculus based Algorithmic Information Theory
- by John Tromp. A theory of the binary lambda calculus. Shows how to build a universal machine in lambda calculus and combinatory theory. You may also want to see John Tromp's page on Binary Lambda Calculus.
- David Evans's slides on the Lambda calculus
- Shows how one might convert a Turing Machine into a Lambda calculus machine.
- Cornell CS 312 Recitation on Lambda Calculus
- A short tutorial introduction to Lambda calculus.
- CS329 IIT Bombay: Notes on Lambda Calculus
- Notes by Rushikesh Joshi.
- Garrigue's notes on Computability and Lambda Calculus
- Demonstrates the simulation of a Turing machine by a Lambda Calculus term and vice versa.
- Lambda calculus: The other Turing Machine
- Harvard CS50 talk by Guy Blelloch and Robert Harper