Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality |
| |
Authors: | Geir Waagbø |
| |
Institution: | (1) Department of Mathematics, University of Oslo, Postboks 1053, Blindern, N-0316 Oslo, Norway , NO |
| |
Abstract: | A modified version of Normann's hierarchy of domains with totality 9] is presented and is shown to be suitable for interpretation
of Martin-L?f's intuitionistic type theory. This gives an interpretation within classical set theory, which is natural in
the sense that -types are interpreted as sets of pairs and -types as sets of choice functions. The hierarchy admits a natural definition of the total objects in the domains, and following
an idea of Berger 3] this makes possible an interpretation where a type is defined to be true if its interpretation contains
a total object. In particular, the empty type contains no total objects and will therefore be false (in any non-empty context). In
addition, there is a natural equivalence relation on the total objects, so we derive a hierarchy of topological spaces (quotient
spaces wrt. the Scott topology), and give a second interpretation using this hierarchy.
Received: 11 December 1995 / Revised version: 14 October 1996 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|