Document Open Access Logo

The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic

Author Ross Horne

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.23.pdf
  • Filesize: 0.65 MB
  • 16 pages

Document Identifiers

Author Details

Ross Horne
  • Computer Science and Communications, University of Luxembourg, Esch-sur-Alzette, Luxembourg

Acknowledgements

I thank Bogdan Aman and Gabriel Ciobanu for their enjoyable discussions.

Cite AsGet BibTex

Ross Horne. The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.23

Abstract

Probabilistic choice, where each branch of a choice is weighted according to a probability distribution, is an established approach for modelling processes, quantifying uncertainty in the environment and other sources of randomness. This paper uncovers new insight showing probabilistic choice has a purely logical interpretation as an operator in an extension of linear logic. By forbidding projection and injection, we reveal additive operators between the standard with and plus operators of linear logic. We call these operators the sub-additives. The attention of the reader is drawn to two sub-additive operators: the first being sound with respect to probabilistic choice; while the second arises due to the fact that probabilistic choice cannot be self-dual, hence has a de Morgan dual counterpart. The proof theoretic justification for the sub-additives is a cut elimination result, employing a technique called decomposition. The justification from the perspective of modelling probabilistic concurrent processes is that implication is sound with respect to established notions of probabilistic refinement, and is fully compositional.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Process calculi
  • Theory of computation → Linear logic
Keywords
  • calculus of structures
  • probabilistic choice
  • probabilistic refinement

Metrics

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

References

  1. Samy Abbes and Albert Benveniste. True-concurrency probabilistic models: Branching cells and distributed probabilities for event structures. Information and Computation, 204(2):231-274, 2006. URL: http://dx.doi.org/10.1016/j.ic.2005.10.001.
  2. Christel Baier and Holger Hermanns. Weak bisimulation for fully probabilistic processes. In Computer Aided Verification, pages 119-130. Springer, 1997. URL: http://dx.doi.org/10.1007/3-540-63166-6_14.
  3. Paola Bruscoli. A Purely Logical Account of Sequentiality in Proof Search. In ICLP, pages 302-316, 2002. URL: http://dx.doi.org/10.1007/3-540-45619-8_21.
  4. Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The focused calculus of structures. In CSL, volume 12, pages 159-173, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2011.159.
  5. Gabriel Ciobanu and Ross Horne. Behavioural Analysis of Sessions using the Calculus of Structures. In PSI 2015, 25-27 August, Kazan, Russia, volume 9609 of LNCS, pages 91-106, 2015. URL: http://dx.doi.org/10.1007/978-3-319-41579-6_8.
  6. Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 833-845. ACM, 2017. URL: http://dx.doi.org/10.1145/3009837.3009859.
  7. Vincent Danos and Russell S. Harmer. Probabilistic Game Semantics. ACM Trans. Comp. Logic, 3(3):359-382, July 2002. URL: http://dx.doi.org/10.1145/507382.507385.
  8. Jerry den Hartog, Erik P. de Vink, and Jacobus W. De Bakker. Metric semantics and full abstractness for action refinement and probabilistic choice. Electronic Notes in Theoretical Computer Science, 40:72-99, 2001. URL: http://dx.doi.org/10.1016/S1571-0661(05)80038-6.
  9. Yuxin Deng. Semantics of Probabilistic Processes: An Operational Approach. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-45198-4.
  10. Yuxin Deng, Matthew Hennessy, Rob van Glabbeek, and Carroll Morgan. Characterising Testing Preorders for Finite Probabilistic Processes. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 313-325, July 2007. URL: http://dx.doi.org/10.1109/LICS.2007.15.
  11. Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan. Characterising Testing Preorders for Finite Probabilistic Processes. Logical Methods in Computer Science, 4(4), 2008. URL: http://dx.doi.org/10.2168/LMCS-4(4:4)2008.
  12. Thomas Ehrhard, Michele Pagani, and Christine Tasson. The computational meaning of probabilistic coherence spaces. In LICS, pages 87-96. IEEE, 2011. URL: http://dx.doi.org/10.1109/LICS.2011.29.
  13. Thomas Ehrhard, Christine Tasson, and Michele Pagani. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Proc. POPL, 49(1):309-320, 2014. URL: http://dx.doi.org/10.1145/2535838.2535865.
  14. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48-73, 2011. URL: http://dx.doi.org/10.1016/j.ic.2010.09.004.
  15. Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50(1):1-112, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  16. Jean-Yves Girard. Between logic and quantic: a tract. Linear logic in computer science, 316:346-381, 2004. URL: http://dx.doi.org/10.1017/CBO9780511550850.011.
  17. Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Computational Logic, 8(1), 2007. URL: http://dx.doi.org/10.1145/1182613.1182614.
  18. Alessio Guglielmi and Tom Gundersen. Normalisation Control in Deep Inference via Atomic Flows. Logical Methods in Computer Science, 4(1), 2008. URL: http://dx.doi.org/10.2168/LMCS-4(1:9)2008.
  19. Alessio Guglielmi and Lutz Straßburger. A system of interaction and structure V: the exponentials and splitting. Mathematical Structures in Computer Science, 21(3):563-584, 2011. URL: http://dx.doi.org/10.1017/S096012951100003X.
  20. Ross Horne. The Consistency and Complexity of Multiplicative Additive System Virtual. Sci. Ann. Comp. Sci., 25(2):245-316, 2015. URL: http://dx.doi.org/10.7561/SACS.2015.2.245.
  21. Ross Horne, Sjouke Mauw, and Alwen Tiu. Semantics for Specialising Attack Trees based on Linear Logic. Fundamenta Informaticae, 153(1-2):57-86, 2017. URL: http://dx.doi.org/10.3233/FI-2017-1531.
  22. Ross Horne and Alwen Tiu. Constructing Weak Simulations from Linear Implications for Processes with Private Names. Mathematical Structure in Computer Science, pages 1-34, 2019. URL: http://dx.doi.org/10.1017/S0960129518000452.
  23. Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. Private Names in Non-Commutative Logic. In CONCUR 2016, pages 31:1-31:16. LIPIcs, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.31.
  24. Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic. ACM Transactions on Computational Logic (TOCL), 20(4), 2019. Google Scholar
  25. Michael Huth and Marta Z. Kwiatkowska. Quantitative analysis and model checking. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 111-122, 1997. URL: http://dx.doi.org/10.1109/LICS.1997.614940.
  26. Cliff Jones and Gordon Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 186-195, June 1989. URL: http://dx.doi.org/10.1109/LICS.1989.39173.
  27. Bengt Jonsson and Wang Yi. Compositional testing preorders for probabilistic processes. In LICS, pages 431-441. IEEE, 1995. URL: http://dx.doi.org/10.1109/LICS.1995.523277.
  28. Bengt Jonsson, Wang Yi, and Kim G Larsen. Probabilistic extensions of process algebras. Handbook of process algebra, pages 685-710, 2001. URL: http://dx.doi.org/10.1016/B978-044482830-9/50029-1.
  29. Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications, 46(3):413–450, 2012. URL: http://dx.doi.org/10.1051/ita/2012012.
  30. Kim G Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and computation, 94(1):1-28, 1991. URL: http://dx.doi.org/10.1016/0890-5401(91)90030-6.
  31. Annabelle McIver and Carroll Morgan. Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science). SpringerVerlag, 2004. URL: http://dx.doi.org/10.1007/b138392.
  32. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1-77, 1992. URL: http://dx.doi.org/10.1016/0890-5401(92)90008-4.
  33. Catuscia Palamidessi and Oltea Mihaela Herescu. A randomized encoding of the π-calculus with mixed choice. Theoretical Computer Science, 335(2-3):373-404, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2004.11.020.
  34. Andrew Pitts. Nominal Logic, a First Order Theory of Names and Binding. Information and Computation, 186(2), 2003. URL: http://dx.doi.org/10.1016/S0890-5401(03)00138-X.
  35. Luca Roversi. A deep inference system with a self-dual binder which is complete for linear lambda calculus. J. of Logic and Computaion, 26(2):677-698, 2016. URL: http://dx.doi.org/10.1093/logcom/exu033.
  36. Davide Sangiorgi. pi-Calculus, Internal Mobility, and Agent-Passing Calculi. Theor. Comput. Sci., 167(1&2):235-274, 1996. URL: http://dx.doi.org/10.1016/0304-3975(96)00075-8.
  37. Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250-273, 1995. URL: http://dx.doi.org/10.1007/3-540-56454-3_13.
  38. Lutz Straßburger. A local system for linear logic. In LPAR, volume 2514, pages 388-402. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-36078-6_26.
  39. Lutz Straßburger and Alessio Guglielmi. A system of interaction and structure IV: The exponentials and decomposition. ACM T. Comp. Log., 12(4):23:1-39, 2011. URL: http://dx.doi.org/10.1145/1970398.1970399.
  40. Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph. Removing Cycles from Proofs. In CSL, pages 9:1-9:17, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2017.9.
  41. Rob van Glabbeek and Ursula Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 37(4-5):229-327, 2001. URL: http://dx.doi.org/10.1007/s002360000041.
  42. Daniele Varacca, Hagen Völzer, and Glynn Winskel. Probabilistic event structures and domains. In CONCUR, pages 481-496, 2004. URL: http://dx.doi.org/10.1007/978-3-540-28644-8_31.
  43. Daniele Varacca and Glynn Winskel. Distributing probability over non-determinism. Mathematical Structures in Computer Science, 16(1):87–113, 2006. URL: http://dx.doi.org/10.1017/S0960129505005074.
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