科研之友
微信
新浪微博
Facebook
分享链接
摘要
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 %26quot;good%26quot; properties. %26lt;br%26gt;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 a la Scott which enforce the existence of %26quot;parallel or%26quot;. 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) [24] and Longley (2002) [13]. Their model is based on the typed partial combinatory algebra SA of concrete data structures and sequential algorithms. %26lt;br%26gt;In this paper, we try to axiomatize this kind of Sequential SDT for the first time. Our approach is based on replacing SA by OSA, the observably sequential algorithms, as suggested by Cartwright et al. (1994) [3]. The axioms are inspired by the realizability model over OSA, and its type O 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.
- 出版日期2012-8
