zbMATH — the first resource for mathematics

Dual unbounded nondeterminacy, recursion, and fixpoints. (English) Zbl 1127.68018
Summary: In languages with unbounded demonic and angelic nondeterminacy, functions acquire a surprisingly rich set of fixpoints. We show how to construct these fixpoints, and describe which ones are suitable for giving a meaning to recursively defined functions. We present algebraic laws for reasoning about them at the language level, and construct a model to show that the laws are sound. The model employs a new kind of power domain-like construct for accommodating arbitrary nondeterminacy.

68N18 Functional programming and lambda calculus
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Aarts C., Backhouse R.C., Boiten E.A., Doornbos H., Hoogendijk P.F., Voermans Ed, Gasteren N., Geldrop R. and Woude J. (1995). Fixed-point calculus. Inf. Process. Lett. 53(3): 131–136 · Zbl 0875.68201
[2] Abramsky, S., Jung, A.: Domain theory. In: Abramsky S., Gabbay D.M., Maibaum T.S.E. (ed.) Handbook of Logic in Computer Science, vol. 3, pp. 1–168. Clarendon Press, Oxford, (1994)
[3] Apt K.R. and Plotkin G.D. (1986). Countable nondeterminism and random assignment. J. ACM 33(4): 724–767 · Zbl 0627.68015
[4] Back, R.-J.R.: Correctness Preserving Program Refinements: Proof Theory and Applications. Tract 131. Mathematisch Centrum, Amsterdam (1980) · Zbl 0451.68018
[5] Back R.J.R. and Wright J. (1990). Duality in specification languages: a lattice-theoretical approach. Acta Inf. 27(7): 583–625 · Zbl 0699.68038
[6] Backhouse, K.: Abstract Interpretation of Domain-Specific Embedded Languages. PhD thesis, Oxford University (2002)
[7] Backhouse, R.: Galois connections and fixed point calculus. In: Backhouse R.C., Crole R.L., Gibbons J. (ed.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, Lecture Notes in Computer Science, vol. 2297, pp. 89–148. Springer, Heidelberg (2000) · Zbl 1065.68030
[8] Bartenschlager G. (1995). Free bounded distributive lattices over finite ordered sets and their skeletons. Acta Math. Universitatis Comenianae 64: 1–23 · Zbl 0922.06010
[9] Bekić, H.: Definable operations in general algebras, and the theory of automata and flowcharts, Lecture Notes in Computer Science, vol. 177, pp. 30–55. Springer, Hedelberg (1984)
[10] Birkhoff, G.: Lattice Theory, volume 25 of Colloquium Publications. American Mathematical Society, 3rd edition (1967) · Zbl 0153.02501
[11] Broy M. (1986). A theory for nondeterminism, parallelism, communication and concurrency. Theor. Comput. Sci. 45(1): 1–61 · Zbl 0601.68022
[12] Chen Y. (2003). A fixpoint theory for non-monotonic parallelism. Theor. Comput. Sci. 308(1–3): 367–392 · Zbl 1070.68081
[13] Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, (1990) · Zbl 0701.06001
[14] de Bakker J.W. (1980). Mathematical Theory of Program Correctness. Prentice-Hall, Englewood cliffs · Zbl 0452.68011
[15] Dijkstra E.W. (1976). A Discipline of programming. Prentice Hall, Englewood cliffs · Zbl 0368.68005
[16] 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 · Zbl 0699.06008
[17] Gunter, C.A.: Relating total and partial correctness interpretations of non-deterministic programs. In: POPL ’90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 306–319. ACM Press, New York (1990)
[18] Heckmann R. (1991). Lower and upper power domain constructions commute on all cpos. Inf. Process. Lett. 40(1): 7–11 · Zbl 0748.68038
[19] Heckmann R. (1991). Power domain constructions. Sci. Comput. Program. 17(1–3): 77–117 · Zbl 0769.08005
[20] Heckmann, R.: An upper power domain construction in terms of strongly compact sets. In: Stephen D., Brookes et al. (ed.) MFPS. Lecture Notes in Computer Science, vol. 598, pp. 272–293. Springer, Heidelberg (1991)
[21] Heckmann, R.: Power domains supporting recursion and failure. In: Raoult J.-C. (ed.) CAAP, Lecture Notes in Computer Science, vol. 581, pp. 165–181. Springer, Heidelburg (1992)
[22] Hennessy, M.: Powerdomains and nondeterministic recursive definitions. In: Ciancaglini M., Montanari U (eds.) Symposium on Programming, Lecture Notes in Computer Science, vol. 137, pp. 178–193, Springer, Heidelberg (1982) · Zbl 0486.68009
[23] Hennessy, M., Plotkin, G.D.: Full abstraction for a simple parallel programming language. In: Becvár J. (ed.) MFCS, Lecture Notes in Computer Science. vol. 74, pp. 108–120. Springer, Heidelberg (1979) · Zbl 0457.68006
[24] Hesselink W.H. (1994). Nondeterminacy and recursion via stacks and games. Theor. Comput. Sci. 124(2): 273–295 · Zbl 0795.68128
[25] Hesselink W.H. (1988). Interpretations of recursion under unbounded nondeterminacy. Theor. Comput. Sci. 59: 211–234 · Zbl 0663.68016
[26] Hesselink W.H. (1989). Predicate-transformer semantics of general recursion. Acta Inf. 26(4): 309–332 · Zbl 0643.03020
[27] Hesselink W.H. (1992). Programs, Recursion and Unbounded Choice. Number 27 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, London
[28] Hitchcock, P., Park, D.: Induction rules and termination proofs. In: IRIA Conference on Automata, Languages, and Programming Theory, pp. 225–251. North-Holland, Amsterdam (1972) · Zbl 0387.68011
[29] Hoofman, R.: Powerdomains. Technical Report RUU-CS-87-23, Institute of Information and Computing Sciences (1987)
[30] Jacobs D. and Gries D. (1985). General correctness: a unification of partial and total correctness. Acta Inf. 22(1): 67–83 · Zbl 0559.68021
[31] Main, M.G.: Free constructions of powerdomains. In: Melton A. (ed.) Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, vol. 239, pp. 162–183. Springer, Heidelberg (1985)
[32] Morris J.M. (1987). A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9: 287–306 · Zbl 0624.68017
[33] Morris, J.M.: Augmenting types with unbounded demonic and angelic nondeterminacy. In: Proceedings of the 7th International Conference on Mathematics of Program Construction, vol. 3125, pp. 274–288. Springer, Heidelberg (2004) · Zbl 1106.68344
[34] Morris J.M. and Bunkenburg A. (1999). Specificational functions. ACM. Trans. Program. Lang. Syst. 21: 677–701
[35] Morris J.M. and Bunkenburg A. (2002). A source of inconsistency in theories of nondeterministic functions. Sci. Comput. Program. 43(1): 77–89 · Zbl 1004.68036
[36] Morris, J.M., Tyrrell M.: Dually nondeterministic functions and functional refinement. Submitted, (2006)
[37] Morris, J.M., Tyrrell M.: Dual unbounded nondeterminacy and recursive functions: a conservation proof. Technical Report CA-0106, School of Computing, Dublin City University, (2006)
[38] Nelson G. (1989). A generalization of Dijkstra’s calculus. ACM Trans. Program. Lang. Syst. 11(4): 517–561
[39] Plotkin G. (1976). A powerdomain construction. SIAM J. Comput. 5(3): 452–487 · Zbl 0355.68015
[40] Plotkin, G.: Domain theory. Unpublished lecture notes (”The Pisa Notes”) (1983)
[41] Schmidt D.A. (1986). Denotational Semantics. Allyn and Bacon, Boston
[42] Smyth M.B. (1978). Power domains. J. Comput. Syst. Sci. 16(1): 23–26 · Zbl 0391.68011
[43] Smyth, M.B.: Power domains and predicate transformers: a topological view. In: Diaz J. (ed.) Proceedings of the 10th Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 153, pp. 662–675. Springer, London (1983) · Zbl 0533.68018
[44] Tarski A. (1955). A lattice-theoretical fixed point theorem and its applications. Pac. J. Math. 5(2): 285–309 · Zbl 0064.26004
[45] Tunnicliffe W.R. (1985). The free completely distributive lattice over a poset. Algebra Univers. 21: 133–135 · Zbl 0585.06005
[46] Ward, N.: A Refinement calculus for nondeterministic expressions. PhD thesis, University of Queensland (1994)
[47] Winskel G. (1993). The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge · Zbl 0919.68082
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.