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

Authors: 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}
  }