## Paper: The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations (at LICS 1986)

**David A. Plaisted**

### Abstract

We present a semantics of nondeterministic recursive programs based on fixpoints of relations rather than functionals. In this approach, one possible definition of the semantics of a nondeterministic program is the set of minimal functions f such that R(f,f) where R is a relation associated with the program. There are several other plausible semantics, corresponding to which fixpoints of R are chosen. The usual fixpoint induction for functionals generalizes to inference rules for relations. These rules permit proofs that all fixpoints of R satisfy some property, or that there exists a fixpoint of R satisfying some property. We give a completeness result for one of these inference rules. Simple inference rules for proving properties of fair fixpoints are also given. Finally, a simple programming language permitting guarded nondeterminism and recursion is given along with its semantics using relational approach.

### BibTeX

@InProceedings{Plaisted-TheDenotionalSemant, author = {David A. Plaisted}, title = {The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations}, booktitle = {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)}, year = {1986}, month = {June}, pages = {163--174 }, location = {Cambridge, MA, USA}, publisher = {IEEE Computer Society Press} }