restatement: \[\frac{}{\Gamma. x : a \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}
Linear logic: \begin{align} B &= \lambda x. \lambda y. \lambda z. x (y z) : (B \to C) \to (A \to B) \to (A \to C) & \text{composition} \\ C &= \lambda x. \lambda y. \lambda z. (x z) y : (A \to (B \to C)) \to (B \to (A \to C)) & \text{exchange} \end{align}
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 (more inference rules) |
| combinatory logic | Hilbert-style deduction (more axioms) |
| currying | exportation |
| types of S and K combinators | Łukasiewicz's axioms |
Example: S, K, and application are complete for the implicational fragment of intuitionistic logic.
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}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}