The Fixed Point Property in Synthetic Domain Theory

We present an elementary axiomatisation of synthetic domain theory and show that it is sufficient to deduce the fixed point property and solve domain equations. Models of these axioms based on partial equivalence relations have received much attention, but there are also very simple sheaf models based on classical domain theory. In any case the aim of this paper ow that an important theorem can be derived from an abstract axiomatisation, rather than from a particular model. Also, by providing a common framework in which both PER and classical models can be expressed, this work builds a bridge between the two. 1 Axioms Synthetic Domain Theory is the study of the dictum that domains are sets and all set-theoretic functions between domains are “continuous” or “computable.” Plainly we cannot mean “sets” in the classical sense, so we have have to work in an (elementary) topos E and by a set we mean an object of E. Since we intend to interpret recursion, we assume that E also h...

• Type: Conference
• Year: 1991
• Where: LICS
• Authors: Paul Taylor 0002
• Keywords: Automated Reasoning, Classical Domain Theory, Domain Theory, LICS 1991, Synthetic Domain Theory