Sequential algorithms for unbounded nondeterminism

Research output: Contribution to journalArticle

2 Citations (Scopus)
83 Downloads (Pure)

Abstract

We give extensional and intensional characterizations of higher-order functional programs with unbounded nondeterminism: as stable and monotone functions between the biorders of states of ordered concrete data structures, and as sequential algorithms (states of an exponential ocds) which compute them. Our fundamental result establishes that these representations are equivalent, by showing how to construct a unique sequential algorithm which computes a given stable and monotone function. We illustrate by defining a denotational semantics for a functional language with countable nondeterminism ("fair PCF"), with an interpretation of fixpoints which allows this to be proved to be computationally adequate. We observe that our model contains functions which cannot be computed in fair PCF, by identifying a further property of the definable elements, and so show that it is not fully abstract.

Original languageEnglish
Pages (from-to)271-287
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
Volume319
DOIs
Publication statusPublished - 21 Dec 2015

Fingerprint

Nondeterminism
Sequential Algorithm
Monotone Function
Denotational Semantics
Concrete Structures
Fixpoint
Countable
Data Structures
Higher Order
Data structures
Semantics
Concretes
Model
Interpretation
Language

Keywords

  • Biorders
  • Fairness
  • Nondeterminism
  • Sequential Algorithms

Cite this

Sequential algorithms for unbounded nondeterminism. / Laird, J.

In: Electronic Notes in Theoretical Computer Science, Vol. 319, 21.12.2015, p. 271-287.

Research output: Contribution to journalArticle

@article{cd7a678ea8a2471185b3dff4cdc67e7b,
title = "Sequential algorithms for unbounded nondeterminism",
abstract = "We give extensional and intensional characterizations of higher-order functional programs with unbounded nondeterminism: as stable and monotone functions between the biorders of states of ordered concrete data structures, and as sequential algorithms (states of an exponential ocds) which compute them. Our fundamental result establishes that these representations are equivalent, by showing how to construct a unique sequential algorithm which computes a given stable and monotone function. We illustrate by defining a denotational semantics for a functional language with countable nondeterminism ({"}fair PCF{"}), with an interpretation of fixpoints which allows this to be proved to be computationally adequate. We observe that our model contains functions which cannot be computed in fair PCF, by identifying a further property of the definable elements, and so show that it is not fully abstract.",
keywords = "Biorders, Fairness, Nondeterminism, Sequential Algorithms",
author = "J. Laird",
year = "2015",
month = "12",
day = "21",
doi = "10.1016/j.entcs.2015.12.017",
language = "English",
volume = "319",
pages = "271--287",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - Sequential algorithms for unbounded nondeterminism

AU - Laird, J.

PY - 2015/12/21

Y1 - 2015/12/21

N2 - We give extensional and intensional characterizations of higher-order functional programs with unbounded nondeterminism: as stable and monotone functions between the biorders of states of ordered concrete data structures, and as sequential algorithms (states of an exponential ocds) which compute them. Our fundamental result establishes that these representations are equivalent, by showing how to construct a unique sequential algorithm which computes a given stable and monotone function. We illustrate by defining a denotational semantics for a functional language with countable nondeterminism ("fair PCF"), with an interpretation of fixpoints which allows this to be proved to be computationally adequate. We observe that our model contains functions which cannot be computed in fair PCF, by identifying a further property of the definable elements, and so show that it is not fully abstract.

AB - We give extensional and intensional characterizations of higher-order functional programs with unbounded nondeterminism: as stable and monotone functions between the biorders of states of ordered concrete data structures, and as sequential algorithms (states of an exponential ocds) which compute them. Our fundamental result establishes that these representations are equivalent, by showing how to construct a unique sequential algorithm which computes a given stable and monotone function. We illustrate by defining a denotational semantics for a functional language with countable nondeterminism ("fair PCF"), with an interpretation of fixpoints which allows this to be proved to be computationally adequate. We observe that our model contains functions which cannot be computed in fair PCF, by identifying a further property of the definable elements, and so show that it is not fully abstract.

KW - Biorders

KW - Fairness

KW - Nondeterminism

KW - Sequential Algorithms

U2 - 10.1016/j.entcs.2015.12.017

DO - 10.1016/j.entcs.2015.12.017

M3 - Article

VL - 319

SP - 271

EP - 287

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -