Untyped Lambda Calculus

Tikhon Jelvis (tikhon@jelv.is)

Press → key to advance.
Zoom in/out: Ctrl or Command + +/-

1 Why

  • simple model of functions
    • everything else stripped away
  • makes it easier to reason about programs
    • formal reasoning: proofs
    • informal reasoning: debugging
  • designing languages
    • simple semantics—easy to extent
    • ML, Haskell, Lisp, …

2 Introduction to theory

  • basis for type theory
  • introduction to concepts & notation
  • "mathematical mindset"

3 Abstract Syntax

  • λ-calculus—syntactic manipulation
  • made up of expressions (\(e\)) $$\begin{align} e ::&= x & \text{variable}\\ &|\quad \lambda x. e & \text{abstraction} \\ &|\quad e_1 e_2 & \text{application} \end{align}$$

4 Examples

  • \(\lambda x. x\) is the identity function
    • compare: \(f(x) = x\)
  • \(\lambda x. \lambda y. x\) constant function
    • implicit parentheses: \(\lambda x. (\lambda y. x)\)
    • compare: \(f(x, y) = x\)

5 Scoping

  • static scope, just like most programming languages
  • names do not matter (α equivalence): $$\lambda x. x \equiv \lambda y. y$$
  • variables can be shadowed: $$\lambda x. \lambda x. x \equiv \lambda x. \lambda y. y$$

6 Free vs Bound

  • bound: defined inside an expression: $$\lambda x. x$$
  • free: not defined inside an expression: $$\lambda x. y$$
  • free vs bound, \(y\) vs \(x\): $$\lambda x. y x$$

7 Evaluation

  • core idea: substitution
    • replace name of argument with its value
  • example: given \(y x\), we can substitute \(\lambda a. a\) for \(x\): $$ y (\lambda a. a) $$
  • careful with scoping!
    • just rename everything

8 Evaluation Rules

  • function application (β-reduction)

$$ \frac{(\lambda x. e_1)e_2}{[e_2/x]e_1} $$

  • extension (η-reduction)

$$ \frac{\lambda x. F x}{F} $$

  • as long as \(x\) does not appear in \(F\)

9 Writing an interpreter

  • this is all we need to write an interpreter
  • any typed functional language:
    • SML, F#, OCaml, Haskell, Scala
  • I will use Haskell syntax

10 Type

$$\begin{align} e ::&= x & \text{variable}\\ &|\quad \lambda x. e & \text{abstraction} \\ &|\quad e_1 e_2 & \text{application} \end{align}$$

  • translate to an algebraic data type: 
type Name = Char

data Expr = Variable Name
          | Lambda Name Expr
          | App Expr Expr

11 Pattern Matching

  • pattern matching: operate on ADT by cases 
eval ∷ Expr → Expr
eval (Lambda x e) = Lambda x e
eval (Variable n) = Variable n
eval (App e₁ e₂)  = case eval e₁ of
  Lambda x body → eval (subst x e₂ body)
  result        → App result e₂

12 Substitution 

subst ∷ Name → Expr → Expr → Expr
subst x newVal (Lambda y body) 
  | x ≠ y     = Lambda y (subst x newVal body)
  | otherwise = Lambda y body
subst x newVal (App e₁ e₂) =
  App (subst x v e₁) (subst x v e₂)
subst x newVal (Variable y)
  | x ≡ y     = newVal
  | otherwise = Variable y

13 Evaluation Order

  • How far to evaluate? 
eval (Lambda x e) = Lambda x (eval e)
  • What order to evaluate in?
    • when to evaluate arguments? 
Lambda x body → eval (subst x (eval e₂) body)

14 Fun Stuff

  • Write your own interpreter (< 1hr)
  • Add parsing, pretty printing and a REPL
  • Experiment with different evaluation orders
  • Add features like numbers

15 Numbers

  • λ-calculus only has functions
  • can we represent data structures and numbers?
  • idea: numbers as repeated application
  • zero: \(\lambda f.\lambda x. x\)
  • one: \(\lambda f. \lambda x. f x\)
  • two: \(\lambda f. \lambda x. f (f x)\)
  • implement addition and subtraction*

16 Data Structures

  • Lisp-style pairs
  • idea: function that applies another function to two arguments
  • cons: $$\lambda x. \lambda y. \lambda f. f x y$$
  • first: $$\lambda x. \lambda y. x$$
  • second: $$\lambda x. \lambda y. y$$
  • build up things like lists