Skip to main content
SpringerLink
Log in

Probabilistic Choice, Reversibility, Loops, and Miracles

  • Conference paper
Unifying Theories of Programming (UTP 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6445))

Included in the following conference series:

Abstract

We consider an addition of probabilistic choice to Abrial’s Generalised Substitution Language (GSL) in a form that accommodates the backtracking interpretation of non-deterministic choice. Our formulation is introduced as an extension of the Prospective Values formalism we have developed to describe the results from a backtracking search. Significant features are that probabilistic choice is governed by feasibility, and non-termination is strict. The former property allows us to use probabilistic choice to generate search heuristics. In this paper we are particularly interested in iteration. By demonstrating sub-conjunctivity and monotonicity properties of expectations we give the basis for a fixed point semantics of iterative constructs, and we consider the practical proof treatment of probabilistic loops. We discuss loop invariants, loops with probabilistic behaviour, and probabilistic termination in the context of a formalism in which a small probability of non-termination can dominate our calculations, proposing a method of limits to avoid this problem. The formal programming constructs described have been implemented in a reversible virtual machine (RVM).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.-R.: The B Book. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  2. Finch, S.R.: Mathematical Constants. Cambridge (2003)

    Google Scholar 

  3. He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Science of Computer Programming 28(2-3), 171–192 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  4. Hehner, E.C.R.: Bunch theory: A simple set theory for computer science. Information Processing Letters 12.1, 26–31 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  5. Hehner, E.C.R.: A Practical Theory of Programming. Springer, Heidelberg (1993); Latest version available on-line

    Book  MATH  Google Scholar 

  6. Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, Computer Laboratory, University of Cambridge (2001)

    Google Scholar 

  7. Hurd, J.: A Formal Approach to Probabilistic Termination. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 230–245. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. He, J., Sanders, J.W.: Unifying probability. In: Dunne, S.E., Stoddart, W. (eds.) UTP 2006. LNCS, vol. 4010, pp. 173–199. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Kozen, D.: Semantics of Probabilistic Programs. Journal of Computer and System Sciences 22(3), 328–350 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  10. McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  11. McIver, A., Morgan, C., Hoang, T.S.: Probabilistic Termination in B. In: Bert, D., Bowen, J., King, S., Walden, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 216–239. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Meinicke1, L., Hayes, I.J.: Algebraic reasoning for probabilistic action systems and while-loops. Acta Informatica 45(5) (2008)

    Google Scholar 

  13. Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Tr-4-95, probabilistic predicate transformers. Technical report, Oxford University Programming Research Group (1995)

    Google Scholar 

  14. Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996)

    Article  Google Scholar 

  15. Stoddart, W.J., Zeyda, F.: A Unification of Probabilistic Choice within a Design-based Model of Reversible Computation. Formal Aspect of Computing (2007) (Published on line), doi:10.1007/s00165-007-0048-1

    Google Scholar 

  16. Stoddart, W.J., Zeyda, F.: Probabilistic Choice. Technical report, University of Teesside, UK, p. 35 (2008)

    Google Scholar 

  17. Stoddart, W.J., Zeyda, F., Dunne, S.E.: Preference and non-deterministic choice. In: Proceedings of ICTAC 2010. LNCS. Springer, Heidelberg (to appear, 2010)

    Google Scholar 

  18. Stoddart, W.J., Zeyda, F., Lynas, A.R.: A Design-based model of reversible computation. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 63–83. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Stoddart, W.J., Zeyda, F., Lynas, A.R.: A virtual machine for supporting reversible probabilistic guarded command languages. Electronic Notes in Theoretical Computer Science 253 (2010), doi:10.1016/j.entcs.2010.02.005

    Google Scholar 

  20. Zeyda, F., Stoddart, W.J., Dunne, S.: A Prospective-value Semantics for the GSL. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 187–202. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Teesside, UK

    Bill Stoddart

Authors
  1. Bill Stoddart
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pete Bell
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, University of Teesside, Borough Road, TS1 3BA, Middlesbrough, UK

    Shengchao Qin

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Stoddart, B., Bell, P. (2010). Probabilistic Choice, Reversibility, Loops, and Miracles. In: Qin, S. (eds) Unifying Theories of Programming. UTP 2010. Lecture Notes in Computer Science, vol 6445. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16690-7_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16690-7_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16689-1

  • Online ISBN: 978-3-642-16690-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation