Confluence and Convergence in Probabilistically Terminating Reduction Systems

  • Maja H. KirkebyEmail author
  • Henning Christiansen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10855)


Convergence of an abstract reduction system (ARS) is the property that any derivation from an initial state will end in the same final state, a.k.a. normal form. We generalize this for probabilistic ARS as almost-sure convergence, meaning that the normal form is reached with probability one, even if diverging derivations may exist. We show and exemplify properties that can be used for proving almost-sure convergence of probabilistic ARS, generalizing known results from ARS.


  1. 1.
    Abdennadher, S.: Operational semantics and confluence of constraint propagation rules. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 252–266. Springer, Heidelberg (1997). Scholar
  2. 2.
    Abdennadher, S., Frühwirth, T., Meuss, H.: On confluence of constraint handling rules. In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 1–15. Springer, Heidelberg (1996). Scholar
  3. 3.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)zbMATHGoogle Scholar
  4. 4.
    Babai, L.: Monte-Carlo algorithms in graph isomorphism testing. Université de Montréal Technical report, DMS, vol. 79, pp. 1–33 (1979)Google Scholar
  5. 5.
    Baier, C., Katoen, J.-P.: Principles of Model Checking, vol. 950. MIT Press (2008)Google Scholar
  6. 6.
    Bournez, O., Garnier, F.: Proving positive almost sure termination under strategies. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 357–371. Springer, Heidelberg (2006). Scholar
  7. 7.
    Bournez, O., Kirchner, C.: Probabilistic rewrite strategies. applications to ELAN. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 252–266. Springer, Heidelberg (2002). Scholar
  8. 8.
    Christiansen, H., Kirkeby, M.H.: On proving confluence modulo equivalence for Constraint Handling Rules. Formal Aspects Comput. 29(1), 57–95 (2017)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Curien, P.-L., Ghelli, G.: On confluence for weakly normalizing systems. In: RTA-1991, pp. 215–225 (1991)CrossRefGoogle Scholar
  10. 10.
    Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL 2015, pp. 489–501 (2015)Google Scholar
  11. 11.
    Donald Frazer, W., McKellar, A.C.: Samplesort: a sampling approach to minimal storage tree sorting. J. ACM 17(3), 496–507 (1970)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Frühwirth, T.W., Di Pierro, A., Wiklicky, H.: Probabilistic constraint handling rules. Electr. Notes Theor. Comput. Sci. 76, 115–130 (2002)CrossRefGoogle Scholar
  13. 13.
    Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst. 5(3), 356–380 (1983)CrossRefGoogle Scholar
  14. 14.
    Herman, T.: Probabilistic self-stabilization. Inf. Process. Letters 35(2), 63–67 (1990)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Roger Hindley, J.: An abstract Church-Rosser theorem. II: applications. J. Symb. Log. 39(1), 1–21 (1974)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Huet, G.P.: Confluent reductions: abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)CrossRefGoogle Scholar
  17. 17.
    Itai, A.: A randomized algorithm for checking equivalence of circular lists. Inf. Process. Lett. 9(3), 118–121 (1979)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Karger, D.R., Stein, C.: A new approach to the minimum cut problem. J. ACM 43(4), 601–640 (1996)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Kirkpatrick, S., Gelatt Jr., D., Vecchi, M.P.: Optimization by simulated annealing. Science 220(4598), 671–680 (1983)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Maffioli, E., Speranza, M.G., Vercellis, C.: Randomized algorithms: an annotated bibliography. Ann. Oper. Res. 1(3), 331–345 (1984)CrossRefGoogle Scholar
  21. 21.
    Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, New York (1995)CrossRefGoogle Scholar
  22. 22.
    Newman, M.H.A.: On theories with a combinatorial definition of “equivalence”. Ann. Math. 43(2), 223–243 (1942)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Rabin, M.O.: The choice coordination problem. Acta Informatica 17(2), 121–134 (1982)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Sato, T.: A statistical learning method for logic programs with distribution semantics. ICLP 1995, 715–729 (1995)MathSciNetGoogle Scholar
  25. 25.
    Sato, T.: A glimpse of symbolic-statistical modeling by PRISM. J. Intell. Inf. Syst. 31(2), 161–176 (2008)CrossRefGoogle Scholar
  26. 26.
    Sato, T., Meyer, P.J.: Infinite probability computation by cyclic explanation graphs. TPLP 14(6), 909–937 (2014)MathSciNetzbMATHGoogle Scholar
  27. 27.
    Sneyers, J., Meert, W., Vennekens, J., Kameya, Y., Sato, T.: CHR(PRISM)-based probabilistic logic learning. In: TPLP, vol. 10(4–6) (2010)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Sneyers, J., De Schreye, D.: Probabilistic termination of CHRiSM programs. In: Vidal, G. (ed.) LOPSTR 2011. LNCS, vol. 7225, pp. 221–236. Springer, Heidelberg (2012). Scholar
  29. 29.
    Weisstein, E.W.: q-Pochhammer Symbol. MathWorld - A Wolfram Web Resource (2017)Google Scholar
  30. 30.
    Zippel, R.: Probabilistic algorithms for sparse polynomials. In: Ng, E.W. (ed.) Symbolic and Algebraic Computation. LNCS, vol. 72, pp. 216–226. Springer, Heidelberg (1979). Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Roskilde UniversityRoskildeDenmark

Personalised recommendations