presentation_1.org

Untyped Lambda Calculus

Introduction

Lambda Calculus

• Invented by Alonzo Church (1920s)
• Equally expressive to the Turing Machine(s)
• Formal Language
• Computational Model
  • Lisp (1950s)
  • ML
  • Haskell
• “Lambda Expressions” in almost every modern programming language

Why should I care?

• Simple Computational Model
  • to describe structure and behaviour (E.g. Operational Semantics, Type Systems)
  • to reason and prove

• Explains why things in FP are like they are
  • Pure Functions
  • Higher-Order Functions
  • Currying
  • Lazy Evaluation

• Understand FP Compilers
  • Introduce FP stuff into other languages
  • Write your own compiler
  • GHC uses an enriched Lambda Calculus internally

Basics

Untyped Lambda Calculus

\begin{align*} t ::= & & \text{Terms:}
& \ x & \text{Variable} \ & \ λ x.t & \text{Abstraction} \ & \ t \ t & \text{Application} \end{align*}

Example - Identity

Lambda Calculus

\begin{equation*} \underbrace{ \underbrace{λ x.x}_\text{Abstraction} \quad \underbrace{y}_\text{Variable} }_\text{Application} → y \end{equation*}

Javascript

\begin{equation*} \underbrace{(\underbrace{function \ (x)\{return \ x;\}}_Abstraction) \ (\underbrace{y}_Variable)}_Application \end{equation*}

Example - $(λ x . λ y . x \ y) \ a \ b$

Abstractions

Think: Function Definitions

$(\underline{λ x . \underline{λ y . x \ y }}) \ a \ b$

Variables

Think: Parameters

$(λ x . λ y . \underline{x} \ \underline{y}) \ \underline{a} \ \underline{b}$

Applications

Think: Function Calls

$\lefteqn{\underline{\phantom{ (λ x . λ y . \underline{x \ y}) \ a }}} \lefteqn{(λ x . λ y . \underline{x \ y}) \ \underline{a \ b}}$

Example - $(λ x . λ y . x \ y) \ a \ b$

\begin{align*} \onslide<1->{ & ( λ \color<3->{orange}{x} . & λ y . & \color<3->{orange}{x} & y & ) & \color<3->{orange}{a} & & b & & \onslide<2->{ \text{Substitute $x \mapsto a $}} }
\onslide<4->{→ & & ( λ \color<6->{cyan}{y} . & \color{orange}{a} & \color<6->{cyan}{y} & ) & & & \color<6->{cyan}{b} & & \onslide<5->{\text{Substitute $y \mapsto b$}} } \ \onslide<7->{→ & & & \color{orange}{a} & \color{cyan}{b} & & & & & &} \end{align*}

Notational Conventions

• We use parentheses to clearify what’s meant
• Applications associate to the left

\begin{equation*} s \ t \ u ≡ (s \ t) \ u \end{equation*}

• Abstractions expand as much to the right as possible

\begin{equation*} λ x . λ y . x \ y \ x ≡ λ x . ( λ y . (x \ y \ x ) ) \end{equation*}

Scope

\begin{equation*} λ x . λ y . x \ y \ z \end{equation*}

Bound and Free

$λ y$

$y$ is bound, $x$ and $z$ are free

$λ x$

$x$ and $y$ are bound, $z$ is free

$λ x$, $λ y$

binders

A term with no free variables is closed

• A combinator
• $id ≡ λ x . x$
• Y, S, K, I …

Higher Order Functions

• Functions that take or return functions
  • Are there “by definition”

\begin{equation*} \underbrace{ \underbrace{λ x.x}_Abstraction \quad \underbrace{λ y.y}_Abstraction }_Application → \underbrace{λ y.y}_Abstraction \end{equation*}

Currying

Idea

• Take a function with $n$ arguments
• Create a function that takes one argument and returns a function with $n-1$ arguments

Example

• (+1) Section in Haskell
• $(λ x . λ y . + x \ y) \ 1 → λ y . + \ 1 \ y$

• Partial Function Application is there “by definition”
  • You can use this stunt to “curry” in every language that supports “Lambda Expressions”

Notes

• Moses Schönfinkel
  • If you want to sound smart: Schönfinkeling

Reductions and Conversions

Alpha Conversion

\begin{equation*} λ x . x →_α λ y . y \end{equation*}

Beta Reduction

\begin{equation*} (λ x . x) \ y →_β y \end{equation*}

Eta Conversion

Iff (if and only if) $x$ is not free in $f$: \begin{gather*} λ x . f \ x →_η f
(λ x . \underbrace{(λ y . y)}_f \ x) \ a →_η \underbrace{(λ y . y)}_f \ a \end{gather*}

If $x$ is free in $f$, η conversion not possible: \begin{equation*} λ x . \underbrace{(λ y . y \ \overset{\substack{\text{Bound} \ ↓}}{x})}_f \ x ¬\to_η ( λ y . y \ \overset{\substack{\text{Free?!} \ ↓}}{x}) \end{equation*}

Remarks

• Everything (Term) is an Expression
  • No statements
• No “destructive” Assignments
  • The reason why FP Languages promote pure functions
  • But you could invent a built-in function to manipulate “state”…

Evaluation

Operational Semantics

• We learned how to write down and talk about Lambda Calculus Terms
• How to evaluate them?
• Different Strategies
  • Interesting outcomes

Full Beta-Reduction

• RedEx
  • \textbf{Red}ucible \textbf{Ex}pression
  • Always an Application

\begin{equation*} \underbrace{ (λ x.x) \ (\underbrace{(λ y.y) \ (λ z.\underbrace{(λ a.a) \ z}_RedEx)}_RedEx) }_RedEx \end{equation*}

Full Beta-Reduction

• Any RedEx, Any Time
• Like in Arithmetics
• Too vague for programming…

Notes

How to write a good test if the next step could be several expressions?

Normal Order Reduction

\begin{align*} \onslide<1->{ & \alert<2->{ (λ x.x) \ ((λ y.y) \ (λ z.(λ a.a) \ z)) } \ } \onslide<3->{→ & \alert<4->{(λ y.y) \ (λ z.(λ a.a) \ z) } \ } \onslide<5->{→ & λ z.\alert<6->{(λ a.a) \ z } \ } \onslide<7->{→ & λ z.z } \end{align*}

Normal Order Reduction

• Left-most, Outer-most RedEx

Call-by-Name

\begin{align*} \onslide<1->{ & \alert<2->{ (λ x.x) \ ((λ y.y) \ (λ z.(λ a.a) \ z)) } \ } \onslide<3->{→ & \alert<4->{(λ y.y) \ (λ z.(λ a.a) \ z) } \ } \onslide<5->{→ & λ z.(λ a.a) \ z \ } \onslide<6->{¬\to} \end{align*}

Call-by-Name

• like Normal Order Reduction, but no reductions inside Abstractions
  • Abstractions are values
• lazy, non-strict
  • Parameters are not evaluated before they are used
• Optimization: Save results → Call-by-Need

Call-by-Value

\begin{align*} \onslide<1->{ & (λ x.x) \ \alert<2->{((λ y.y) \ (λ z.(λ a.a) \ z)) } \ } \onslide<3->{ → & \alert<4->{(λ x.x) \ (λ z.(λ a.a) \ z)} \ } \onslide<5->{ → & λ z.(λ a.a) \ z \ } \onslide<6->{¬ →} \end{align*}

Call-by-Value

• Outer-most, only if right-hand side was reduced to a value
• No reductions inside Abstractions
  • Abstractions are values
• eager, strict
  • Parameters are evaluated before they are used

Church Encodings

Church Encodings

• Encode Data into the Lambda Calculus
• To simplify our formulas, let’s say that we have declarations

\begin{gather*} id ≡ λ x.x
id \ y → y \end{gather*}

Booleans

Definitions

\begin{align*} true & ≡ & λ t. λ f.t
false & ≡ & λ t. λ f.f \ \ \onslide<2->{ test & ≡ & λ c . λ t . λ f . c \ t \ f } \end{align*}

Example

\begin{align*} \onslide<3->{& \alert<4->{test} \ true \ a \ b }
\onslide<5->{≡ & \ \alert<6->{(λ c . λ t . λ f . c \ t \ f) \ true } \ a \ b } \ \onslide<7->{→ & \ \alert<8->{(λ t . λ f . true \ t \ f) \ a} \ b } \ \onslide<9->{→ & \ \alert<10->{(λ f . true \ a \ f) \ b }} \ \onslide<11->{→ & \alert<12->{true} \ a \ b } \ \onslide<13->{≡ & \alert<14->{(λ t. λ f.t) \ a} \ b } \ \onslide<15->{→ & \alert<16->{(λ f.a) \ b } } \ \onslide<17->{→ & a } \end{align*}

And

Definitions

\begin{align*} true & ≡ & λ t. λ f.t
false & ≡ & λ t. λ f.f \ \ \onslide<2->{ and & ≡ & λ p . λ q . p \ q \ p } \end{align*}

Example

\begin{align*} \onslide<3->{& \alert<4->{and} \ true \ false }
\onslide<5->{≡ & \alert<6->{(λ p . λ q . p \ q \ p) \ true } \ false } \ \onslide<7->{→ & \alert<8->{(λ q . true \ q \ true) \ false } } \ \onslide<9->{→ & \alert<10->{true} \ false \ true } \ \onslide<11->{≡ & \alert<12->{(λ t. λ f.t) \ false} \ true } \ \onslide<13->{→ & \alert<14->{(λ f .false) \ true } } \ \onslide<15->{→ & false } \end{align*}

Or

\begin{equation*} λ p . λ q . p \ p \ q \end{equation*}

Pairs

Definitions

\begin{align*} \onslide<1->{pair & ≡ & λ x. λ y . λ z . z \ x \ y }
\onslide<2->{ first & ≡ & (λ p. p) \ λ x . λ y . x \ second & ≡ & (λ p. p) \ λ x . λ y . y } \end{align*}

Example

\begin{align*} \onslide<3->{pair_AB & ≡ & \alert<4->{pair} \ a \ b }
\onslide<5->{& ≡ & \alert<6->{(λ x. λ y . λ z . z\ x\ y) \ a } \ b } \ \onslide<7->{& → & \alert<8->{(λ y . λ z . z\ a\ y) \ b } } \ \onslide<9->{& → & λ z . z\ a \ b } \ \onslide<10->{& ≡ & pair’_ab } \ \end{align*}

Pairs (continued)

Definitions

\begin{align*} \onslide<1->{pair & ≡ & λ x. λ y . λ z . z \ x \ y
first & ≡ & (λ p. p) \ λ x . λ y . x \ pair’_ab & ≡ & λ z . z\ a \ b \ } \end{align*}

Example

\begin{align*} \onslide<2->{& & \alert<3->{first} \ pair’_ab }
\onslide<4->{& ≡ & \alert<5->{(λ p. p) \ (λ x . λ y . x) \ pair’_ab} } \ \onslide<6->{& → & \alert<7->{pair’_ab} \ (λ x . λ y . x) } \ \onslide<8->{& ≡ & \alert<9->{(λ z . z\ a \ b) \ (λ x . λ y . x) }} \ \onslide<10->{& → & \alert<11->{(λ x . λ y . x) \ a} \ b } \ \onslide<12->{& → & \alert<13->{(λ y . a) \ b } } \ \onslide<14->{& → & a} \end{align*}

Numerals

Peano Axioms

Every natural number can be defined with $0$ and a successor function \begin{align*} 0 & ≡ & λ f. λ x. x
1 & ≡ & λ f. λ x. f \ x \ 2 & ≡ & λ f. λ x. f \ (f \ x) \ 3 & ≡ & λ f. λ x. f \ (f \ (f \ x)) \ \end{align*}

Meaning

$0$

$f$ is evaluated $0$ times

$1$

$f$ is evaluated once

$x$

can be every lambda term

Numerals Example - Successor

Definitions

\begin{align*} \onslide<1->{ 0 & ≡ & λ f. λ x. x
1 & ≡ & λ f. λ x. f \ x \ } \ \onslide<2->{ successor & ≡ & λ n. λ f. λ x. f \ (n \ f \ x) } \end{align*}

Example

\begin{align*} \onslide<+(2)->{& & \alert<+(2)->{successor} \ 1 }
\onslide<+(2)->{& ≡ & \alert<+(2)->{(λ n. λ f. λ x. f \ (n \ f \ x)) \ 1 } } \ \onslide<+(2)->{& → & λ f. λ x. f \ (\alert<+(2)->{1} \ f \ x) } \ \onslide<+(2)->{& ≡ & λ f. λ x. f \ (\alert<+(2)->{(λ f. λ x. f \ x) \ f } \ x) } \ \onslide<+(2)->{& → & λ f. λ x. f \ (\alert<+(2)->{(λ x. f \ x) \ x}) } \ \onslide<+(2)->{& → & λ f. λ x. f \ (f \ x) } \ \onslide<+(2)->{& ≡ & 2} \end{align*}

Note

We use Normal Order Reduction to reduce inside abstractions!

Numerals Example - 0 + 0

Definitions

\begin{align*} \onslide<+->{0 & ≡ & λ f. λ x. x }
\ \onslide<+->{plus & ≡ & λ m. λ n. λ f. λ x. m \ f \ (n \ f \ x) } \end{align*}

Definitions

\begin{align*} \onslide<+->{& & \alert<+->{plus} \ 0 \ 0}
\onslide<+->{& ≡ & \alert<+->{(λ m. λ n. λ f. λ x. m \ f \ (n \ f \ x)) \ 0 } \ 0 } \ \onslide<+->{& → & \alert<+->{(λ n. λ f. λ x. 0 \ f \ (n \ f \ x)) \ 0 }} \ \onslide<+->{& → & λ f. λ x. \alert<+->{0} \ f \ (0 \ f \ x) } \ \onslide<+->{& ≡ & λ f. λ x. \alert<+->{(λ f. λ x. x) \ f} \ (0 \ f \ x) } \ \onslide<+->{& → & λ f. λ x. \alert<+->{(λ x. x) \ (0 \ f \ x) }} \ \onslide<+->{& → & λ f. λ x. \alert<+->{0} \ f \ x } \ \onslide<+->{& ≡ & λ f. λ x. \alert<+->{(λ f. λ x. x) \ f } \ x } \ \onslide<+->{& → & λ f. λ x. \alert<+->{(λ x. x) \ x }} \ \onslide<+->{& → & λ f. λ x. x } \ \onslide<+->{& ≡ & 0 } \end{align*}

End

Thanks

• Hope you enjoyed this talk and learned something new.
• Hope it wasn’t too much math and dusty formulas … :)

Books

Good Math

Image

Description

“A Geek’s Guide to the Beauty of Numbers, Logic, and Computation”

• Easy to understand

The Implementation of Functional Programming Languages

Image

Description

• How to compile to the Lambda Calculus?
• Out-of-print, but freely available
  • \small{https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/}

Types and Programming Languages

Image

Description

• Types systems explained by building interpreters and proving properties
• Very “mathematical”, but very complete and self-contained