Interpretations of recursion under unbounded nondeterminacy

DOI10.1016/0304-3975(88)90142-9MaRDI QIDQ1115173zbMATH OpenOpenAlexWikidataFDO

Authors W. H. Hesselink

Publication date 1988

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://pure.rug.nl/ws/files/3378932/1988ThCompSciHesselink1.pdf

zbMATH Keywords

denotational semanticsoperational semanticsunbounded nondeterminacyweakest preconditions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

This well written article concerns the semantics of language that contains unbounded nondeterminacy. Although already many papers have been written on this issue, the author succeeds in treating the subject from an original and interesting perspective. He does so by giving a denotational semantics without the standard tools of cpos or limits, thus circumventing the usual problems in the denotational semantics of unbounded nondeterminism. Instead, he bases both his operational and denotational semantics on an axiomatically defined notion of interpretation, using elementary mathematical means. Next, the well known notions of weakest (liberal) preconditions are characterized as smallest (largest) preparator functions, which are a kind of objects dual to interpretations. Finally, a characterization is given of the spectrum of interpretations which cannot deliver unjustified meaningful values upon divergence. Again, corresponding preparator functions are determined.

Recommendations

• A simple fixpoint argument without the restriction to continuity
• Dual unbounded nondeterminacy, recursion, and fixpoints
• Nondeterminacy and recursion via stacks and games
• A category-theoretic semantics for unbounded indeterminacy
• scientific article; zbMATH DE number 3924117

Cites work

• A mathematical approach to nondeterminism in data types
• Countable nondeterminism and random assignment
• Deadlock and fairness in morphisms of transition systems
• scientific article; zbMATH DE number 3856436 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 3714908 (Why is no real title available?)
• scientific article; zbMATH DE number 3729429 (Why is no real title available?)
• scientific article; zbMATH DE number 3735115 (Why is no real title available?)
• scientific article; zbMATH DE number 3532506 (Why is no real title available?)
• Predicative programming Part I
• Programming as a Discipline of Mathematical Nature
• Proof rules and transformations dealing with fairness
• Some Properties of Predicate Transformers
• Specification-oriented semantics for communicating processes

Cited in

(10)

• Deadlock and fairness in morphisms of transition systems
• Nondeterminacy and recursion via stacks and games
• Safety and progress of recursive procedures
• Semantics of under-determined expressions
• Relational semantics revisited
• From Chaos to Undefinedness
• A category-theoretic semantics for unbounded indeterminacy
• Command algebras, recursion and program transformation
• Alternating states for dual nondeterminism in imperative programming
• Dual unbounded nondeterminacy, recursion, and fixpoints

This page was built for publication: Interpretations of recursion under unbounded nondeterminacy

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1115173)