Abstract
We consider type universes as examples of regular algebras in the area of the denotational semantics of programming languages. The paper concentrates on our method which was used implicitly in the studies of the domain universes underlying MetaSoft, cf. [BBP90], and BSI/VDM, cf. [TW90].
Technically speaking the method allows to prove that a given algebra, e.g., an algebra of types, is regular. It is demonstrated by means of an example that the method applies even to universes which are essentially regular, i.e., which are neither cpo's, nor the images of the initial regular algebra.
Sponsored by the Polish Academy of Sciences, project MetaSoft, grant CPBP 02.17
Preview
Unable to display preview. Download preview PDF.
References
J. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. An initial algebra semantics and continuous algebras. Journal of the ACM, 24(1):68–95, January 1977.
Marek A. Bednarczyk, Andrzej M. Borzyszkowski, and Wiesław Pawłowski. Towards the semantics of the definitional language of MetaSoft. In Dines Bjørner, editor, VDM & Z: Formal Methods in Software Development, 3rd VDM-Europe Symposium, Kiel, pages 477–503. LNCS, vol. 428, Springer-Verlag, 1990.
Dines Bjørner and Cliff B. Jones. The Vienna Development Method: The Meta-Language, volume 61 of LNCS. Springer-Verlag, 1978.
Dines Bjørner and Cliff B. Jones. Formal Specification of Software Development. Prentice Hall, Englewood Cliffs, 1982.
Andrzej J. Blikle. MetaSoft Primer. Towards a Metalanguage of Applied Denotational Semantics, volume 288 of LNCS. Springer-Verlag, 1987.
Andrzej J. Blikle and Andrzej Tarlecki. Naive denotational semantics. In Proceedings IFIP Congress 1983. North Holland, 1983.
Bruno Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.
Carl Gunter and Achim Jung. Coherence and consistency in domains. In 3rd IEEE Symposium on Logic in Computer Science, pages 309–317. IEEE, 1988.
Peter Gorm Larsen, editor. The dynamic semantics of the BSI/VDM specification language. Technical report, IFAD, Munkebjærgvænget 17, DK-5230 Odense M, Denmark, July 1990.
Hagen Huwig and Axal Poigné. A note on inconsistencies caused by fixed-points in a cartesian closed category. Theoretical Computer Science, 73:101–112, 1990.
Brian Q. Monahan. A type model for VDM. In Dines Bjørner and Cliff B. Jones, editors, VDM—A Formal Method at Work, VDM-Europe Symposium, Brussels, pages 210–236. LNCS, vol. 252, Springer-Verlag, 1987.
M. Nielsen, K. Havelund, K. R. Wagner, and C. George. The RAISE language, methods and tools. In R. Bloomfield, R. Jones, and L. Marshall, editors, VDM: The Way Ahead, 2nd VDM-Europe Symposium, Dublin, pages 376–405. LNCS, vol. 328, Springer-Verlag, 1988.
Gordon Plotkin. Domains. Postgraduate Course—Lecture Notes, Edinburgh University, 1985.
M. B. Smyth. Quasi-uniformities: Reconciling domains with metric spaces. LNCS vol. 298, 1987.
J. Tiuryn. Fixed points and algebras with infinitely long expressions. Part I. Fundamenta Informatics, 2(1):103–128, 1978. also in Proceedings MFCS'77, LNCS, vol. 53, 1977.
Andrzej Tarlecki and Morten Wieth. A naive domain universe for VDM. In Dines Bjørner, editor, VDM & Z: Formal Methods in Software Development, 3rd VDM-Europe Symposium, Kiel, pages 552–579. LNCS, vol. 428, Springer-Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bednarczyk, M.A., Borzyszkowski, A.M. (1991). Cpo's do not form a cpo, and yet recursion works. In: Prehn, S., Toetenel, W.J. (eds) VDM'91 Formal Software Development Methods. VDM 1991. Lecture Notes in Computer Science, vol 551. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54834-3_17
Download citation
DOI: https://doi.org/10.1007/3-540-54834-3_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54834-8
Online ISBN: 978-3-540-46449-5
eBook Packages: Springer Book Archive