Lambda Calculus Talk from Pycon 2019

This is a fantastic introduction to Lambda Calculus by David Beazley. He uses Python to implement it. He imagines a world where all you have are functions that take one parameter (the parameter is also a function) – that’s it, no variables, strings, nothing else just functions that take a singular function as a parameter --, and from this basic starting point is able to derive the concepts of True and False, natural numbers, arithmetic, basic control structures, recursion, and ycombinators. Using just some clever manipulation of functions he’s able to essentially create an instruction set that can do much of what you would expect a computer to be able to do. For someone who has no real training in any of the theory behind computer science this was fantastic, and I thought some of you guys might enjoy it too.

11 Likes

Thanks for this great recommendation! I watched the whole video, and followed along using Lazy Racket.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Usage:
;; Run `racket -I lazy` to open the REPL
;; Run `(load "main.rkt")` from inside the REPL

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Booleans

;; There is nothing intrinsically true or false. We will define both of them
;; using behaviors.
;; True takes two arguments and returns the first one. On the other hand, false
;; takes two arguments and returns the second one.

(define FALSE
  (lambda (x)
    (lambda (y)
      y)))
(define TRUE
  (lambda (x)
    (lambda (y)
      x)))

;; Logic Operations

(define NOT
  (lambda (x)
    ((x FALSE) TRUE)))

;; (printf "NOT(FALSE) -> ~a\n" (NOT FALSE))
;; (printf "NOT(TRUE ) -> ~a\n" (NOT TRUE ))

(define AND
  (lambda (x)
    (lambda (y)
      ((x y) x))))

;; (printf "AND(FALSE)(FALSE) -> ~a\n" ((AND FALSE) FALSE))
;; (printf "AND(FALSE)(TRUE ) -> ~a\n" ((AND FALSE) TRUE ))
;; (printf "AND(TRUE )(FALSE) -> ~a\n" ((AND TRUE ) FALSE))
;; (printf "AND(TRUE )(TRUE ) -> ~a\n" ((AND TRUE ) TRUE ))

(define OR
  (lambda (x)
    (lambda (y)
      ((x x) y))))

;; (printf "OR(FALSE)(FALSE) -> ~a\n" ((OR FALSE) FALSE))
;; (printf "OR(FALSE)(TRUE ) -> ~a\n" ((OR FALSE) TRUE ))
;; (printf "OR(TRUE )(FALSE) -> ~a\n" ((OR TRUE ) FALSE))
;; (printf "OR(TRUE )(TRUE ) -> ~a\n" ((OR TRUE ) TRUE ))

(define XOR
  (lambda (x)
    (lambda (y)
      ((x (NOT y)) y))))

;; (printf "XOR(FALSE)(FALSE) -> ~a\n" ((XOR FALSE) FALSE))
;; (printf "XOR(FALSE)(TRUE ) -> ~a\n" ((XOR FALSE) TRUE ))
;; (printf "XOR(TRUE )(FALSE) -> ~a\n" ((XOR TRUE ) FALSE))
;; (printf "XOR(TRUE )(TRUE ) -> ~a\n" ((XOR TRUE ) TRUE ))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Numbers

(define ZERO  (lambda (f) (lambda (x)                x)))
(define ONE   (lambda (f) (lambda (x)             (f x))))
(define TWO   (lambda (f) (lambda (x)          (f (f x)))))
(define THREE (lambda (f) (lambda (x)       (f (f (f x))))))
(define FOUR  (lambda (f) (lambda (x)    (f (f (f (f x)))))))
(define FIVE  (lambda (f) (lambda (x) (f (f (f (f (f x))))))))

(define show-num
  (lambda (n)
    ((n add1) 0)))

;; (printf "\n")
;; (printf "ZERO  -> ~a\n" (show-num ZERO ))
;; (printf "ONE   -> ~a\n" (show-num ONE  ))
;; (printf "TWO   -> ~a\n" (show-num TWO  ))
;; (printf "THREE -> ~a\n" (show-num THREE))
;; (printf "FOUR  -> ~a\n" (show-num FOUR ))
;; (printf "FIVE  -> ~a\n" (show-num FIVE ))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Data-Structures

(define CONS
  (lambda (a)
    (lambda (b)
      (lambda (i)
        ((i b) a)))))

(define CAR
  (lambda (p)
    (p FALSE)))

(define CDR
  (lambda (p)
    (p TRUE)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Arithmetic

(define SUCC
  (lambda (n)
    (lambda (f)
      (lambda (x)
        (f ((n f) x))))))

(define ADD
  (lambda (x)
    (lambda (y)
      ((y SUCC) x))))

(define MUL
  (lambda (x)
    (lambda (y)
      (lambda (f)
        (y (x f))))))

(define PRED-HELPER
  (lambda (p)
    ((CONS (SUCC (CAR p))) (CAR p))))

;; Predecessor
(define PRED
  (lambda (n)
    (CDR ((n PRED-HELPER) ((CONS ZERO) ZERO)))))

(define SUB
  (lambda (x)
    (lambda (y)
      ((y PRED) x))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Control-Flow

(define ZERO?
  (lambda (n)
    ((n (lambda (_) FALSE)) TRUE)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Computation / Recursion

;; Factorial
;; (define FACT
;;   (lambda (n)
;;     (((ZERO? n) ONE) ((MUL n) (FACT (PRED n))))))

;; Factorial without self-reference
(define FACT
  ((lambda (f)
    (lambda (n)
      (((ZERO? n) ONE) ((MUL n) ((f f) (PRED n))))))
   (lambda (f)
    (lambda (n)
      (((ZERO? n) ONE) ((MUL n) ((f f) (PRED n))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; The Y Combinator

;; Equality here is in the mathematical sense, not an assignment:
;; fact = (λf: λn: 1 if n == 0 else n * f(n - 1))(fact)
;; Take the part in the first parentheses:
;; R = (λf: λn: 1 if n == 0 else n * f(n - 1))
;; We get:
;; fact = R(fact)
;; fact is a fixed-point of R
;; Suppose there was a function Y that computes the fixed point of R:
;; Y(R) -> Fixed-Point of R (whatever it is)
;; Y(R) = R(Y(R))
;; Recursion Trick:
;; Y(R) = (λx: R(x))(Y(R))
;; Remove Self-Reference:
;; Y(R) = (λx: R(x(x)))(λx: R(x(x)))
;; Pull the R out:
;; Y(R) = (λf: (λx: f(x(x)))(λx: f(x(x))))(R)
;; We get the Y combinator:
;; Y = (λf: (λx: f(x(x)))(λx: f(x(x))))

(define Y
  (lambda (f)
    ((lambda (x) (f (x x)))
     (lambda (x) (f (x x))))))

(define FACT-R
  (lambda (f)
    (lambda (n)
      (((ZERO? n) ONE) ((MUL n) (f (PRED n)))))))

(define FACT-Y (Y FACT-R))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

It’s hard to say what the most surprising thing in the video was:

  • Lambda Calculus is Turing-Complete.
  • Building a linked-list using functions.
  • The Y Combinator.

I really liked all of it.

I love his style so hard. He’s like a stage magician. His other stuff are also very entertaining and instructive.

1 Like