A Relationship between Equilogical Spaces and Type Two Effectivity
- 31 October 2002
- 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