---
title: "nlab-tte"
description: "nLab Type Two Theory of Effectivity Contents Contents Idea What is called Weihrauch’s Type-2 Theory (Weihrauch 87) is a measure for the complexity of computable functions on non- discrete topologica…"
doc_version: 1
last_updated: 2026-10-17
canonical_url: "http://parc.yolo.scapegoat.dev/note/research/institute/research/2026/04/16/philosophical-foundations-of-mathematics/sources/web/nlab-tte"
---

# nlab-tte

nLab Type Two Theory of Effectivity Contents Contents Idea What is called Weihrauch’s Type-2 Theory (Weihrauch 87) is a measure for the complexity of computable functions on non- discrete topologica…

## Content

## nLab Type Two Theory of Effectivity

Contents

## Contents

## Idea

What is called *Weihrauch’s Type-2 Theory* ([Weihrauch 87](https://ncatlab.org/nlab/show/Type+Two+Theory+of+Effectivity#Weihrauch87)) is a measure for the complexity of [computable functions](https://ncatlab.org/nlab/show/computable+functions) on non- [discrete](https://ncatlab.org/nlab/show/discrete+spaces) [topological spaces](https://ncatlab.org/nlab/show/topological+spaces) such as the [real line](https://ncatlab.org/nlab/show/real+line), the topic of [computable analysis](https://ncatlab.org/nlab/show/computable+analysis). While some approaches to [computability](https://ncatlab.org/nlab/show/computability) of [continuous functions](https://ncatlab.org/nlab/show/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](https://ncatlab.org/nlab/show/computation).

A quick survey is in the beginning of ([Schröder 04](https://ncatlab.org/nlab/show/Type+Two+Theory+of+Effectivity#Schroeder04)).

Essentially the type-II theory considers [functions](https://ncatlab.org/nlab/show/functions) between [topological spaces](https://ncatlab.org/nlab/show/topological+spaces) which may be encoded by infinite sequences of [natural numbers](https://ncatlab.org/nlab/show/natural+numbers), this is discussed in detail at *[computable function (analysis)](https://ncatlab.org/nlab/show/computable+function+%28analysis%29)*. As such this is a mathematical theory of [computability](https://ncatlab.org/nlab/show/computability) closely related to [exact real computer arithmetic](https://ncatlab.org/nlab/show/exact+real+computer+arithmetic).

- [computability](https://ncatlab.org/nlab/show/computability), [computable function (analysis)](https://ncatlab.org/nlab/show/computable+function+%28analysis%29)
- [domain theory](https://ncatlab.org/nlab/show/domain+theory)

**[computability](https://ncatlab.org/nlab/show/computability)**

|  | type I computability | type II computability |
| --- | --- | --- |
| typical domain | [natural numbers](https://ncatlab.org/nlab/show/natural+numbers) $\mathbb{N}$ | [Baire space](https://ncatlab.org/nlab/show/Baire+space+%28computability%29) of infinite sequences $\mathbb{B} = \mathbb{N}^{\mathbb{N}}$ |
| [computable functions](https://ncatlab.org/nlab/show/computable+functions) | [partial recursive function](https://ncatlab.org/nlab/show/partial+recursive+function) | [computable function (analysis)](https://ncatlab.org/nlab/show/computable+function+%28analysis%29) |
| type of [computable mathematics](https://ncatlab.org/nlab/show/computable+mathematics) | [recursive mathematics](https://ncatlab.org/nlab/show/recursive+mathematics) | [computable analysis](https://ncatlab.org/nlab/show/computable+analysis), [Type Two Theory of Effectivity](https://ncatlab.org/nlab/show/Type+Two+Theory+of+Effectivity) |
| type of [realizability](https://ncatlab.org/nlab/show/realizability) | [number realizability](https://ncatlab.org/nlab/show/number+realizability) | [function realizability](https://ncatlab.org/nlab/show/function+realizability) |
| [partial combinatory algebra](https://ncatlab.org/nlab/show/partial+combinatory+algebra) | [Kleene's first partial combinatory algebra](https://ncatlab.org/nlab/show/Kleene%27s+first+partial+combinatory+algebra) | [Kleene's second partial combinatory algebra](https://ncatlab.org/nlab/show/Kleene%27s+second+partial+combinatory+algebra) |

## References

The original article is

- [Klaus Weihrauch](https://ncatlab.org/nlab/show/Klaus+Weihrauch), *Computability*, EATCS Monographs in Theoretical Computer ScienceSpringer Verlag, Berlin Heidelberg (1987)
- [Klaus Weihrauch](https://ncatlab.org/nlab/show/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](http://web.archive.org/web/20160806025322/http://homepages.inf.ed.ac.uk/als/Research/Others/schroeder-mlq04.pdf))

Last revised on June 14, 2023 at 00:37:01. See the [history](https://ncatlab.org/nlab/history/Type+Two+Theory+of+Effectivity) of this page for a list of all contributions to it.

## Sitemap

- [Home](http://parc.yolo.scapegoat.dev/)
- [Home markdown mirror](http://parc.yolo.scapegoat.dev/index.md)
- [Markdown sitemap](http://parc.yolo.scapegoat.dev/sitemap.md)