First steps in synthetic domain theory. (English) Zbl 0747.18004
Category theory, Proc. Int. Conf., Como/Italy 1990, Lect. Notes Math. 1488, 131-156 (1991).
[For the entire collection see Zbl 0733.00009.]
Domain theory studies various categories \(\mathcal C\) of directed complete posets, which allow the possibility of finding fixed points of endomaps \(X\to X\) in \(\mathcal C\), as well as fixed points of various endofunctors \({\mathcal C}\to{\mathcal C}\), giving rise to functions defined by general recursion and interpretations for recursively defined types, respectively. (See S. Vickers, Topology via logic (1989; Zbl 0668.54001), for a very readable introduction to domains in the context of the theory of frames.)
The approach in this paper is motivated by analogy with the categorical approach to differential geometry known as Synthetic Differential Geometry (SDG). In SDG, following the work of Lawvere et al., “manifolds” are objects of some topos \(\mathcal E\) with a distinguished ring object \(R\), which plays the role of the real line. \(\mathcal E\) is required to satisfy various axioms related to \(R\). The usual category of manifolds can be embedded in these topos models and the approach allows for an intuitive, yet rigorous development of the subject.
In the paper under review, the author begins an axiomatic development of “synthetic domain theory” in an attempt to study effectivity in a categorical setting by considering a category \(\mathcal S\) with a distinguished object \(\Sigma\), which is a classifier of “semi- decidable” sets. \(\mathcal S\) could be a topos, but the full topos structure is not required; according to the author, the categorical properties required of \(\mathcal S\) are modelled on the category of modest sets in the effective topos [see J. M. E. Hyland, Ann. Pure Appl. Logic 40, 135-165 (1988; Zbl 0659.18007)]. The paper proceeds to develop the theory of these semi-decidable sets (or \(\Sigma\)-subsets), adding axioms to the theory as they are needed for further results and culminating in a discussion of \(\omega\)-chains and directed unions.
Domain theory studies various categories \(\mathcal C\) of directed complete posets, which allow the possibility of finding fixed points of endomaps \(X\to X\) in \(\mathcal C\), as well as fixed points of various endofunctors \({\mathcal C}\to{\mathcal C}\), giving rise to functions defined by general recursion and interpretations for recursively defined types, respectively. (See S. Vickers, Topology via logic (1989; Zbl 0668.54001), for a very readable introduction to domains in the context of the theory of frames.)
The approach in this paper is motivated by analogy with the categorical approach to differential geometry known as Synthetic Differential Geometry (SDG). In SDG, following the work of Lawvere et al., “manifolds” are objects of some topos \(\mathcal E\) with a distinguished ring object \(R\), which plays the role of the real line. \(\mathcal E\) is required to satisfy various axioms related to \(R\). The usual category of manifolds can be embedded in these topos models and the approach allows for an intuitive, yet rigorous development of the subject.
In the paper under review, the author begins an axiomatic development of “synthetic domain theory” in an attempt to study effectivity in a categorical setting by considering a category \(\mathcal S\) with a distinguished object \(\Sigma\), which is a classifier of “semi- decidable” sets. \(\mathcal S\) could be a topos, but the full topos structure is not required; according to the author, the categorical properties required of \(\mathcal S\) are modelled on the category of modest sets in the effective topos [see J. M. E. Hyland, Ann. Pure Appl. Logic 40, 135-165 (1988; Zbl 0659.18007)]. The paper proceeds to develop the theory of these semi-decidable sets (or \(\Sigma\)-subsets), adding axioms to the theory as they are needed for further results and culminating in a discussion of \(\omega\)-chains and directed unions.
Reviewer: K.I.Rosenthal (Schenectady)
