Let be the set of natural numbers equipped with the discrete topology, so that the function space is a countable product of copies of . By means of continued fractions, this space is homeomorphic to the Baire space of irrational numbers between and .
To define Kleene’s second algebra, we need several ingredients:
There is a function which takes the constant function at to , and any other function to the predecessor of the first non-zero .
Each irrational number releases a stream of rational approximants by successive truncations of the continued fraction of . By coding rational numbers by natural numbers, we get a corresponding stream of natural numbers . The map
that sends to is continuous.
is the terminal coalgebra of the endofunctor on , so there is an isomorphism whose inverse is denoted .
Composition of functions defines a map .
Now consider the composite
and curry this to a map . Let be the inclusion map.
Kleene’s second algebra is the applicative structure or partial binary operation on defined by the pullback
|type I computability||type II computability|
|typical domain||natural numbers||Baire space of infinite sequences|
|computable functions||partial recursive function||computable function (analysis)|
|type of computable mathematics||recursive mathematics||computable analysis, Type Two Theory of Effectivity|
|type of realizability||number realizability||function realizability|
|partial combinatory algebra||Kleene's first partial combinatory algebra||Kleene's second partial combinatory algebra|
Stephen Kleene, Introduction to Meta-Mathematics (1952)
Andrej Bauer, section 2 of Realizability as connection between constructive and computable mathematics, in T. Grubba, P. Hertling, H. Tsuiki, and Klaus Weihrauch, (eds.) CCA 2005 - Second International Conference on Computability and Complexity in Analysis, August 25-29,2005, Kyoto, Japan, ser. Informatik Berichte, , vol. 326-7/2005. FernUniversität Hagen, Germany, 2005, pp. 378–379. (pdf)
A presentation of neighborhood functions using algebras and co-algebras: