Universal profinite domains. (English) Zbl 0628.68050

The author introduces and studies the profinite domains in the order- theoretic approach to programming semantics. The mathematical problem of the existence of a profinite universal domain is investigated. Thus, the paper provides and explains a technique for constructing an infinite class of universal profinite domains. The category of profinite domains and continuous functions is shown to be bicartesian closed and necessary conditions are provided for the existence of solutions of domain equations within this category. According to the author, “this is a rather natural, and in a sense inevitable, category which contains SFP (see Plotkin, 1976) as a full subcategory”. An approach similar to information systems is extended to categories larger than the one considered by Scott.
Reviewer: G.Ciobanu


68Q99 Theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
18B35 Preorders, orders, domains and lattices (viewed as categories)
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
Full Text: DOI


[1] Amadio, R.; Bruce, K.; Longo, G., The finitary projection model for second order lambda calculus and solutions to higher order domain equations, (Logic in Computer Science (1986), IEEE Computer Society: IEEE Computer Society New York), 122-130
[2] Barendregt, H. P., The Lambda Calculus: Its Syntax and Semantics, (Studies in Logic and The Foundations of Mathematics, Vol. 103 (1984), North-Holland: North-Holland Amsterdam) · Zbl 0467.03010
[3] Bracho, F., Continuously Generated Fixed-Points, (Doctoral dissertation (1983), Oxford University: Oxford University Oxford) · Zbl 0679.68148
[4] Gunter, C. A., Profinite Solutions for Recursive Domain Equations, (Doctoral dissertation (1985), Univ. of Wisconsin at Madison)
[5] Hennessy, M.; Plotkin, G. D., Full abstraction for a simple parallel programming language, (Mathematical Foundations of Computer Science. Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 74 (1979), Springer-Verlag: Springer-Verlag Berlin), 108-120 · Zbl 0457.68006
[6] Hrbacek, K., Powerdomain construction in the category of algebraic lattices, (Brauer, W., Automata, Languages and Programming. Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 194 (1985), Springer-Verlag: Springer-Verlag Berlin), 281-289 · Zbl 0573.68003
[7] Huwig, H.; Poigné, A., A note on inconsistencies caused by fix-points in a cartesian closed category (1986), Manuscript
[8] Kamimura, T., and Tang, A.Theoret. Comput. Sci.; Kamimura, T., and Tang, A.Theoret. Comput. Sci.
[9] Kanda, A., Fully effective solutions of recursive domain equations, (Bečv́ař, J., Mathematical Foundations of Computer Science. Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 74 (1979), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0404.68008
[10] Kanda, A., Effective Solutions of Recursive Domain Equations, (Doctoral dissertation (1980), Warwick University) · Zbl 0404.68008
[11] Koymans, C. P.J., Models of the lambda calculus, Inform. Contr., 52, 306-332 (1982) · Zbl 0542.03004
[12] Lambek, J.; Scott, P. J., Introduction to Higher-Order Categorical Logic, (Cambridge Studies in Advanced Mathematics, Vol. 7 (1986), Cambridge Univ. Press: Cambridge Univ. Press London) · Zbl 0642.03002
[13] Lawvere, F. W., Diagonal arguments and cartesian closed categories, (Category Theory, Homology Theory and their Aplications II. Category Theory, Homology Theory and their Aplications II, Lecture Notes in Mathematics, Vol. 92 (1969), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0218.18002
[14] MacQueen, D.; Plotkin, G. D.; Sethi, R., An ideal model for recursive polymorphic types, (Kennedy, K., Principles of Programming Languages (1984), Association for Computing Machinery: Association for Computing Machinery New York), 165-174
[15] Mulmuley, K., Full Abstraction and Semantic Equivalence, (Doctoral dissertation (1985), Carnegie-Mellon Univ: Carnegie-Mellon Univ Pittsburgh) · Zbl 0857.68056
[16] Plotkin, G. D., A powerdomain construction, SIAM J. Comput, 5, 452-487 (1976) · Zbl 0355.68015
[17] Plotkin, G. D., The category of complete partial orders: A tool for making meaning, (Summer School on Foundations of Artificial Intelligence and Computer Science (1978), Instituto di Scienze dell’ Informazione: Instituto di Scienze dell’ Informazione University di Pisa)
[18] Plotkin, G. D., \(T^ω\) as a universal domain, J. Comput. System Sci., 17, 209-236 (1978) · Zbl 0419.03007
[19] Poigné, A., A note on distributive laws and power domains, (Category Theory and Computer Programming. Category Theory and Computer Programming, Lecture Notes in Computer Science, Vol. 240 (1986), Springer-Verlag: Springer-Verlag Berlin), 252-265 · Zbl 0634.18001
[20] Scott, D. S., Continuous lattices, (Lawvere, F. W., Toposes, Algebraic Geometry and Logic. Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics, Vol. 274 (1976), Springer-Verlag: Springer-Verlag Berlin), 97-136 · Zbl 0239.54006
[21] Scott, D. S., Data types as lattices, SIAM J. Comput., 5, 522-587 (1976) · Zbl 0337.02018
[22] Scott, D. S., Lectures on a Mathematical Theory of Computation, (Technical Report, No. PRG-19 (1981), Oxford Univ. Computing Laboratory) · Zbl 0516.68064
[23] Scott, D. S., Some ordered sets in computer science, (Rival, I., Ordered Sets (1981), Reidel: Reidel Dordrecht), 677-718 · Zbl 0497.06001
[24] Scott, D. S., Domains for denotational semantics, (Nielsen, M.; Schmidt, E. M., Automata, Languages and Programming. Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 140 (1982), Springer-Verlag: Springer-Verlag Berlin), 577-613 · Zbl 0495.68025
[25] Scott, D. S., Notes on cpo’s/SFP-objects and the like (1982), Manuscript, unpublished
[26] Smyth, M. B., Powerdomains, J. Comput. System Sci., 16, 23-36 (1978) · Zbl 0408.68017
[27] Smyth, M. B., The largest cartesian closed category of domains, Theoret. Comput. Sci., 27, 109-119 (1983) · Zbl 0556.68017
[28] Smyth, M. B.; Plotkin, G. D., The category-theoretic solution of recursive domain equations, SIAM J. Comput., 11, 761-783 (1982) · Zbl 0493.68022
[29] Winskel, G.; Larsen, K., Using information systems to solve recursive domain equations effectively, (Kahn, G.; Plotkin, G. D., Semantics of Data Types. Semantics of Data Types, Lecture Notes in Computer Science, Vol. 173 (1984), Springer-Verlag: Springer-Verlag Berlin), 109-130 · Zbl 0539.68019
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.