Volume 44, Number 5, 323-344, DOI: 10.1007/s00236-007-0049-9

Dual unbounded nondeterminacy, recursion, and fixpoints

Joseph M. Morris and Malcolm Tyrrell

View Related Documents

Abstract

In languages with unbounded demonic and angelic nondeterminacy, functions acquire a surprisingly rich set of fixpoints. We show how to construct these fixpoints, and describe which ones are suitable for giving a meaning to recursively defined functions. We present algebraic laws for reasoning about them at the language level, and construct a model to show that the laws are sound. The model employs a new kind of power domain-like construct for accommodating arbitrary nondeterminacy.

Fulltext Preview

Image of the first page of the fulltext document