Kleene's second algebra



Kleene’s second algebra is a partial combinatory algebra based on Baire space. It was introduced by Kleene to formalize Brouwer‘s notion of choice sequence.


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 BB of irrational numbers between 00 and 11.

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

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

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

    ϕ:BB\phi \colon B \to B

    that sends β\beta to (β 1,β 2,)(\beta_1, \beta_2, \ldots) is continuous.

  3. BB is the terminal coalgebra of the endofunctor ×- \times \mathbb{N} on TopTop, so there is an isomorphism ξ:BB×\xi \colon B \to B \times \mathbb{N} whose inverse is denoted prefixprefix.

  4. Composition of functions \mathbb{N} \to \mathbb{N} defines a map comp:B×BBcomp \colon B \times B \to B.

Now consider the composite

B×B×1 B×prefixB×B1 B×ϕB×BcompBp1+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 ψ:B×B(1+) \psi \colon B \times B \to (1 + \mathbb{N})^\mathbb{N}. Let i:1+i \colon \mathbb{N} \to 1 + \mathbb{N} be the inclusion map.

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

D i B×B ψ (1+) \array{ D & \to & \mathbb{N}^\mathbb{N} \\ \downarrow & & \downarrow^\mathrlap{i^\mathbb{N}} \\ B \times B & \underset{\psi}{\to} & (1 + \mathbb{N})^\mathbb{N} }


Relation to function realizability

Kleene’s second algebra is an abstraction of function realizability introduced for the purpose of extracting computational content from proofs in intuitionistic analysis. (e.g. Streicher 07, p. 17)


type I computabilitytype II computability
typical domainnatural numbers \mathbb{N}Baire space of infinite sequences 𝔹= \mathbb{B} = \mathbb{N}^{\mathbb{N}}
computable functionspartial recursive functioncomputable function (analysis)
type of computable mathematicsrecursive mathematicscomputable analysis, Type Two Theory of Effectivity
type of realizabilitynumber realizabilityfunction realizability
partial combinatory algebraKleene's first partial combinatory algebraKleene's second partial combinatory algebra


A presentation of neighborhood functions using algebras and co-algebras: