nLab
Kleene's second algebra

Kleene’s second algebra is a partial combinatory algebra based on Baire space.

Let $\mathbb{N}$ be the set of natural numbers equipped with the discrete topology, so that the function space ${\mathbb{N}}^{\mathbb{N}}$ is a countable product of copies of $\mathbb{N}$. By means of continued fractions?, this space is homeomorphic to the Baire space $B$ of irrational numbers between $0$ and $1$.

To define Kleene’s second algebra, we need several ingredients:

1. There is a function $p:B\to 1+\mathbb{N}$ which takes the constant function at $0$ to $*\in 1$, and any other function $\alpha :\mathbb{N}\to \mathbb{N}$ to the predecessor of the first non-zero $\alpha (k)$.

2. Each irrational number $\beta \in B$ releases a stream of rational approximants $q_1(\beta ),q_2(\beta ),\dots$ by successive truncations of the continued fraction of $\beta$. By coding rational numbers by natural numbers, we get a corresponding stream of natural numbers $({\beta }_1,{\beta }_2,\dots )\in {\mathbb{N}}^{\mathbb{N}}$. The map

   $$\varphi :B\to B$$\phi \colon B \to B

   that sends $\beta$ to $({\beta }_1,{\beta }_2,\dots )$ is continuous.

3. $B$ is the terminal coalgebra of the endofunctor $-\times \mathbb{N}$ on $\mathrm{Top}$, so there is an isomorphism $\xi :B\to B\times \mathbb{N}$ whose inverse is denoted $\mathrm{prefix}$.

4. Composition of functions $\mathbb{N}\to \mathbb{N}$ defines a map $\mathrm{comp}:B\times B\to B$.

Now consider the composite

$$B\times B\times \mathbb{N}\stackrel{1_B\times \mathrm{prefix}}{\to }B\times B\stackrel{1_B\times \varphi }{\to }B\times B\stackrel{\mathrm{comp}}{\to }B\stackrel{p}{\to }1+\mathbb{N}$$B \times B \times \mathbb{N} \stackrel{1_B \times prefix}{\to} B \times B \stackrel{1_B \times \phi}{\to} B \times B \stackrel{comp}{\to} B \stackrel{p}{\to} 1 + \mathbb{N}

and curry this to a map $\psi :B\times B\to (1+\mathbb{N}{)}^{\mathbb{N}}$. Let $i:\mathbb{N}\to 1+\mathbb{N}$ be the inclusion map.

Kleene’s second algebra is the applicative structure or partial binary operation on $B$ defined by the pullback

$$\begin{array}{ccc}D& \to & {\mathbb{N}}^{\mathbb{N}}\\ \downarrow & & {\downarrow }^{i^{\mathbb{N}}}\\ B\times B& \underset{\psi }{\to }& (1+\mathbb{N}{)}^{\mathbb{N}}\end{array}$$\array{ D & \to & \mathbb{N}^\mathbb{N} \\ \downarrow & & \downarrow^\mathrlap{i^\mathbb{N}} \\ B \times B & \underset{\psi}{\to} & (1 + \mathbb{N})^\mathbb{N} }