Type Two Theory of Effectivity



Constructivism, Realizability, Computability



What is called Weihrauch’s Type-2 Theory (Weihrauch 87) is a measure for the complexity of computable functions on non-discrete topological spaces such as the real line, the topic of computable analysis. While some approaches to computability of continuous functions take pointwise addition as an elementary operation, Weihrauch’s Type-2 theory is instead “bit oriented” and takes into account the finitary aspects of computation.

A quick survey is in the beginning of (Schröder 04).

Essentially the type-II theory considers functions between topological spaces which may be encoded by infinite sequences of natural numbers, this is discussed in detail at computable function (analysis). As such this is a mathematical theory of computability closely related to exact real computer arithmetic.


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


The original article is

  • Klaus Weihrauch, Computability, EATCS Monographs in Theoretical Computer ScienceSpringer Verlag, Berlin Heidelberg (1987)

  • Klaus Weihrauch, A foundation of computable analysis in D.S. Bridges, C.S. Calude, J. Gibbons, S. Reeves, I.H. Witten (eds.), Combinatorics, complexity and logic, discrete mathematics and computer science, Proceedings of DMTCS 96, Springer Verlag, Singapore (1997), pp. 66–89

The equivalence of this to real PCF is shown in

  • Holger Schulz, Type Two Theory of Effectivity and Real PCF, Electronic Notes in Theoretical Computer Science Volume 35, 2000, Pages 191–203

See also

  • Matthias Schröder, Spaces Allowing Type-2 Complexity Theory Revisited, 2004 (pdf)

Last revised on January 27, 2018 at 23:48:31. See the history of this page for a list of all contributions to it.