{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:32:14Z","timestamp":1725510734226},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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\u00f4le 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.<\/jats:p>","DOI":"10.1007\/s00165-007-0048-1","type":"journal-article","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T16:36:08Z","timestamp":1194885368000},"page":"107-131","source":"Crossref","is-referenced-by-count":5,"title":["A unification of probabilistic choice within a design-based model of reversible computation"],"prefix":"10.1145","volume":"25","author":[{"given":"Bill","family":"Stoddart","sequence":"first","affiliation":[{"name":"School of Computing, University of Teesside, Borough Road, TSI 3BA, Middlesbrough, UK"}]},{"given":"Frank","family":"Zeyda","sequence":"additional","affiliation":[{"name":"High Integrity Systems Engineering Group, Department of Computer Science, University of York, York, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R Mussat WJ (2002) On using conditional definitions in formal theories. In: ZB 2002: Formal Specification and Development in Z and B Vol 2272. Lecture Notes in Computer Science. Springer Heidelberg","DOI":"10.1007\/3-540-45648-1_13"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bennett C (1973) The logical reversibility of computation. IBM J Res Dev 6","DOI":"10.1147\/rd.176.0525"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02084158"},{"key":"e_1_2_1_2_4_2","unstructured":"den Hartog J (2001) Probabilistic extensions of semantic models. PhD thesis IPA Amsterdam"},{"key":"e_1_2_1_2_5_2","volume-title":"Lectures on computation","author":"Feynman RP","year":"1996"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/321420.321422"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90071-5"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8596-5","volume-title":"A practical theory of programming. Texts and Monographs in Computer Science","author":"Hehner ECR","year":"1993"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"He J Sanders JW (2006) Unifying probability. In: First international symposium on unifying theories of programming UTP 2006 Vol 4010. Lecture Notes in Computer Science. Springer Heidelberg pp 173\u2013199","DOI":"10.1007\/11768173_11"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Landauer R (1961) Irreversibility and heat generated in the computing process. IBM J R D 5","DOI":"10.1147\/rd.53.0183"},{"key":"e_1_2_1_2_12_2","unstructured":"McIver A Morgan CC (2004) Abstraction refinement and proof for probabilistic systems. Springer Heidelberg"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69559"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Stoddart WJ Dunne SE Galloway AJ (1999) Undefined expressions and logic in Z and B. Form Methods Syst Des 15(3)","DOI":"10.1023\/A:1008797018928"},{"key":"e_1_2_1_2_16_2","unstructured":"Stoddart WJ (2006) The reversible virtual machine. User and technical manuals University of Teesside UK"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Stoddart WJ Zeyda F Lynas AR (2006) A design-based model of reversible computation. In: UTP 2006 First international symposium on unifying theories of programming Vol 4010. Lecture Notes in Computer Science Springer Heidelberg pp 63\u201383","DOI":"10.1007\/11768173_4"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Varacca D Winskel G (2007) Distributing probability over nondeterminism. Mathematical Structures in Computer Science (in press)","DOI":"10.1017\/S0960129505005074"},{"key":"e_1_2_1_2_19_2","unstructured":"Zeyda F (2007) Reversible computation in B. PhD thesis University of Teesside"},{"key":"e_1_2_1_2_20_2","unstructured":"Zeyda F Stoddart WJ Dunne S (2003) The refinement of reversible computations. In: RCS\u201903: 2nd International workshop on refinement of critical systems: methods tools and developments"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Zeyda F Stoddart WJ Dunne S (2005) A prospective-value semantics for the GSL. In: ZB 2005: Formal specification and development in Z and B Vol 3455. Lecture Notes in Computer Science Springer Heidelberg pp 187\u2013202","DOI":"10.1007\/11415787_12"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Zuliani P (2001) Logical reversibility. IBM J R D 45(6)","DOI":"10.1147\/rd.456.0807"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0048-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0048-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0048-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:58:01Z","timestamp":1641484681000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0048-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["10.1007\/s00165-007-0048-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0048-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,1]]}}}