A synthetic theory of sequential domains

详细信息	查看全文 | 推荐本文 |

• 作者：Bernhard Reus^a ; ^{bernhard@sussex.ac.uk} ; Thomas Streicher^b ; ^{streicher@mathematik.tu-darmstadt.de}
• 关键词：68Q10 ; 68Q55 ; 68Q70
• 刊名：Annals of Pure and Applied Logic
• 出版年：2012
• 期刊代码：4_01680072
• 类别：cp
• 出版时间：August, 2012
• 卷：163
• 期：8
• 页码：1062-1074
• 文件大小：296 K

摘要

Synthetic Domain Theory (SDT) was originally suggested by Dana Scott as a uniform and logic based account of domain theory. In SDT the domain structure is intrinsic to a chosen class of sets with 鈥済ood鈥?properties.

General SDT has a lot of different models which differ w.r.t.聽the ambient logic but also w.r.t.聽the PCF hierarchy, i.e.聽the finite type hierarchy over the partial natural numbers. From the early days of SDT we know satisfactory axiomatizations of SDT 脿 la Scott which enforce the existence of 鈥減arallel or鈥? A realizability model for SDT where the PCF hierarchy coincides with the strongly stable model of Bucciarelli and Ehrhard has been found independently by van Oosten (1999) and Longley (2002) . Their model is based on the typed partial combinatory algebra of concrete data structures and sequential algorithms.

In this paper, we try to axiomatize this kind of Sequential SDT for the first time. Our approach is based on replacing by , the observably sequential algorithms, as suggested by Cartwright et聽al. (1994) . The axioms are inspired by the realizability model over and its type of observations with two global elements standing for nontermination and termination with error, respectively. Unlike in traditional domain theory this type is not a dominance because binary infimum is not available as an operation. This forces us to adapt some of the basic machinery of SDT.