## Untyped Lambda Calculus

Tikhon Jelvis (tikhon@jelv.is)

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

# 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

# 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)$$
• cons: $$\lambda x. \lambda y. \lambda f. f x y$$
• first: $$\lambda x. \lambda y. x$$
• second: $$\lambda x. \lambda y. y$$