On the fixpoints of nondeterministic recursive definitions

DOI10.1016/0022-0000(84)90014-XMaRDI QIDQ1059391zbMATH OpenOpenAlexFDO

Authors Tsong Yueh Chen

Publication date 1984

Published in Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0022-0000(84)90014-x

zbMATH Keywords

Egli orderingfixpoint semantics of boundedly nondeterministic recursive definitions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

This work studies the fixpoint semantics of boundedly nondeterministic recursive definitions; examined is the existence and characteristics of various fixpoints of functionals continuous with respect to Egli ordering \(\subseteq\). The following facts are established. Maximal fixpoints exist but are not unique. The optimal fixpoint which is by definition the greatest fixpoint dominated by all maximal fixpoints exists uniquely. The least and the optimal fixpoints are shown to be respectively the least and the greatest among all \(\subseteq\)-related fixpoints. A greatest fixpoint exists iff the set of all fixpoints is \(\subseteq\)-related. Considered is also the so called well-defined fixpoint. These results are illustrated by appropriate examples.

Recommendations

• On the structural properties of the set of fixpoints for nondeterministic recursive definitions
• Dual unbounded nondeterminacy, recursion, and fixpoints
• A fixpoint theory for non-monotonic parallelism
• scientific article; zbMATH DE number 1948158
• Relational semantics revisited

Cites work

• Backtracking in recursive computations
• Formalization of correctness of recursive definitions
• Formalization of equivalence of recursively defined functions
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3551848 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• On the relationship between computed functions and fixpoints of nondeterministic recursive definitions
• The convergence of functions to fixedpoints of recursive definitions
• The Theoretical Aspects of the Optimal Fixedpoint

Cited in

(9)

• A generalization of Naundorf's fixpoint theorem
• A fixpoint theory for non-monotonic parallelism
• On the structural properties of the set of fixpoints for nondeterministic recursive definitions
• scientific article; zbMATH DE number 1101591 (Why is no real title available?)
• scientific article; zbMATH DE number 1948158 (Why is no real title available?)
• Recursive definitions and fixed-points
• Fixpoints for general correctness
• From Chaos to Undefinedness
• Dual unbounded nondeterminacy, recursion, and fixpoints

This page was built for publication: On the fixpoints of nondeterministic recursive definitions

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