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