On the fixpoints of nondeterministic recursive definitions (Q1059391)

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.