License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.23
URN: urn:nbn:de:0030-drops-105300
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10530/
Go to the corresponding LIPIcs Volume Portal

Horne, Ross

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

pdf-format:
LIPIcs-FSCD-2019-23.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{horne:LIPIcs:2019:10530,
  author =	{Ross Horne},
  title =	{{The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10530},
  URN =		{urn:nbn:de:0030-drops-105300},
  doi =		{10.4230/LIPIcs.FSCD.2019.23},
  annote =	{Keywords: calculus of structures, probabilistic choice, probabilistic refinement}
}

Keywords: calculus of structures, probabilistic choice, probabilistic refinement
Collection: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue Date: 2019
Date of publication: 18.06.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI