The sub-additives : a proof theory for probabilistic choice extending linear logic

Horne, Ross; Geuvers, Herman and Geuvers, Herman, eds. (2019) 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, 131 . Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, DEU, 23:1-23:16. ISBN 9783959771078 (https://doi.org/10.4230/LIPIcs.FSCD.2019.23)

[thumbnail of Horne-FSCD2019-The-sub-additives-proof-theory-probabilistic-choice-extending-linear-logic]
Preview
 Text. Filename: Horne-FSCD2019-The-sub-additives-proof-theory-probabilistic-choice-extending-linear-logic.pdf
Final Published Version
License: Creative Commons Attribution 3.0 logo
Download (687kB)| Preview

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.

ORCID iDs

Horne, Ross ORCID logoORCID: https://orcid.org/0000-0003-0162-1901; Geuvers, Herman and Geuvers, Herman
  • Item type:Book Section
    ID code:87269
    Dates:
    Date
    Event
    18 June 2019
    Published
    8 April 2019
    Accepted
    Notes:Publisher Copyright: © Ross Horne. 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
    Subjects:Science > Mathematics > Electronic computers. Computer science
    Department:Faculty of Science > Computer and Information Sciences
    Depositing user: Pure Administrator
    Date deposited:09 Nov 2023 16:07
    Last modified:11 Nov 2024 15:33
    Related URLs:
    URI:https://strathprints.strath.ac.uk/id/eprint/87269
CORE (COnnecting REpositories)