A Relationship between Equilogical Spaces and Type Two Effectivity

• 31 October 2002
• Andrej Bauer
• Publications

Abstract: In this paper I compare two well studied approaches to topological semantics—the domain-theoretic approach, exemplified by the category of countably based equilogical spaces, `omega`Equ, and Type Two Effectivity, exemplified by the category of Baire space representations, Rep(B). These two categories are both locally cartesian closed extensions of countably based `T_0`-spaces. A natural question to ask is how they are related.

First, we show that Rep(B) is equivalent to a full coreflective subcategory of `omega`Equ, consisting of the so-called `0`-equilogical spaces. This establishes a pair of adjoint functors between Rep(B) and `omega`Equ. The inclusion of Rep(B) in `omega`Equ and its coreflection have many desirable properties, but they do not preserve exponentials in general. This means that the cartesian closed structures of Rep(B) and `omega`Equ are essentially different. However, in a second comparison we show that Rep(B) and `omega`Equ do share a common cartesian closed subcategory that contains all countably based `T_0`-spaces. Therefore, the domain-theoretic approach and TTE yield equivalent topological semantics of computation for all higher-order types over countably based `T_0`-spaces. We consider several examples involving the natural numbers and the real numbers to demonstrate how these comparisons make it possible to transfer results from one setting to another.

Published in: Mathematical logic quarterly, 2002, vol. 48, suppl. 1, 1-15.

Download: equtte.pdf, equtte.ps.gz