M = X
| λX.M
| (M M)
X = a variable: x, y, ...
x
(x y)
(λx.x)
(λy.(λz.y))
((λy.(y y)) (λy.(y y)))
- α-conversion
- β-reduction
- η-conversion
(a) Do computation with ONLY single-argument functions (no nullary function). Other type of values can be encoded with functions.
(b) Functions are first class, which means that functions can be passed as values.
(c) Multi-argument function is just a syntactic sugar. We can convert a multi-arg function to single arg functions. The process is known as Currying (c.f. Haskell Curry).
#lang racket
((λ (x y) (+ x y)) 3 4)
;; is equivalent to
(((λ (x) (λ (y) (+ x y))) 3) 4)
(define TRUE (λ (x) (λ (y) x))); given 2 things, choose the 1st
(define FALSE (λ (x) (λ (y) y))); given 2 things, choose the 2nd
(define NOT (λ (b) ((b FALSE) TRUE)))
;; fully expanded: (λ (b) ((b (λ (x) (λ (y) y))) (λ (x) (λ (y) x))))
(define AND (λ (x)
(λ (y)
((x y) x))))
(define OR (λ (x)
(λ (y)
((x x) y))))
(define IF (λ (c)
(λ (t)
(λ (f)
((c t) f)))))
https://en.wikipedia.org/wiki/Church_encoding
;; represent numbers with the number of times of repeatedly applying f
(define ZERO (λ (f) (λ (x) x))) ; Note this is how we defined FALSE
(define ONE (λ (f) (λ (x) (f x))))
(define TWO (λ (f) (λ (x) (f (f x)))))
(define THREE (λ (f) (λ (x) (f (f (f x))))))
(define FOUR (λ (f) (λ (x) (f (f (f (f x)))))))
(define FIVE (λ (f) (λ (x) (f (f (f (f (f x))))))))
(define SIX (λ (f) (λ (x) (f (f (f (f (f (f x)))))))))
(define SEVEN (λ (f) (λ (x) (f (f (f (f (f (f (f x))))))))))
;; and so on
;; we need this helper to actually see what the number is
(define _ (λ (x) (add1 x)))
((ZERO _) 0)
((ONE _) 0)
((TWO _) 0)
((THREE _) 0)
;; alternative helper for visualization
(define c (circle 5 "solid" "black"))
(define z (circle 5 "outline" "black"))
(define ~ (λ (x) (beside c x)))
((ZERO ~) z)
((ONE ~) empty-image)
((TWO ~) empty-image)
((THREE ~) empty-image)
https://wiki.haskell.org/Peano_numbers
;; Another way of encoding natural numbers
;; Recursive definition
;; NATURAL is one of:
;; - ZERO
;; - SUCC(NATURAL)
;; successor
;; n is a natural number,
;; which is a function with 2 arguments
;; that applies some function n times to its argument
(define SUCC (λ (n)
(λ (f)
(λ (x)
(f ((n f) x))))));apply f to x n times, then apply f again
(((SUCC ZERO) _) 0)
(((SUCC (SUCC ZERO)) _) 0)
(((SUCC (SUCC (SUCC ZERO))) _) 0)
;; Addition
#;
(define PLUS (λ (m)
(λ (n)
(λ (f)
(λ (x)
((m f) ((n f) x))))))); apply f n times, then apply f m times
;; a simpler definition using SUCC
(define PLUS (λ (m)
(λ (n)
((m SUCC) n))))
(print "4 + 3 = ")
((((PLUS FOUR) THREE) _) 0)
(print "2 + 3 = ")
((((PLUS (SUCC (SUCC ZERO))) (SUCC (SUCC (SUCC ZERO)))) _) 0)
;; Multiplication (repeated addition)
(define MULT (λ (m)
(λ (n)
((m (PLUS n)) ZERO))))
(print "2 x 2 = ")
((((MULT TWO) TWO) _) 0)
(print "3 x 4 = ")
((((MULT THREE) FOUR) _) 0)
;; Exponentiation
(define EXP (λ (m)
(λ (n)
(n m))))
((((EXP THREE) FOUR) _) 0)
((((EXP TWO) SIX) _) 0)
For predecessor and subtraction, we need to introduce pairs first
;; Encoding pairs and lists
;; we want the ability to 'select' from two paired items
(define CONS (λ (a) (λ (b) (λ (s) ((s a) b)))))
(define CAR (λ (p) (p TRUE)))
(define CDR (λ (p) (p FALSE)))
(define NIL FALSE) ;; denote empty list
;; Predecessor
;; the "wisdom tooth trick"
(define T (λ (p) ((CONS (SUCC (CAR p))) (CAR p))))
(define PRED (λ (n) (CDR ((n T) ((CONS ZERO) ZERO)))))
;; Subtraction
(define SUB (λ (x) (λ (y) ((y PRED) x))))
Division can be defined recursively (see below).
(define ZERO? (λ (n); if n is a natural number
((n (λ (x) FALSE)); apply this function to TRUE n times
TRUE))); if apply 0 times then it's TRUE
(define LEQ? (λ (m) (λ (n) (ZERO? ((SUB m) n)))))
(define GT? (λ (m) (λ (n) (NOT ((LEQ? m) n)))))
(define EQ? (λ (m) (λ (n) ((AND ((LEQ? m) n)) ((LEQ? n) m)))))
;; a somewhat interesting program:
; (if (zero? (+ 1 1)) (+ 1 2) (+ 3 4))
(((IF (ZERO? ((PLUS ONE) ONE)))
((((PLUS ONE) TWO) _) 0))
((((PLUS THREE) FOUR) _) 0))
Y-combinator
;; In Racket, recursive procedures can be defined using self-reference
;; However, in λ-calculus, functions are anonymous
#;
(define factorial
(λ (n)
(if (zero? n)
1
(* n (factorial (sub1 n))))))
#;
(define (divide n m)
(if (>= n m)
(add1 (divide (- n m) m))
0))
;; Y combinator
;; Y f = f (Y f)
(define Y (λ (f) ((λ (x) (f (x x))) (λ (x) (f (x x))))))
(define factorial (Y (λ (f)
(λ (n)
(if (zero? n)
1
(* n (f (sub1 n))))))))
(define FACTORIAL (Y (λ (f)
(λ (n)
(((ZERO? n)
ONE)
((MULT n) (f (PRED n))))))))
(define divide
(Y (λ (f)
(λ (n)
(λ (m)
(if (>= n m)
(add1 ((f (- n m)) m))
0))))))
(define DIVIDE
(Y (λ (f)
(λ (n)
(λ (m)
((((OR ((GT? n) m)) ((EQ? n) m))
(SUCC ((f ((SUB n) m)) m)))
ZERO))))))
- (Book) Church, A. (1941). The calculi of lambda-conversion. Princeton;London;: Princeton university press.
- (Book) The Lambda Calculus Its Syntax and Semantics. H.P. BARENDREGT
- (Paper) The Impact of the Lambda Calculus in Logic and Computer Science. Henk Barendregt
- (Paper) Call-by-Name, Call-by-Value, and The Lambda Calculus. Gordon Plotkin
- (Course notes, chapter 4) Felleisen, Matthias & Flatt, Matthew. (2007). Programming Languages and Lambda Calculi.
- (Paper) A Syntactic Theory of Sequential State. Matthias Felleisen and Daniel Friedman
- (Paper) Moggi, E. (1989). Computational lambda-calculus and monads. Paper presented at the 14-23. doi:10.1109/LICS.1989.39155.
- (Book) Barendregt, H. P., Dekkers, W., Statman, R., & Cambridge Core EBA eBooks Complete Collection. (2013). Lambda calculus with types. Cambridge;New York;: Cambridge University Press. doi:10.1017/CBO9781139032636
- (Book) Type theory and Formal Proofs. Ron Nederpelt and Herman Geuvers
- (Screencast) Lambda Calculus: PyCon 2019 Tutorial
- (Article) Compiling to lambda-calculus: Turtles all the way down
- Blog posts on lambda calculus from Good Math/Bad Math