Syntax

 M  = X
    | λX.M
    | (M M)
 X  = a variable: x, y, ...

Examples

 x
 (x y)
 (λx.x)
 (λy.(λz.y))
 ((λy.(y y)) (λy.(y y)))

Reductions

  • α-conversion
  • β-reduction
  • η-conversion

Ideas

(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)

Encoding Booleans

(define TRUE (λ (x) (λ (y) x))); given 2 things, choose the 1st
(define FALSE (λ (x) (λ (y) y))); given 2 things, choose the 2nd

Encoding NOT

(define NOT (λ (b) ((b FALSE) TRUE)))
;; fully expanded: (λ (b) ((b (λ (x) (λ (y) y))) (λ (x) (λ (y) x))))

Encoding AND, OR, IF

(define AND (λ (x)
              (λ (y)
                ((x y) x))))

(define OR (λ (x)
             (λ (y)
               ((x x) y))))

(define IF (λ (c)
             (λ (t)
               (λ (f)
                 ((c t) f)))))

Encoding Natural Numbers

Church Encoding

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

Helpers for visualization

;; 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)

Peano numbers

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)

Arithmetics

;; 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).

Predicates

(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))

Recursion

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))))))

References