Infinite trace equivalence

We solve a longstanding problem by providing a denotational model for nondeterministic programs that identifies two programs iff they have the same range of possible behaviours. We discuss the difficulties with traditional approaches, where divergence is bottom or where a term denotes a function fro...

Full description

Saved in:
Bibliographic Details
Published in:Annals of pure and applied logic 2008-02, Vol.151 (2), p.170-198
Main Author: Levy, Paul Blain
Format: Article
Language:English
Subjects:
Game semantics
Infinite traces
Jump-With-Argument
Nondeterminism
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We solve a longstanding problem by providing a denotational model for nondeterministic programs that identifies two programs iff they have the same range of possible behaviours. We discuss the difficulties with traditional approaches, where divergence is bottom or where a term denotes a function from a set of environments. We see that making forcing explicit, in the manner of game semantics, allows us to avoid these problems. We begin by modelling a first-order language with sequential I/O and unbounded nondeterminism (no harder to model, using this method, than finite nondeterminism). Then we extend the model to a calculus with higher-order and recursive types, by adapting standard game semantics. Traditional adequacy proofs using logical relations are not applicable, so we use instead a novel hiding and unhiding argument.
ISSN:0168-0072
DOI:10.1016/j.apal.2007.10.007