Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized

Definition 2.5

The abstraction of an expression $e \in \mathsf{Expr}\, \Gamma \, A$ with respect to a variable $x \in \Gamma $ is the expression $\langle x \rangle \, e \in \mathsf{Expr}\, \Gamma \, A$ defined recursively by

\begin{align*} \langle x \rangle \, x & = \mathsf{S}\cdot \mathsf{K}\cdot \mathsf{K}, \\ \langle x \rangle \, y & = \mathsf{K}\cdot y & & \text{if $x \neq y \in \Gamma $}, \\ \langle x \rangle \, a & = \mathsf{K}\cdot a & & \text{if $a \in A$}, \\ \langle x \rangle \, (e_1 \cdot e_2) & = \mathsf{S}\cdot (\langle x \rangle \, e_1) \cdot (\langle x \rangle \, e_2). \end{align*}

LaTeX Lean

Definition 4.1

A (total) combinatory algebra (CA) is given by a carrier set $A$ and a total binary operation ${-} \cdot {-} : A \times A \to A$, such that there are $\mathsf{K}, \mathsf{S}$ satisfying the characteristic equations

\begin{equation*} \mathsf{K}\cdot x \cdot y = x \qquad \text{and}\qquad \mathsf{S}\cdot x \cdot y \cdot z = (x \cdot z) \cdot (y \cdot z). \end{equation*}

LaTeX Lean

Definition 3.3Booleans

There are combinators $\mathsf{ite} \, \mathsf{fal}, \mathsf{tru} \in A$ such that, for all $a, b \in a$,

\begin{equation*} \mathsf{ite} \, \mathsf{tru} \ ,a \, b = a \text{and} \mathsf{ite} \, \mathsf{fal} \, a \, b = b. \end{equation*}

LaTeX

Lean

PCA.ite
PCA.fal
PCA.tru
PCA.eq_ite_fal
PCA.eq_ite_tru

Definition 3.1Identity

There is the identity combinator $\mathsf{I} \in A$ such that $I \, a = a$ for all $a \in A$.

LaTeX

Lean

PCA.I
PCA.eq_I

Definition 3.4Numerals

For each $n \in \mathbb {N}$ there is $\overline{n} \in A$, as well as combinators $\mathsf{succ}, \mathsf{primrec} \in A$ such that, for all $n \in \mathbb {N}$ and $a, f \in A$,

\begin{align*} \mathsf{succ} \, \overline{n} & = \overline{n+1}, \\ \mathsf{primrec} \, a \, f \, \overline{0} & = a, \\ \mathsf{primrec} \, a \, f \, \overline{n+1} & = f \, \overline{n} \, (\mathsf{primrec} \, a \, f \, \overline{n}). \end{align*}

LaTeX

Lean

PCA.numeral
PCA.succ
PCA.primrec
PCA.eq_primrec_zero
PCA.eq_primrec_succ

Definition 3.2Pairing

There are combinators $\mathsf{pair}, \mathsf{fst}, \mathsf{snd} \in A$ such that, for all $a, b \in A$,

\begin{align*} \mathsf{fst}\, (\mathsf{pair}\, a\, b) & = a, & \mathsf{snd}\, (\mathsf{pair}\, a\, b) & = b. \end{align*}

LaTeX

Lean

PCA.pair
PCA.fst
PCA.snd
PCA.eq_fst_pair
PCA.eq_snd_pair

Definition 3.5

There is a combinator $\mathsf{Y} \in A$ such that, for all $a \in A$,

\begin{equation*} \mathsf{Y} \, a = a (\mathsf{Z} \, a). \end{equation*}

LaTeX

Lean

PCA.Y
PCA.df_Y
PCA.eq_Y

Definition 3.6General recursion

There is a combinator $\mathsf{Z} \in A$ such that, for all $f, a \in A$,

\begin{equation*} \mathsf{Z} \, f\, {\Downarrow }, \qquad \text{and}\qquad \mathsf{Z} \, f \, a = f (\mathsf{Z} \, f) \, a. \end{equation*}

LaTeX

Lean

PCA.Z
PCA.df_Z
PCA.eq_Z

Definition 2.3

The evaluation $[\! [ e ]\! ] \, \eta $ of an expression $e \in \mathsf{Expr}\, \Gamma \, A$ in a PCA $A$ at a valuation $\eta : \Gamma \to A$ is defined recursively by the clauses

\begin{align*} [\! [ \mathsf{K} ]\! ] \, \eta & = \mathsf{K}\\ [\! [ \mathsf{S} ]\! ] \, \eta & = \mathsf{K}\\ [\! [ a ]\! ] \, \eta & = a & & \text{if $a \in A$}\\ [\! [ x ]\! ] \, \eta & = \eta (x) & & \text{if $x \in \Gamma $}\\ [\! [ e_1 \cdot e_2 ]\! ] \, \eta & = ([\! [ e_1 ]\! ] \, \eta ) \cdot _A ([\! [ e_2 ]\! ] \, \eta ). \end{align*}

LaTeX Lean

Definition 2.1

Given a set $\Gamma $ of variables and a set $A$ of elements, the expressions $\mathsf{Expr}\, \Gamma \, A$ are generated inductively by the following clauses:

the constants $\mathtt{K}$ and $\mathtt{S}$ are expressions,
an element $a \in A$ is an expression,
a variable $x \in \Gamma $ is an expression,
if $e_1$ and $e_2$ are expressions then $e_1 \cdot e_2$ is an expression.

LaTeX Lean

Definition 2.4

An expression $e \in \mathsf{Expr}\, \Gamma \, A$ is defined when $[\! [ e ]\! ] \, \eta \, {\Downarrow }$ for all $\eta : \Gamma \to A$.

LaTeX Lean

Definition 5.1

The free combinatory algebra is generated freely by the symbols $\mathsf{K}$ and $\mathsf{S}$ and formal binary application, quotiented by provable equality.

LaTeX Lean

Definition 5.3

The application ${-} \cdot {-} : \mathcal{P}\, A \times \mathcal{P}\, A \to \mathcal{P}\, A$ is defined by

\begin{equation*} S \cdot T = \{ x \in A \mid \exists y \in A.\, \mathsf{toSet}\, y \subseteq T \land \langle x,y \rangle \in S\} . \end{equation*}

LaTeX Lean

Definition 5.2

A listing on a set $A$ is a section $\mathsf{fromList} : \mathsf{List}\, A \to A$ and a retraction $\mathsf{toList} : A \to \mathsf{List}\, A$.

LaTeX Lean

Definition 2.2

Given a valuation $\eta : \Gamma \to A$, $x \in A$ and $a \in a$, we may override $\eta $ to get a valuation $\eta [x \mapsto a] : \Gamma \to A$ such that

\begin{equation*} (\eta [x \mapsto a]) y = \begin{cases} \eta (y) & \text{if $y \in \Gamma $,}\\ a & \text{if $y = x$.} \end{cases}\end{equation*}

LaTeX Lean

Definition 1.1

A partial application on a set $A$ is a map ${-} \cdot _A {-} : \widetilde{A} \times \widetilde{A} \to \widetilde{A}$.

LaTeX Lean

Definition 1.2

A set $A$ with a partial map ${-} \cdot _A {-}$ is a partial combinatory algebra (PCA) if there are elements $\mathsf{K}, \mathsf{S}\in \widetilde{A}$ such that, for all $u, v, w \in \widetilde{A}$:

\begin{align*} & K\, {\Downarrow }, & & S\, {\Downarrow },\\ & u\, {\Downarrow } \Rightarrow \mathsf{K}\, u\, {\Downarrow }, & & u\, {\Downarrow } \Rightarrow \mathsf{S}\, u\, {\Downarrow }, \\ & u\, {\Downarrow } \land v\, {\Downarrow } \Rightarrow \mathsf{K}\, u \, v\, {\Downarrow }, & & u\, {\Downarrow } \land v\, {\Downarrow } \Rightarrow \mathsf{S}\, u \, v\, {\Downarrow }, \\ & u\, {\Downarrow } \land v\, {\Downarrow } \Rightarrow \mathsf{K}\, u \, v = u, & & u\, {\Downarrow } \land v\, {\Downarrow } \land w\, {\Downarrow } \Rightarrow \mathsf{S}\, u \, v \, w\, {\Downarrow }, \\ & & & u\, {\Downarrow } \land v\, {\Downarrow } \land w\, {\Downarrow } \Rightarrow \mathsf{S}\, u \, v \, w = (u \, w) \, (v \, w), \\ \end{align*}

LaTeX Lean

Definition 3.7

A partial map $f : A \rightharpoonup A$ is represented by $a \in A$ when, for all $b \in B$, $f(b) = a \cdot b$.

LaTeX

Proposition 2.6

An abstraction $\langle x \rangle \, e$ is defined.

LaTeX Lean

Proposition 2.7

Let $x \in \Gamma $ and $e \in \mathsf{Expr}\, (\Gamma \cup \{ x\} )\, A$. Then for every $a \in A$ and $\eta : \Gamma \to A$

\begin{equation*} [\! [ (\langle x \rangle \, e) \cdot a ]\! ] \, \eta = [\! [ e ]\! ] \, \eta [x \mapsto a]. \end{equation*}

LaTeX Lean

Proposition 4.2

Every combinatory algebra is a partial combinatory algebra.

LaTeX Lean

Theorem 5.4

The set $\mathcal{P}\, A$ with the application as above is a combinatory algebra.

LaTeX Lean

Theorem 3.8

Every general recursive map $f : \mathbb {N}\rightharpoonup \mathbb {N}$ is represented in the following sense: there is $a \in A$ such that, for all $n \in \mathbb {N}$, if $f(n)\, {\Downarrow }$ then $\overline{f(n)} = a \cdot \overline{n}$.

LaTeX