Technical Report

 

A powerdoman semantics for indeterminism Public Deposited

Analytics

Downloadable Content

Download PDF
https://ir.library.oregonstate.edu/concern/technical_reports/0r967c207

Descriptions

Attribute NameValues
Alternative Title
Creator
Abstract
  • 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
Series
Rights Statement
Publisher
Language

Relationships

Parents:

This work has no parents.

Items

Thumbnail Title Date Uploaded Visibility Actions
Wise_David_S_1984_01.pdf 2023-01-26 Public