文章基本信息

标题：The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic
本地全文：下载
作者：Ross Horne
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：131
页码：1-16
DOI：10.4230/LIPIcs.FSCD.2019.23
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：calculus of structures; probabilistic choice; probabilistic refinement