Technical Report

A powerdoman semantics for indeterminism

Public Deposited

Downloadable Content

Download PDF


Attribute NameValues
  • A denotational semantics is presented for a language that includes multiple-valued functions (essentially Lisp S-expressions), which map from ground values into the power domain of ground values. The domain equations are reflexive. and fixed points of all functions are defined. Thus, it is possible to specify an operating system as a function whose codomain is a set of possible behaviors of the system, only one of which is realized under an operational semantics. Such a system can be specified using "pure" applicative programming (recursion equations without side effects) over primitive functions like amb, frons, arbiter, or arbit, all of which are formally defined. Tempered by 'environmental transparency,' we consider a power domain semantics in which the power domain may only occur within the codomain in the equation that defines func­tion space. The problem addressed is how to define the analog of 'fixed point' for a function from the ground domain to that power domain, in a semantics that uses natural extension as the axiom for function application. Denotational and equivalent operational semantics are presented for the Smyth-upside-down power domain; a similar denotational semantics is presented for the Plotkin power domain (Egli-Milner order), along with a likely operational semantics.
Resource Type
Date Issued
Academic Affiliation
Rights Statement



This work has no parents.