research-article

Open access

Dually nondeterministic functions

Authors:

Joseph M. Morris,

Malcolm TyrrellAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 6

Article No.: 34, Pages 1 - 34

https://doi.org/10.1145/1391956.1391961

Published: 30 October 2008 Publication History

Abstract

Nondeterminacy is a fundamental notion in computing. We show that it can be described by a general theory that accounts for it in the form in which it occurs in many programming contexts, among them specifications, competing agents, data refinement, abstract interpretation, imperative programming, process algebras, and recursion theory. Underpinning these applications is a theory of nondeterministic functions; we construct such a theory. The theory consists of an algebra with which practitioners can reason about nondeterministic functions, and a denotational model to establish the soundness of the theory. The model is based on the idea of free completely distributive lattices over partially ordered sets. We deduce the important properties of nondeterministic functions.

References

[1]

Abramsky, S. and Jung, A. 1994. Domain theory. In Handbook of Logic in Computer Science, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, Eds. Vol. 3. Clarendon Press, 1--168.

Digital Library

[2]

Apt, K. R. and Plotkin, G. D. 1986. Countable nondeterminism and random assignment. J. ACM 33, 4, 724--767.

Digital Library

[3]

Back, R.-J. R. 1980. Correctness preserving program refinements: Proof theory and applications. Tract 131, Mathematisch Centrum, Amsterdam.

[4]

Back, R.-J. R. and von Wright, J. 1990. Duality in specification languages: a lattice-theoretical approach. Acta Inf. 27, 7, 583--625.

Digital Library

[5]

Back, R.-J. and von Wright, J. 1998. Refinement Calculus: A Systematic Introduction. Springer-Verlag, New York.

[6]

Bartenschlager, G. 1995. Free bounded distributive lattices over finite ordered sets and their skeletons. Acta Math. Univ. Comen. 64, 1--23.

[7]

Berry, G. 1978. Stable models of typed lambda-calculi. In Proceedings of the 5th Colloquium on Automata, Languages and Programming. Lecture Notes in Comput. Science, vol. 62. Springer-Verlag, New York, 72--89.

Digital Library

[8]

Bird, R. and de Moor, O. 1997. Algebra of Programming. Prentice Hall, London. ISBN 0-13-507245-X.

Digital Library

[9]

Birkhoff, G. 1967. Lattice Theory, 3rd ed. Colloquium Publications, vol. 25. American Mathematical Society.

[10]

Bois, A. R. D., Pointon, R., Loidl, H.-W., and Trinder, P. 2002. Implementing declarative parallel bottom-avoiding choice. In Proceedings of the 14th Symposium on Computer Architecture and High Performance Computing, A. F. de Souza, Ed. IEEE Computer Society Press, Los Alamitos, CA.

Digital Library

[11]

Bonsangue, M. 1998. Topological Duality in Semantics. Electronic Notes in Theoretical Computer Science, vol. 8. Elsevier, Amsterdam.

[12]

Bonsangue, M. M. and Kok, J. N. 1994. The weakest precondition calculus: Recursion and duality. Formal Asp. Comput. 6, 788--800.

[13]

Boute, R. T. 2005. Functional declarative language design and predicate calculus: a practical approach. ACM Trans. Program. Lang. Syst. 27, 5, 988--1047.

Digital Library

[14]

Broy, M. 1986. A theory for nondeterminism, parallelism, communication, and concurrency. Theoret. Comput. Sci. 45, 1, 1--61.

Digital Library

[15]

Cattani, G. L. and Winskel, G. 1996. Presheaf models for concurrency. In Computer Science Logic, D. van Dalen and M. Bezem, Eds. Lecture Notes in Computer Science, vol. 1258. Springer, 58--75.

Digital Library

[16]

Cousot, P. 1996. Abstract interpretation. ACM Comput. Surv. 28, 2, 324--328.

Digital Library

[17]

Davey, B. and Priestley, H. 2002. Introduction to Lattices and Order, 2nd ed. Cambridge University Press.

[18]

de Moor, O. and Gibbons, J. 2000. Invited talk: Pointwise relational programming. In Proceedings of the 8th International Conference on Algebraic Methodology and Software Technology. Lecture Notes in Computer Science. Vol. 1816. Springer-Verlag, New York, 371--390.

Digital Library

[19]

DeRoever, W.-P. and Engelhardt, K. 1999. Data Refinement: Model-Oriented Proof Methods and Their Comparison. Cambridge University Press, New York, NY, USA.

Digital Library

[20]

Dijkstra, E. W. 1976. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ.

Digital Library

[21]

Dijkstra, E. W. 1982. The equivalence of bounded nondeterminacy and continuity. In Selected Writings on Computing: A Personal Perspective, Springer-Verlag, New York.

Digital Library

[22]

Flannery, K. E. and Martin, J. J. 1990. The Hoare and Smith power domain constructors commute under composition. J. Comput. Syst. Sci. 40, 2, 125--135.

Digital Library

[23]

Freese, R., Jezek, J., and Nation, J. 1995. Free Lattices. Mathematical Surveys and Monographs, vol. 42. American Mathematical Society.

[24]

Gardiner, P. H. B., Martin, C. E., and de Moor, O. 1994. An algebraic construction of predicate transformers. Sci. Comput. Program. 22, 1-2, 21--44.

Digital Library

[25]

Gardiner, P. H. B. and Morgan, C. C. 1991. Data refinement of predicate transformers. Theoret. Comput. Sci. 87, 143--162.

Digital Library

[26]

Gries, D. and Schneider, F. B. 1993. A Logical Approach to Discrete Math. Springer-Verlag, New York.

Digital Library

[27]

Harmer, R. and McCusker, G. 1999. A fully abstract game semantics for finite nondeterminism. In Proceedings of the 14th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 422--430.

Digital Library

[28]

Heckmann, R. 1991a. Lower and upper power domain constructions commute on all cpos. Inf. Process. Lett. 40, 1, 7--11.

Digital Library

[29]

Heckmann, R. 1991b. Power domain constructions. Sci. Comput. Program. 17, 1-3, 77--117.

Digital Library

[30]

Heckmann, R. 1991c. An upper power domain construction in terms of strongly compact sets. In MFPS, S. D. Brookes, M. G. Main, A. Melton, M. W. Mislove, and D. A. Schmidt, Eds. Lecture Notes in Computer Science, vol. 598. Springer-Verlag, New York, 272--293.

Digital Library

[31]

Hehner, E. C. R. 1993. A Practical Theory of Programming. Springer Verlag, New York, London. 2nd ed. 2004 at http://www.cs.toronto.edu/~hehner/aPToP/.

Digital Library

[32]

Hennessy, M. and Plotkin, G. D. 1979. Full abstraction for a simple parallel programming language. In MFCS, J. Becvár, Ed. Lecture Notes in Computer Science, vol. 74. Springer, 108--120.

[33]

Hesselink, W. H. 1990. Modalities of nondeterminacy. In Beauty is our Business: A Birthday Salute to E.W. Dijkstra, W. H. J. Feijen, A. J. M. van Gasteren, D. Gries, and J. Misra, Eds. Springer-Verlag, New York, 182--192.

Digital Library

[34]

Hesselink, W. 2004. Multirelations are predicate transformers. Tech. rep., Dept. of Computing Science, University of Groningen, The Netherlands.

[35]

Hoare, C. A. R. 1984. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ.

Digital Library

[36]

Hoare, C. A. R., He, J., and Sanders, J. W. 1987. Prespecification in data refinement. Inf. Process. Lett. 25, 2, 71--76.

Digital Library

[37]

Hoofman, R. 1987. Powerdomains. Tech. Rep. RUU-CS-87-23, Institute of Information and Computing Sciences, Utrecht University.

[38]

Hoogerwoord, R. R. 1989. The design of functional programs: a calculational approach. Ph.D. thesis, Technische Universiteit Eindhoven.

[39]

Hughes, J. and Moran, A. 1995. Making choices lazily. In Proceedings of the 7th International Conference on Functional Programming Languages and Computer Architecture. ACM, New York, 108--119.

Digital Library

[40]

Hughes, J. and O'Donnell, J. 1991. Nondeterministic functional programming with sets. In Proceedings of the 4th Higher Order Workshop Banff 1990 (Sept. 10--14, 1990, Alberta, Bc, Canada). Springer-Verlag, New York.

[41]

Jacobs, D. and Gries, D. 1985. General correctness: A unification of partial and total correctness. Acta Inf. 22, 1, 67--83.

Digital Library

[42]

Jones, S. P., Reid, A., Henderson, F., Hoare, T., and Marlow, S. 1999. A semantics for imprecise exceptions. In Proceedings of the ACM SIGPLAN 1999 Conference on Programming Language Design and Implementation. ACM, New York, 25--36.

Digital Library

[43]

Laird, J. 2006. Bidomains and full abstraction for countable nondeterminism. In Proceedings of the Foundations of Software Science and Computation Structures 2006. Lecture Notes in Computer Science, vol. 3921. Springer-Verlag, New York.

Digital Library

[44]

Larsen, P. G. and Hansen, B. S. 1996. Semantics of under-determined expressions. Form. Asp. Comput. 8, 1, 47--66.

[45]

Lassen, S. B. 1998. Relational reasoning about functions and nondeterminism. Ph.D. dissertation. Dept of Computer Science, University of Aarhus.

[46]

Levy, P. B. 2005. Infinite trace equivalence. In Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science, vol. 155. Springer-Verlag, New York, 195--209.

Digital Library

[47]

Main, M. G. 1985. Free constructions of powerdomains. In Mathematical Foundations of Programming Semantics, A. Melton, Ed. Lecture Notes in Computer Science, vol. 239. Springer-Verlag, New York, 162--183.

Digital Library

[48]

Martin, C. E., Curtis, S. A., and Rewitzky, I. 2004. Modelling nondeterminism. In Proceedings of the 7th International Conference on Mathematics of Program Construction, D. Kozen and C. Shankland, Eds. Lecture Notes in Computer Science, vol. 3125. Springer-Verlag, New York, 228--251.

[49]

Morgan, C. 1988. The specification statement. ACM Trans. Prog. Lang. Syst. 10, 403--419.

Digital Library

[50]

Morgan, C. 1990. Programming from Specifications. Series in Computer Science. Prentice-Hall, Englewood Cliffs, NJ.

Digital Library

[51]

Morgan, C. and Gardiner, P. H. B. 1991. Data refinement by calculation. Acta Informatica 27, 481--503.

Digital Library

[52]

Morris, J. M. 1987. A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Prog. 9, 287--306.

Digital Library

[53]

Morris, J. M. 2004. Augmenting types with unbounded demonic and angelic nondeterminacy. In Proceedings of the 7th International Conference on Mathematics of Program Construction, D. Kozen and C. Shankland, Eds. Lecture Notes in Computer Science, vol. 3125. Springer-Verlag, New York, 274--288.

[54]

Morris, J. M. and Bunkenburg, A. 1999. Specificational functions. ACM Trans. Prog. Lang. Syst. 21, 677--701.

Digital Library

[55]

Morris, J. M. and Bunkenburg, A. 2002. A source of inconsistency in theories of nondeterministic functions. Sci. Comput. Program. 43, 1, 77--89.

Digital Library

[56]

Morris, J. M., Bunkenburg, A., and Tyrrell, M. 2008. Term transformers: A new approach to state. submitted.

[57]

Morris, J. M. and Tyrrell, M. 2007. Dual unbounded nondeterminacy, recursion, and fixpoints. Acta Inf. 44, 5, 323--344.

Digital Library

[58]

Naumann, D. A. 2001a. Ideal models for pointwise relational and state-free imperative programming. In Proceedings of the 3rd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. ACM, New York, 4--15.

Digital Library

[59]

Naumann, D. A. 2001b. Predicate transformer semantics of a higher-order imperative language with record subtyping. Sci. Comput. Prog. 41, 1, 1--51.

Digital Library

[60]

Nelson, G. 1992. Some generalizations and applications of Dijkstra's guarded commands. In Programming and Mathematical Method, M. Broy, Ed. NATO ASI Series F: Computer and Systems Sciences, vol. 88. Springer-Verlag New York.

[61]

Norvell, T. S. and Hehner, E. C. R. 1993. Logical specifications for functional programs. In Proceedings of the 2nd International Conference on Mathematics of Program Construction. Lecture Notes in Computer Science, vol. 669. Springer-Verlag, New York, 269--290.

Digital Library

[62]

Nygaard, M. and Winskel, G. 2002. Linearity in process languages. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, Press, Los Alamitos, CA, 433--441.

Digital Library

[63]

Nygaard, M. and Winskel, G. 2004. Domain theory for concurrency. Theoret. Comput. Sci. 316, 1, 153--190.

Digital Library

[64]

Partsch, H. A. 1990. Specification and Transformation of Programs. Springer-Verlag, New York.

Digital Library

[65]

Plotkin, G. 1976. A powerdomain construction. SIAM J. Comput. 5, 3, 452--487.

Digital Library

[66]

Plotkin, G. 1979. Dijkstra's predicate transformers and smyth's powerdomains. In Proceedings of the Copenhagen Winter School on Abstract Software Specifications, D. Bjorner, Ed. Lecture Notes in Computer Science, vol. 96. Springer-Verlag, New York, 527--553.

Digital Library

[67]

Reynolds, J. C. 1998. Theories of Programming Languages. Cambridge University Press, Cambridge, UK.

Digital Library

[68]

Roscoe, A. W. 1998. The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs, NJ.

Digital Library

[69]

Smyth, M. B. 1978. Power domains. J. Comput. Syst. Sci. 16, 1, 23--26.

[70]

Smyth, M. B. 1983. Power domains and predicate transformers: A topological view. In Proceedings of the 10th Colloquium on Automata, Languages and Programming, J. Diaz, Ed. Lecture Notes in Computer Science, vol. 153. Springer-Verlag, London, UK, 662--675.

Digital Library

[71]

Spivey, J. 1988. Understanding Z: A Specification Language and its Formal Semantics. Cambridge University Press, Cambridge, UK.

Digital Library

[72]

Tunnicliffe, W. R. 1985. The free completely distributive lattice over a poset. Algebra Univ. 21, 133--135.

[73]

Tyrrell, M., Morris, J. M., Butterfield, A., and Hughes, A. 2006. A lattice-theoretic model for an algebra of communicating sequential processes. In Proceedings of the 3rd International Colloquium on Theoretical Aspects of Computing, K. Barkaoui, A. Cavalcanti, and A. Cerone, Eds. Lecture Notes in Computing Science, vol. 4281. Springer-Verlag, New York.

Digital Library

[74]

von Wright, J. 1994. The lattice of data refinement. Acta Inf. 31, 105--135.

Digital Library

[75]

Ward, N. 1994. A refinement calculus for nondeterministic expressions. Ph.D. dissertation, University of Queensland.

[76]

Winskel, G. 1993. The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA, USA.

Digital Library

[77]

Woodcock, J. and Loomes, M. 1988. Software engineering mathematics. Addison-Wesley Longman Publishing Co., Inc., Boston, MA.

Digital Library

Cited By

Koenig JShao ZHermanns HZhang LKobayashi NMiller D(2020)Refinement-Based Game Semantics for Certified Abstraction LayersProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394799(633-647)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394799
Bird RRabe F(2019)How to Calculate with Nondeterministic FunctionsMathematics of Program Construction10.1007/978-3-030-33636-3_6(138-154)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-33636-3_6
Naumann D(2016)Towards patterns for heaps and imperative lambdasJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2015.10.00885:5(1038-1056)Online publication date: Aug-2016
https://doi.org/10.1016/j.jlamp.2015.10.008
Show More Cited By

Recommendations

Terms with unbounded demonic and angelic nondeterminacy

We show how to introduce demonic and angelic nondeterminacy into the term language of each type in typical programming or specification language. For each type we introduce (binary infix) operators @? and @? on terms of the type, corresponding to ...
Expansions of Dually Pseudocomplemented Heyting Algebras

We investigate expansions of Heyting algebras (EHAs) in possession of a unary term describing the filters that correspond to congruences. Hasimoto proved that Heyting algebras equipped with finitely many (dual) normal operators have such a term, ...
Complexity of Some Problems Concerning Varieties and Quasi-Varieties of Algebras

In this paper we consider the complexity of several problems involving finite algebraic structures. Given finite algebras A and B, these problems ask the following. (1) Do A and B satisfy precisely the same identities? (2) Do they satisfy the same ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 30, Issue 6

October 2008

245 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1391956

Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 October 2008

Accepted: 01 February 2008

Revised: 01 October 2006

Received: 01 December 2005

Published in TOPLAS Volume 30, Issue 6

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Science Foundation Ireland

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
488
Total Downloads

Downloads (Last 12 months)46
Downloads (Last 6 weeks)7

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Koenig JShao ZHermanns HZhang LKobayashi NMiller D(2020)Refinement-Based Game Semantics for Certified Abstraction LayersProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394799(633-647)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394799
Bird RRabe F(2019)How to Calculate with Nondeterministic FunctionsMathematics of Program Construction10.1007/978-3-030-33636-3_6(138-154)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-33636-3_6
Naumann D(2016)Towards patterns for heaps and imperative lambdasJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2015.10.00885:5(1038-1056)Online publication date: Aug-2016
https://doi.org/10.1016/j.jlamp.2015.10.008
McCorkle EHosking AEugster PHirschfeld R(2013)Building connections between theories of computing and physical systemsProceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software10.1145/2509578.2509587(153-172)Online publication date: 29-Oct-2013
https://dl.acm.org/doi/10.1145/2509578.2509587
Ribeiro PCavalcanti A(2013)Designs with Angelic NondeterminismProceedings of the 2013 International Symposium on Theoretical Aspects of Software Engineering10.1109/TASE.2013.18(71-78)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1109/TASE.2013.18
Hayes IBurns ADongol BJones C(2013)Comparing Degrees of Non-Determinism in Expression EvaluationThe Computer Journal10.1093/comjnl/bxt00556:6(741-755)Online publication date: 1-Jun-2013
https://dl.acm.org/doi/10.1093/comjnl/bxt005
Morris JBunkenburg ATyrrell M(2009)Term transformersACM Transactions on Programming Languages and Systems10.1145/1516507.151651131:4(1-42)Online publication date: 26-May-2009
https://dl.acm.org/doi/10.1145/1516507.1516511
Morris JTyrrell M(2008)Modelling higher-order dual nondeterminacyActa Informatica10.1007/s00236-008-0076-145:6(441-465)Online publication date: 18-Jul-2008
https://dl.acm.org/doi/10.1007/s00236-008-0076-1

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents