Skip to main content
SpringerLink
Log in

Cpo's do not form a cpo, and yet recursion works

  • Papers
  • Conference paper
  • First Online:
Book cover VDM'91 Formal Software Development Methods (VDM 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 551))

Included in the following conference series:

  • 113 Accesses

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

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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.

    Google Scholar 

  2. 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.

    Google Scholar 

  3. Dines Bjørner and Cliff B. Jones. The Vienna Development Method: The Meta-Language, volume 61 of LNCS. Springer-Verlag, 1978.

    Google Scholar 

  4. Dines Bjørner and Cliff B. Jones. Formal Specification of Software Development. Prentice Hall, Englewood Cliffs, 1982.

    Google Scholar 

  5. Andrzej J. Blikle. MetaSoft Primer. Towards a Metalanguage of Applied Denotational Semantics, volume 288 of LNCS. Springer-Verlag, 1987.

    Google Scholar 

  6. Andrzej J. Blikle and Andrzej Tarlecki. Naive denotational semantics. In Proceedings IFIP Congress 1983. North Holland, 1983.

    Google Scholar 

  7. Bruno Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.

    Google Scholar 

  8. Carl Gunter and Achim Jung. Coherence and consistency in domains. In 3rd IEEE Symposium on Logic in Computer Science, pages 309–317. IEEE, 1988.

    Google Scholar 

  9. 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.

    Google Scholar 

  10. 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.

    Google Scholar 

  11. 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.

    Google Scholar 

  12. 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.

    Google Scholar 

  13. Gordon Plotkin. Domains. Postgraduate Course—Lecture Notes, Edinburgh University, 1985.

    Google Scholar 

  14. M. B. Smyth. Quasi-uniformities: Reconciling domains with metric spaces. LNCS vol. 298, 1987.

    Google Scholar 

  15. 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.

    Google Scholar 

  16. 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Polish Academy of Sciences, ul. Jaśkowa Dolina 31, P.O.Box 562, 80252, Gdańsk, Poland

    Marek A. Bednarczyk & Andrzej M. Borzyszkowski

Authors
  1. Marek A. Bednarczyk
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrzej M. Borzyszkowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

S. Prehn W. J. Toetenel

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation