On domains witnessing increase in information
Keywords:Scott domain, dI-domains, semi-regular topology, programming language semantics, recursive domain equations, dependent product, dependent sum, lambda calculus
The paper considers algebraic directed-complete partial orders with a semi-regular Scott topology, called regular domains. As is well know, the category of Scott domains and continuous maps is Cartesian closed. This is no longer true, if the domains are required to be regular. Two Cartesian closed subcategories of the regular Scott domains are exhibited: regular dI-domains with stable maps and strongly regular Scott domains with continuous maps. Here a Scott domains is strongly regular if all of its compact open subsets are regular open. In one considers only embeddings of dependent products and sums. Moreover, they are w-cocomplete and their object classes are closed under several constructions used in programming language semantics. It follows that recursive domains equations can be solved and models of typed and untyped lambda calculi can be constructed. Both kinds of domains can be udes in giving meaning to programming language constructs.
S. Abramsky and A. Jung, Domain theory, in: S. Abramsky, D. M. Gabbay and T. S. E. Maibaum, eds., Handbook of Logic in Computer Science, Vol. 3, Semantic Structures, Oxford University Press, Oxford, 1994, 1-168.
R. M. Amadio and P.-L. Curien, Domains and Lambda-Calculi, Cambridge University Press, Cambridge, 1998. https://doi.org/10.1017/CBO9780511983504
H. Barendregt, The Lambda Calculus, Its Syntax and Semantics, North-Holland, Amsterdam, 1984.
G. Berry, Stable models of typed lambda-calculi, in: G. Ausiello and C. Böhm, eds., Automata, Languages, and Programming, 5th Colloquium, Lec. Notes Comp. Sci. 62, Springer-Verlag, Berlin, 1978, 72-89. https://doi.org/10.1007/3-540-08860-1_7
T. Coquand, C. Gunter and G. Winskel, Domain theoretic models of polymorphism, Inform. and Comput. 81 (1989), 123-167. https://doi.org/10.1016/0890-5401(89)90068-0
Yu. L. Ershov, Computable functionals of finite type, Algebra I Logika 11 (1972), 367-437. https://doi.org/10.1007/BF02219096
English translation: Algebra and Logic 11 (1972), 203-242. https://doi.org/10.1007/BF02219096
C. A. Gunter, Semantics of Programming Languages, MIT Press, Cambridge, MA, 1992.
C. A. Gunter and D. S. Scott, Semantic Domains, in: J. van Leeuwen, ed., Handbook of Theoretical Computer Science, Vol. B, Formal Models and Semantics, Elsevier, Amsterdam, 1990, 633-674.
A. Jung, Notes on existential domains, manuscript, 1992.
E. Palmgren and V. Stoltenberg-Hansen, Domain interpretations of Martin-Löf's partial type theory, Ann. Pure Appl. Logic 48 (1990), 135-196. https://doi.org/10.1016/0168-0072(90)90044-3
G. D. Plotkin, A powerdomain construction, SIAM J. Comput. 5 (1976), 452-487. https://doi.org/10.1137/0205035
D. S. Scott, Outline of a mathematical theory of computation, in: 4th Annual Princeton Conference on Information Sciences and Systems, 1970, 169-176.
M. B. Smyth and G. D. Plotkin, The category-theoretic solution of recursive domain equations, SIAM J. Comput. 11 (1982), 761-783. https://doi.org/10.1137/0211062
V. Stoltenberg-Hansen, I. Lindström and E. R. Griffor, Mathematical Theory of Domains, Cambridge University Press, Cambridge, 1994. https://doi.org/10.1017/CBO9781139166386
G.-Q. Zhang, Logic of Domains, Birkhäuser, Boston, 1991. https://doi.org/10.1007/978-1-4612-0445-9
How to Cite
This journal is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.