Inductive Construction of Repletion |
| |
Authors: | Thomas Streicher |
| |
Institution: | (1) Departments of Mathematics, TH Darmstadt, Schlossgartenstraße 7, D-64289 Darmstadt, Germany. e-mail |
| |
Abstract: | The aim of this paper is to give a purely logical construction of repletion, i.e. the reflection of an arbitrary set to a replete one. Replete sets within constructive logic were introduced independently by M. Hyland and P. Taylor as the most restrictive but sufficiently general notion of predomain suitable for the purposes of denotational semantics à la Scott.For any set A its repletion R(A) appears as an inductively defined subset of S2(A) (A S) S which can be expressed within the internal language of a model of type theory. More explicitly, R(A) is the least subset of S2(A) containing all point filters and closed under a class of generalised limit processes . Improvements of our construction arise from several results saying that it suffices for the purpose of repletion to consider more restrictive classes of generalised limit processes . |
| |
Keywords: | synthetic domain theory constructive logic inductive definitions denotational semantics |
本文献已被 SpringerLink 等数据库收录! |
|