analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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 computability | type II computability | |
---|---|---|
typical domain | natural numbers $\mathbb{N}$ | Baire space of infinite sequences $\mathbb{B} = \mathbb{N}^{\mathbb{N}}$ |
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 |
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
See also