constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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 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
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 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)
Thomas Streicher, example 3.4 of Realizability (2017/18) (pdf)
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 coalgebras:
Last revised on May 13, 2022 at 13:34:11. See the history of this page for a list of all contributions to it.