Document Open Access Logo

Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms

Author Claudia Faggian

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.19.pdf
  • Filesize: 1.07 MB
  • 25 pages

Document Identifiers

Author Details

Claudia Faggian
  • Université de Paris, IRIF, CNRS, F-75013 Paris, France

Acknowledgements

This work benefitted of fruitful discussions with U. Dal Lago, B. Valiron, and T. Leventis. I also wish to thank the anonymous referees for valuable comments and suggestions.

Cite AsGet BibTex

Claudia Faggian. Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 19:1-19:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.19

Abstract

While a mature body of work supports the study of rewriting systems, abstract tools for Probabilistic Rewriting are still limited. We study in this setting questions such as uniqueness of the result (unique limit distribution) and normalizing strategies (is there a strategy to find a result with greatest probability?). The goal is to have tools to analyse the operational properties of probabilistic calculi (such as probabilistic lambda-calculi) whose evaluation is also non-deterministic, in the sense that different reductions are possible.

Subject Classification

ACM Subject Classification
  • Theory of computation → Probabilistic computation
  • Theory of computation → Rewrite systems
  • Theory of computation → Logic
Keywords
  • probabilistic rewriting
  • PARS
  • abstract rewriting systems
  • confluence
  • probabilistic lambda calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Gul A. Agha, José Meseguer, and Koushik Sen. PMaude: Rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci., 153(2):213-239, 2006. Google Scholar
  2. Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. PACMPL, 2(POPL):34:1-34:32, 2018. Google Scholar
  3. Martin Avanzini, U. Dal Lago, and Akihisa Yamada. On Probabilistic Term Rewriting. In Symposium on Functional and Logic Programming, FLOP, pages 132-148, 2018. Google Scholar
  4. Olivier Bournez and Florent Garnier. Proving Positive Almost Sure Termination Under Strategies. In Rewriting Techniques and Applications, RTA, pages 357-371, 2006. Google Scholar
  5. Olivier Bournez and Claude Kirchner. Probabilistic Rewrite Strategies. Applications to ELAN. In Rewriting Techniques and Applications, RTA, pages 252-266, 2002. Google Scholar
  6. N. Cagman and J.R. Hindley. Combinatory weak reduction in lambda calculus. Theor. Comput. Sci., 1998. Google Scholar
  7. Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. The geometry of parallelism: classical, probabilistic, and quantum effects. In POPL, pages 833-845, 2017. Google Scholar
  8. Ugo Dal Lago and Simone Martini. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci., 398(1-3):32-50, 2008. Google Scholar
  9. Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. Confluence Results for a Quantum Lambda Calculus with Measurements. Electr. Notes Theor. Comput. Sci., 270(2):251-261, 2011. Google Scholar
  10. Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO - Theor. Inf. and Applic., 46(3):413-450, 2012. Google Scholar
  11. Ugo de'Liguoro and Adolfo Piperno. Non Deterministic Extensions of Untyped Lambda-Calculus. Inf. Comput., 122(2):149-177, 1995. Google Scholar
  12. Nachum Dershowitz, Stéphane Kaplan, and David A. Plaisted. Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, . . Theor. Comput. Sci., 83(1):71-96, 1991. Google Scholar
  13. Alessandra Di Pierro, Chris Hankin, and Herbert Wiklicky. Probabilistic lambda-calculus and Quantitative Program Analysis. J. Log. Comput., 15(2):159-179, 2005. Google Scholar
  14. Alejandro Díaz-Caro, Pablo Arrighi, Manuel Gadella, and Jonathan Grattage. Measurements and Confluence in Quantum Lambda Calculi With Explicit Qubits. Electr. Notes Theor. Comput. Sci., 270(1):59-74, 2011. Google Scholar
  15. Alejandro Díaz-Caro and Guido Martinez. Confluence in Probabilistic Rewriting. Electr. Notes Theor. Comput. Sci., 338:115-131, 2018. Google Scholar
  16. Thomas Ehrhard, Michele Pagani, and Christine Tasson. The Computational Meaning of Probabilistic Coherence Spaces. In LICS, pages 87-96, 2011. Google Scholar
  17. Claudia Faggian. Probabilistic Rewriting: On Normalization, Termination, and Unique Normal Forms (Extended Version). Available at URL: http://arxiv.org/abs/1804.05578.
  18. Claudia Faggian and Simona Ronchi Della Rocca. Lambda Calculus and Probabilistic Computation. In LICS, 2019. Google Scholar
  19. Luis María Ferrer Fioriti and Holger Hermanns. Probabilistic Termination: Soundness, Completeness, and Compositionality. In POPL, pages 489-501, 2015. Google Scholar
  20. Hongfei Fu and Krishnendu Chatterjee. Termination of Nondeterministic Probabilistic Programs. In Verification, Model Checking, and Abstract Interpretation VMCAI, pages 468-490, 2019. Google Scholar
  21. W.A. Howard. Assignment of ordinals to terms for primitive recursive functionals of finite type. In Intuitionism and Proof Theory, 1970. Google Scholar
  22. Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. J. ACM, 65(5):30:1-30:68, 2018. Google Scholar
  23. Richard Kennaway. On transfinite abstract reduction systems. Tech. rep., CWI, Amsterdam, 1992. Google Scholar
  24. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Transfinite Reductions in Orthogonal Term Rewriting Systems. Inf. Comput., 119(1):18-38, 1995. Google Scholar
  25. Maja H. Kirkeby and Henning Christiansen. Confluence and Convergence in Probabilistically Terminating Reduction Systems. In Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, pages 164-179, 2017. Google Scholar
  26. Jan Willem Klop and Roel C. de Vrijer. Infinitary Normalization. In We Will Show Them! Essays in Honour of Dov Gabbay, Volume Two, pages 169-192, 2005. Google Scholar
  27. Daphne Koller, David A. McAllester, and Avi Pfeffer. Effective Bayesian Inference for Stochastic Programs. In National Conference on Artificial Intelligence and Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, pages 740-747, 1997. Google Scholar
  28. Yves Lafont. Interaction Nets. In POPL, pages 95-108, 1990. Google Scholar
  29. Simon Marlow. Parallel and Concurrent Programming in Haskell. O’Reilly Media, 2013. Google Scholar
  30. Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. A new proof rule for almost-sure termination. PACMPL, 2(POPL):33:1-33:28, 2018. Google Scholar
  31. Mark Newman. On Theories with a Combinatorial Definition of “Equivalence”. Annals of Mathematics, 43(2):223–243, 1942. Google Scholar
  32. Sungwoo Park, Frank Pfenning, and Sebastian Thrun. A probabilistic language based upon sampling functions. In POPL, pages 171-182, 2005. Google Scholar
  33. Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley &Sons, Inc., New York, NY, USA, 1st edition, 1994. Google Scholar
  34. Michael O. Rabin. Probabilistic Automata. Information and Control, 6(3):230-245, 1963. Google Scholar
  35. Norman Ramsey and Avi Pfeffer. Stochastic lambda calculus and monads of probability distributions. In POPL, pages 154-165, 2002. Google Scholar
  36. N. Saheb-Djahromi. Probabilistic LCF. In Mathematical Foundations of Computer Science, pages 442-451, 1978. Google Scholar
  37. Eugene S. Santos. Computability by Probabilistic turing Machines. In Transactions of the American Mathematical Society, pages 159:165-184, 1971. Google Scholar
  38. Alex K. Simpson. Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics. In Rewriting Techniques and Applications, RTA, pages 219-234, 2005. Google Scholar
  39. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  40. Vincent van Oostrom. Random Descent. In Term Rewriting and Applications, RTA, page 314–328, 2007. Google Scholar
  41. Vincent van Oostrom and Yoshihito Toyama. Normalisation by Random Descent. In Formal Structures for Computation and Deduction, FSCD, pages 32:1-32:18, 2016. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact