General synthetic domain theory – a logical approach
General synthetic domain theory – a logical approach
复制标题
一般综合域理论——一种逻辑方法
DOI：
--
复制
发表时间：
1997
影响因子：
0.5
通讯作者：
T. Streicher
中科院分区：
文献类型：
--
作者：
Bernhard Reus;T. Streicher
综合域理论（Synthetic domain theory，SDT）是域理论的一个版本，其中所有函数都是连续的。在达纳·斯科特最初的建议之后，已经开发了几种SDT方法，这些方法是逻辑的或分类的，公理化的或面向模型的，并且要么专门针对斯科特域，要么旨在提供一个通用的理论，公理化迄今为止研究的各种域概念的共同结构。在雷乌斯和斯特雷彻（Streicher，1993）、雷乌斯（Reus，1995）和雷乌斯（Reus，1998）中，我们发展了SDT的逻辑和公理化版本，它的特殊之处在于它抓住了Domain Theory à la Scott的本质，但排除了例如稳定Domain Theory，因为它要求函数空间上的顺序是逐点的。在这篇文章中，我们将给出一个一般SDT的逻辑和公理说明，目的是掌握所有域概念的共同结构。如上述，基本逻辑是构造类型理论的一个充分表达的版本。我们从几个基本公理开始，这些公理产生了一个核心理论，在此基础上，我们研究了前域的各种概念（例如，完备和良好完备的S-空间（Longley和Simpson 1997）），定义了适当的域概念，并验证了域理论的通常归纳原理。虽然每个领域都有一个逻辑上可定义的“专门化顺序”，但我们在公理和定理的表述中尽可能地避免顺序理论的概念。原因是函数空间上的序不能要求是逐点的，因为这将排除贝里稳定域的模型。逻辑语言的使用--被理解为类型论的某些范畴模型的内部语言--避免了在纯粹范畴方法中普遍存在的内部观点和外部观点的令人恼火的共存。因此，本文的目的是提供一个基本的介绍合成域理论，虽然需要一些基本类型理论的知识。
Synthetic domain theory (SDT) is a version of Domain Theory where ‘all functions are continuous’. Following the original suggestion of Dana Scott, several approaches to SDT have been developed that are logical or categorical, axiomatic or model-oriented in character and that are either specialised towards Scott domains or aim at providing a general theory axiomatising the structure common to the various notions of domains studied so far. In Reus and Streicher (1993), Reus (1995) and Reus (1998), we have developed a logical and axiomatic version of SDT, which is special in the sense that it captures the essence of Domain Theory à la Scott but rules out, for example, Stable Domain Theory, as it requires order on function spaces to be pointwise. In this article we will give a logical and axiomatic account of a general SDT with the aim of grasping the structure common to all notions of domains. As in loc.cit., the underlying logic is a sufficiently expressive version of constructive type theory. We start with a few basic axioms giving rise to a core theory on top of which we study various notions of predomains (such as, for example, complete and well-complete S-spaces (Longley and Simpson 1997)), define the appropriate notion of domain and verify the usual induction principles of domain theory. Although each domain carries a logically definable ‘specialization order’, we avoid order-theoretic notions as much as possible in the formulation of axioms and theorems. The reason is that the order on function spaces cannot be required to be pointwise, as this would rule out the model of stable domains à la Berry. The consequent use of logical language – understood as the internal language of some categorical model of type theory – avoids the irritating coexistence of the internal and the external view pervading purely categorical approaches. Therefore, the paper is aimed at providing an elementary introduction to synthetic domain theory, albeit requiring some knowledge of basic type theory.