Untyped lambda calculus

\begin{align} K \; x \; y &= x \\ S \; x \; y \; z &= (x \; z) \; (y \; z) \end{align}

Simply typed lambda calculus

\[\frac{x : a \in \Gamma}{\Gamma \vdash x : a}\] → introduction (abstraction): \[\frac{\Gamma, x : a \vdash m : b}{\Gamma \vdash \lambda x^a . m : a \rightarrow b}\] → elimination (application): \[\frac{\Gamma \vdash m : a \rightarrow b \qquad \Gamma \vdash n : a}{\Gamma \vdash m \; n : b}\] × introduction (pair formation): \[\frac{\Gamma \vdash m : a \qquad \Gamma \vdash n : b}{\Gamma \vdash \langle m, n \rangle : a \times b}\] × elimination (pair extraction): \[\frac{\Gamma \vdash m : a \times b}{\Gamma \vdash \pi_1 \; m : a}\] \[\frac{\Gamma \vdash m : a \times b}{\Gamma \vdash \pi_2 \; m : b}\] Typed combinators: \begin{align} K &: a \rightarrow b \rightarrow a \\ S &: (a \rightarrow b \rightarrow c) \rightarrow (a \rightarrow b) \rightarrow (a \rightarrow c) \end{align}

Curry Howard correspondence

A program is a proof of its type.
programming logic
type theorem
program proof
inhabited type tautology
function type (→) implication (→)
product type (×) conjunction (∧)
abstraction implication introduction
application implication elimination (modus ponens)
lambda calculus natural deduction (focus on inference rules)
combinatory logic Hilbert-style deduction (focus on axioms)
Example: S, K, and application are complete for the implicational fragment of intuitionistic logic.

Primitive recursive functions

\begin{align} \text{zero} &: \mathbb{N} \\ \text{succ} &: \mathbb{N} \rightarrow \mathbb{N} \\ \text{iter} &: \mathbb{N} \rightarrow (\mathbb{N} \rightarrow \mathbb{N}) \rightarrow (\mathbb{N} \rightarrow \mathbb{N}) \end{align} \begin{align} \text{iter} \; \text{zero} \; f \; x &= x \\ \text{iter} \; (\text{succ} \; n) \; f \; x &= f \; (\text{iter} \; n \; f \; x) \\ \end{align} In other words, \[\text{iter} \; n \; f = f^n\] Examples: \[\text{add}, \text{mul}, \text{pow} : \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{N}\] \begin{align} \text{add} &= \lambda x. \text{iter} \; x \; \text{succ} \\ \text{mul} &= \lambda y. \lambda x. \text{iter} \; x \; (\text{add} \; y) \; \text{zero} \\ \text{pow} &= \lambda y. \lambda x. \text{iter} \; x \; (\text{mul} \; y) \; (\text{succ} \; \text{zero}) \end{align}

Primitive recursive functionals (System T)

Generalizes iteration to higher types: \[\text{iter} : \mathbb{N} \rightarrow (a \rightarrow a) \rightarrow (a \rightarrow a)\] System T is the set of computable functions whose termination is provable in Peano arithmetic.

System F

System F is the set of first-order functions that are provably total in second-order arithmetic. Parametric polymorphism → theorems about programs for free. \[\mathbb{B} = \forall a. a \rightarrow a \rightarrow a\] \begin{align} \text{T} &= \Lambda a. \lambda x^a. \lambda y^a. x \\ \text{F} &= \Lambda a. \lambda x^a. \lambda y^a. y \end{align} \[\mathbb{N} = \forall a. (a \rightarrow a) \rightarrow (a \rightarrow a)\] \begin{align} 0 &= \Lambda a. \lambda f^{a \rightarrow a}. \lambda x^a. x \\ 1 &= \Lambda a. \lambda f^{a \rightarrow a}. \lambda x^a. f \; x \\ 2 &= \Lambda a. \lambda f^{a \rightarrow a}. \lambda x^a. f \; (f \; x) \\ 3 &= \Lambda a. \lambda f^{a \rightarrow a}. \lambda x^a. f \; (f \; (f \; x)) \end{align} \begin{align} \text{id} &: \forall a. a \rightarrow a \\ \text{id} &= \Lambda a. \lambda x^a. x \end{align} \begin{align} \text{apply} &: \forall a. \forall b. (a \rightarrow b) \rightarrow (a \rightarrow b) \\ \text{apply} &= \Lambda a. \Lambda b. \lambda f^{a \rightarrow b}. \lambda x^a. f \; x \end{align} \begin{align} \text{compose} &: \forall a. \forall b. \forall c. (a \rightarrow b) \rightarrow (b \rightarrow c) \rightarrow (a \rightarrow c) \\ \text{compose} &= \Lambda a. \Lambda b. \Lambda c. \lambda f^{a \rightarrow b}. \lambda g^{b \rightarrow c}. \lambda x^a. g \; (f \; x) \end{align}

Calculus of constructions

Programming computable functions (PCF)

\[Y : (a \rightarrow a) \rightarrow a\] \[Y \; f = f \; (Y \; f)\]