A unification of probabilistic choice within a design-based model of reversible computation

Hdl Handle:
http://hdl.handle.net/10149/58314
Title:
A unification of probabilistic choice within a design-based model of reversible computation
Authors:
Stoddart, W. J. (Bill); Zeyda, F. (Frank)
Affiliation:
University of Teesside. School of Computing; University of York. Department of Computer Science. High Integrity Systems Engineering Group.
Citation:
Stoddart, W. J. and Zeyda, F. (2007) 'A unification of probabilistic choice within a design-based model of reversible computation', Formal Aspects of Computing FAC Special Issue on Unifying Theories of Programming; 25: pp.1-25
Publisher:
Springer Verlag
Journal:
Formal Aspects of Computing
Issue Date:
Oct-2007
URI:
http://hdl.handle.net/10149/58314
DOI:
10.1007/s00165-007-0048-1
Additional Links:
http://www.springerlink.com/content/102822/?k=Stoddart
Abstract:
We see reversible computing as a generalisation of sequential computation obtained by revoking the law of the excluded miracle. Our execution language includes naked guarded commands and non-deterministic choice. Choices which lead to miraculous continuations invoke reverse computation, and non-deterministic choice plays the rôle of provisional choice within a backtracking context. We require probabilistic choice for symmetry breaking and sampling large search spaces, but must formulate it differently from previous approaches to obtain the required interactions between probabilistic choice and non-deterministic choice and between probabilistic choice and feasibility. Our formulation allows us to derive the post-distributions which characterise a program, and we use these to construct a relational model. We consider refinement as containment of convex closures within distribution space, qualified with additional conditions to avoid over-refinement. We link the non-probabilistic and probabilistic versions of the model with a Galois connection and show that classical designs are a retract of our probabilistic designs. We consider the interaction between probabilistic and non-deterministic choice and find the same initially counter-intuitive results that have been noted by other investigators. We provide an alternative formulation, within the same model, of oblivious non-determinism, which allows all non-deterministic choices to be moved to the start of a computation. We consider the interaction between probabilistic choice and feasibility that is required to match an operational interpretation in which infeasible commands provoke reverse execution, and we present a small case study to show how the interaction between probabilistic choice and feasibility can be exploited in a practical program. All programming structures described here are supported by our implementation platform, the Reversible Virtual Machine, whose development has accompanied our theoretical investigations.
Type:
Article
Keywords:
reversible computing; backtracking; probability; Hoare-He designs; bunches
ISSN:
0934-5043
Rights:
Author can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 18/01/2010]
Citation Count:
0 [Web of Science and Scopus, 18/01/2010]

Full metadata record

DC FieldValue Language
dc.contributor.authorStoddart, W. J. (Bill)-
dc.contributor.authorZeyda, F. (Frank)-
dc.date.accessioned2009-04-01T10:48:47Z-
dc.date.available2009-04-01T10:48:47Z-
dc.date.issued2007-10-
dc.identifier.citationFormal Aspects of Computing FAC Special Issue on Unifying Theories of Programming; 25: 1-25-
dc.identifier.issn0934-5043-
dc.identifier.doi10.1007/s00165-007-0048-1-
dc.identifier.urihttp://hdl.handle.net/10149/58314-
dc.description.abstractWe see reversible computing as a generalisation of sequential computation obtained by revoking the law of the excluded miracle. Our execution language includes naked guarded commands and non-deterministic choice. Choices which lead to miraculous continuations invoke reverse computation, and non-deterministic choice plays the rôle of provisional choice within a backtracking context. We require probabilistic choice for symmetry breaking and sampling large search spaces, but must formulate it differently from previous approaches to obtain the required interactions between probabilistic choice and non-deterministic choice and between probabilistic choice and feasibility. Our formulation allows us to derive the post-distributions which characterise a program, and we use these to construct a relational model. We consider refinement as containment of convex closures within distribution space, qualified with additional conditions to avoid over-refinement. We link the non-probabilistic and probabilistic versions of the model with a Galois connection and show that classical designs are a retract of our probabilistic designs. We consider the interaction between probabilistic and non-deterministic choice and find the same initially counter-intuitive results that have been noted by other investigators. We provide an alternative formulation, within the same model, of oblivious non-determinism, which allows all non-deterministic choices to be moved to the start of a computation. We consider the interaction between probabilistic choice and feasibility that is required to match an operational interpretation in which infeasible commands provoke reverse execution, and we present a small case study to show how the interaction between probabilistic choice and feasibility can be exploited in a practical program. All programming structures described here are supported by our implementation platform, the Reversible Virtual Machine, whose development has accompanied our theoretical investigations.-
dc.publisherSpringer Verlag-
dc.relation.urlhttp://www.springerlink.com/content/102822/?k=Stoddart-
dc.rightsAuthor can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 18/01/2010]-
dc.subjectreversible computing-
dc.subjectbacktracking-
dc.subjectprobability-
dc.subjectHoare-He designs-
dc.subjectbunches-
dc.titleA unification of probabilistic choice within a design-based model of reversible computation-
dc.typeArticle-
dc.contributor.departmentUniversity of Teesside. School of Computing; University of York. Department of Computer Science. High Integrity Systems Engineering Group.-
dc.identifier.journalFormal Aspects of Computing-
ref.assessmentRAE 2008-
ref.citationcount0 [Web of Science and Scopus, 18/01/2010]-
or.citation.harvardStoddart, W. J. and Zeyda, F. (2007) 'A unification of probabilistic choice within a design-based model of reversible computation', Formal Aspects of Computing FAC Special Issue on Unifying Theories of Programming; 25: pp.1-25-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.