Data Refinement with Probability in Mind

T. M. Rabehaja*, J. W. Sanders

*Corresponding author for this work

Research output: Contribution to journalArticle

Abstract

The definition of data refinement between datatypes is expressed in terms of all programs that invoke procedures of the types. As a result it is laborious to check. Simulations provide sound conditions that, being 'static', facilitate checking; but then their soundness is important. In this paper we extract a technique from the heart of the theory and show it to be equivalent to data refinement; it plays a key role in establishing properties about simulations in any of the computational models. We survey the difficulties confronting the theory when the procedures and invoking programs may contain probabilistic choices, and show that then each of the two simulation conditions is alone not complete as a rule for data refinement, even if the datatypes are deterministic (in contrast to the standard case). The last part of the paper discusses work in progress.

Original languageEnglish
Pages (from-to)165-176
Number of pages12
JournalElectronic Notes in Theoretical Computer Science
Volume259
Issue numberC
DOIs
Publication statusPublished - 31 Dec 2009
Externally publishedYes

Keywords

  • Data refinement
  • incompleteness
  • probability
  • simulations

Fingerprint Dive into the research topics of 'Data Refinement with Probability in Mind'. Together they form a unique fingerprint.

Cite this