Hostname: page-component-cd9895bd7-gxg78 Total loading time: 0 Render date: 2024-12-26T18:13:13.306Z Has data issue: false hasContentIssue false
  • English
  • Français

Consistent disjunctive sequent calculi and Scott domains

Published online by Cambridge University Press:  17 August 2021

Longchun Wang Open the ORCID record for Longchun Wang [Opens in a new window]  and
Qingguo Li Open the ORCID record for Qingguo Li [Opens in a new window]
Longchun Wang
Affiliation:
School of Mathematics, Hunan University, Changsha410086, China School of Mathematical Sciences, Qufu Normal University, Qufu273165, China
Qingguo Li*
Affiliation:
School of Mathematics, Hunan University, Changsha410086, China
*
*Corresponding author. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Based on the framework of disjunctive propositional logic, we first provide a syntactic representation for Scott domains. Precisely, we establish a category of consistent disjunctive sequent calculi with consequence relations, and show it is equivalent to that of Scott domains with Scott-continuous functions. Furthermore, we illustrate the approach to solving recursive domain equations by introducing some standard domain constructions, such as lifting and sums. The subsystems relation on consistent finitary disjunctive sequent calculi makes these domain constructions continuous. Solutions to recursive domain equations are given by constructing the least fixed point of a continuous function.

Keywords

Consistent disjunctive sequent calculusScott domaincategorical equivalencefixed pointdomain equation
Type
Special Issue: Theory and Applications of Models of Computation (TAMC 2020)
Information
Mathematical Structures in Computer Science , Volume 32 , Issue 2: Theory and Applications of Models of Computation (TAMC 2020) , February 2022 , pp. 127 - 150
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abramsky, S. (1987). Domain Theory and the Logic of Observable Properties. Phd thesis, University of London.Google Scholar
Abramsky, S. (1991). Domain theory in logical form. Annals of Pure and Applied Logic 51 1–77.CrossRefGoogle Scholar
Chen, Y. and Jung, A. (2006). A logical approach to stable Domains. Theoretical Computer Science 368 124–148.CrossRefGoogle Scholar
Davey, B. A. and Priestley, H. A. (2002). Introduction to Lattices and Order, Cambridge, Cambridge University Press.CrossRefGoogle Scholar
Erné, M. (2018). Categories of locally hypercompact spaces and quasicontinuous posets. Applied Categorical Structures 26 (5) 823–854.CrossRefGoogle Scholar
Gallier, J. H. (2015). Logic for Computer Science: Foundations of Automatic Theorem Proving, New York, Courier Dover Publications.Google Scholar
Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. and Scott, D. S. (2003). Continuous Lattices and Domains, Cambridge, Cambridge University Press.CrossRefGoogle Scholar
Goubault-Larrecq, J. (2013). Non-Hausdorff Topology and Domain Theory , New Mathematical Monographs, vol. 22, Cambridge, Cambridge University Press.Google Scholar
Ho, W., Goubault-Larrecq, J., Jung, A. and Xi, X. (2018). The Ho-Zhao problem. Logical Methods in Computer Science 14 (1:7) 1–19.Google Scholar
Hoofman, R. (1993). Continuous information systems. Information and Computation 105 42–71.CrossRefGoogle Scholar
Huang, M., Zhou, X. and Li, Q. (2015). Re-visiting axioms of information systems. Information and Compution 247 130–140.CrossRefGoogle Scholar
Jung, A., Kegelmann, M. and Moshier, M. A. (1999). Multi lingual sequent calculus and coherent spaces. Fundamenta Informaticae 37 369–412.CrossRefGoogle Scholar
Jung, A. (2013). Continuous Domain Theory in Logical Form, Lecture Notes in Computer Science, vol. 7860, Springer Verlag, 166–177.Google Scholar
Larsen, K. G. and Winskel, G. (1984). Using Information Systems to Solve Recursive Domain Equations Effectively, Lecture Notes in Computer Science, vol. 173, Springer Verlag, 109–130.Google Scholar
Scott, D. S. (1982). Domains for Denotational Semantics, Lecture Notes in Computer Science, vol. 140, Springer Verlag, 577–613.Google Scholar
Spreen, D., Xu, L. and Mao, X. (2008). Information systems revisited: The general continuous case. Theoretical Computer Science 405 176–187.CrossRefGoogle Scholar
Vickers, S. (2004). Entailment systems for stably locally compact locales. Theoretical Computer Science 316 259–296.CrossRefGoogle Scholar
Wang, L. and Li, Q. (2020a). A representation of proper BC domains based on conjunctive sequent calculi. Mathematical Structures in Computer Science 30 1–13.CrossRefGoogle Scholar
Wang, L. and Li, Q. (2020b). A logic for Lawson compact algebraic L-domains. Theoretical Computer Science 813 410–327.CrossRefGoogle Scholar
Wang, L. and Li, Q. (2021). Representations of stably continuous semi-lattices by information systems and abstract bases. Information Processing Letters 165 106036.CrossRefGoogle Scholar
Wu, M., Guo, L. and Li, Q. (2016). A representation of L-domains by information system. Theoretical Computer Science 612 126–136.CrossRefGoogle Scholar
Yao, W. (2016). A categorical isomorphism between injective stratified fuzzy T 0 spaces and fuzzy continuous lattices. IEEE Transactions on Fuzzy Systems 24 (1) 131–139.Google Scholar
Zhang, G. (1992). Disjunctive Systems and L-Domains, Lecture Notes in Computer Science, vol. 623, Springer Verlag, 284–295.Google Scholar