Bounded complete domains and their logical form. (English) Zbl 07629149
Summary: We establish a framework of approximable disjunctive sequent calculus, which is sound and complete with respect to approximable FD-algebras. We show that the category of approximable FD-algebras with approximable mappings is equivalent to that of bounded complete domains with Scott continuous functions. This extends Abramsky’s logical representation of Scott domains as domain prelocales to a continuous setting. We also consider some domain constructions applied to approximable FD-algebras and show how to construct the approximable FD-algebras we need for defining the semantics of programming languages. According to a substructure relation, we define a pointed \(\omega\)-chain complete class of approximable FD-algebras, on which the domain constructions are made continuous and then the initial solutions to recursive domain equations are transformed into the fixed-points of such continuous functions.
MSC:
| 68Qxx | Theory of computing |
Keywords:
domain theory; bounded complete domains; approximable FD-algebras; stable open sets; domain equationsReferences:
| [1] | Abramsky, S., Domain Theory and the Logic of Observable Properties (1987), University of London, Ph.D. Thesis |
| [2] | Abramsky, S., Domain theory in logical form, Ann. Pure Appl. Log., 51, 1-77 (1991) · Zbl 0737.03006 |
| [3] | Andradi, H.; Ho, W. K., A topological Scott convergence theorem, Log. Methods Comput. Sci., 15, 1-29 (2019) · Zbl 1415.54001 |
| [4] | Bonsangue, M.; Kok, J., Toward an infinitary logic of domains: Abramsky logic for transition systems, Inf. Comput., 155, 170-201 (1999) · Zbl 1004.03030 |
| [5] | Chen, Y.; Jung, A., A logical approach to stable domains, Theor. Comput. Sci., 368, 124-148 (2006) · Zbl 1105.03026 |
| [6] | Edalat, A., Domains for computation in mathematics, physics and exact real arithmetic, Bull. Symb. Log., 3, 4, 401-452 (1997) · Zbl 0946.03055 |
| [7] | Gierz, G.; Hofmann, K. H.; Keimel, K.; Lawson, J. D.; Mislove, M.; Scott, D. S., Continuous Lattices and Domains (2003), Cambridge University Press · Zbl 1088.06001 |
| [8] | Goubault-Larrecq, J., Non-Hausdorff Topology and Domain Theory (2013), Cambridge University Press · Zbl 1280.54002 |
| [9] | He, Q.; Xu, L., Weak algebraic information systems and a new equivalent category of DOM of domains, Theor. Comput. Sci., 763, 1-19 (2019) · Zbl 1411.68055 |
| [10] | Huang, M.; Zhou, X.; Li, Q., Re-visiting axioms of information systems, Inf. Comput., 247, 130-140 (2015) · Zbl 1336.68159 |
| [11] | Jung, A.; Kegelmann, M.; Moshier, M. A., Multi lingual sequent calculus and coherent spaces, Fundam. Inform., 37, 369-412 (1999) · Zbl 0935.68068 |
| [12] | Jung, A., Continuous Domain Theory in Logical Form, Lecture Notes in Computer Science, vol. 7860, 166-177 (2013), Springer Verlag · Zbl 1264.68106 |
| [13] | Keimel, K.; Plotkin, G. D., Mixed powerdomains for probability and nondeterminism, Log. Methods Comput. Sci., 13, 1-84 (2017) · Zbl 1448.06002 |
| [14] | Larsen, K. G.; Winskel, G., Using information systems to solve recursive domain equations effectively, Inf. Comput., 91, 232-258 (1991) · Zbl 0731.68071 |
| [15] | Lawson, J. D., Spaces of maximal points, Math. Struct. Comput. Sci., 7, 543-555 (1997) · Zbl 0985.54025 |
| [16] | Li, Q.; Guo, L., Formal query systems on contexts and a representation of algebraic lattices, Inf. Sci., 239, 72-84 (2013) · Zbl 1320.68174 |
| [17] | Rounds, W.; Zhang, G., Clausal logic and logic programming in algebraic domains, Inf. Comput., 171, 183-200 (2001) · Zbl 1005.68094 |
| [18] | Scott, D. S., Domains for Denotational Semantics, Lecture Notes in Computer Science, vol. 140, 577-613 (1982), Springer Verlag · Zbl 0495.68025 |
| [19] | Simpson, A.; Voorneveld, N., Behavioural equivalence via modalities for algebraic effects, ACM Trans. Program. Lang. Syst., 42, 1-45 (2019) |
| [20] | Spreen, D.; Xu, L.; Mao, X., Information systems revisited: the general continuous case, Theor. Comput. Sci., 405, 176-187 (2008) · Zbl 1158.68023 |
| [21] | Spreen, D., Generalised information systems capture L-domains, Theor. Comput. Sci., 869, 1-28 (2021) · Zbl 1502.68174 |
| [22] | Sünderhauf, P., Discrete Approximation of Spaces (1994), Technische Hochschule Darmstadt, Ph.D. Thesis |
| [23] | Wang, L.; Li, Q., A logic for Lawson compact algebraic L-domains, Theor. Comput. Sci., 813, 410-427 (2020) · Zbl 1481.03012 |
| [24] | Wang, L.; Li, Q., Representations of stably continuous semi-lattices by information systems and abstract bases, Inf. Process. Lett., 165, Article 106036 pp. (2021) · Zbl 1506.68052 |
| [25] | Wang, L.; Guo, L.; Li, Q., Continuous domains in Formal Concept Analysis, Fundam. Inform., 179, 295-319 (2021) · Zbl 1519.68267 |
| [26] | Wang, L.; Li, Q.; Zhou, X., Continuous L-domains in logical form, Ann. Pure Appl. Log., 172, Article 102993 pp. (2021) · Zbl 1532.03048 |
| [27] | Wang, L.; Li, Q., Consistent disjunctive sequent calculi and Scott domains (2021), Mathematical Structures in Computer Science |
| [28] | Xia, C.; Zhao, B., A categorical characterization of the least Q-quantale completion of Q-ordered semigroups, Fuzzy Sets Syst., 382, 129-141 (2020) · Zbl 1465.06009 |
| [29] | Zhang, G. Q., Disjunctive Systems and L-Domains, Lecture Notes in Computer Science, vol. 623, 284-295 (1992), Springer Verlag · Zbl 1425.68244 |
| [30] | Zhao, D. S., Closure spaces and completions of posets, Semigroup Forum, 90, 2, 545-555 (2015) · Zbl 1467.06001 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
