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, (), 122-130
[2] Barendregt, H.P., The lambda calculus: its syntax and semantics, () · Zbl 0467.03010
[3] Bracho, F., Continuously generated fixed-points, () · Zbl 0679.68148
[4] Gunter, C.A., Profinite solutions for recursive domain equations, ()
[5] Hennessy, M.; Plotkin, G.D., Full abstraction for a simple parallel programming language, (), 108-120 · Zbl 0457.68006
[6] Hrbacek, K., Powerdomain construction in the category of algebraic lattices, (), 281-289
[7] Huwig, H.; Poigné, A., A note on inconsistencies caused by fix-points in a Cartesian closed category, (1986), Manuscript
[8] {\scKamimura, T., and Tang, A.} (in press). Finitely continuous posets, Theoret. Comput. Sci.
[9] Kanda, A., Fully effective solutions of recursive domain equations, () · Zbl 0404.68008
[10] Kanda, A., Effective solutions of recursive domain equations, () · 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, () · Zbl 0642.03002
[13] Lawvere, F.W., Diagonal arguments and Cartesian closed categories, () · Zbl 0218.18002
[14] MacQueen, D.; Plotkin, G.D.; Sethi, R., An ideal model for recursive polymorphic types, (), 165-174
[15] Mulmuley, K., Full abstraction and semantic equivalence, () · 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, ()
[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, (), 252-265
[20] Scott, D.S., Continuous lattices, (), 97-136
[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, () · Zbl 0516.68064
[23] Scott, D.S., Some ordered sets in computer science, (), 677-718
[24] Scott, D.S., Domains for denotational semantics, (), 577-613
[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, (), 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.