Resource sharing linear logic

2020 ◽  
Vol 30 (1) ◽  
pp. 295-319
Author(s):  
Hidenori Kurokawa ◽  
Hirohiko Kushida
Keyword(s):  
Computational Model ◽  
Resource Sharing ◽  
Linear Logic ◽  
Cut Elimination ◽  
Parallel Version ◽  
Phase Semantics

Abstract In this paper, we introduce a new logic that we call ‘resource sharing linear logic (RSLL)’. In linear logic (LL), formulas without modality express some resource-conscious situation (a formula can be used only once); formulas with modality express a situation with unlimited resources. We introduce the logic RSLL in which we have a strengthened modality (S5-modality) that can be understood as expressing not only unlimited resources but also resources shared by different agents. Observing that merely strengthening the modality allows weakening axiom to be derivable in a Hilbert-style formulation of this logic, we reformulate RSLL as a logic similar to affine logic by a hypersequent calculus that has weakening as a primitive rule. We prove the completeness of the hypersequent calculus with respect to phase semantics and the cut-elimination theorem for the system by a syntactical method. We also prove the decidability of RSLL via a computational interpretation of RSLL, which is a parallel version of Kopylov’s computational model for LL. We then introduce an explicit counterpart of RSLL in the style of Artemov’s justication logic (JRSLL). We prove a realization theorem for RSLL via its explicit counterpart.

Non-commutative logic II: sequent calculus and phase semantics

2000 ◽  
Vol 10 (2) ◽  
pp. 277-312 ◽  
Author(s):  
PAUL RUET
Keyword(s):  
Special Class ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Partial Orders ◽  
Cut Elimination ◽  
Phase Semantics ◽  
Entropy Relation

Non-commutative logic, which is a unification of commutative linear logic and cyclic linear logic, is extended to all linear connectives: additives, exponentials and constants. We give two equivalent versions of the sequent calculus (directly with the structure of order varieties, and with their presentations as partial orders), phase semantics and a cut-elimination theorem. This involves, in particular, the study of the entropy relation between partial orders, and the introduction of a special class of order varieties: the series–parallel order varieties.

On the unification of classical, intuitionistic and affine logics

2018 ◽  
Vol 29 (8) ◽  
pp. 1177-1216
Author(s):  
CHUCK LIANG
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Kripke Semantics ◽  
Cut Elimination ◽  
Structural Rules ◽  
Phase Semantics ◽  
Intuitionistic Logics

This article presents a unified logic that combines classical logic, intuitionistic logic and affine linear logic (restricting contraction but not weakening). We show that this unification can be achieved semantically, syntactically and in the computational interpretation of proofs. It extends our previous work in combining classical and intuitionistic logics. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. We define a phase semantics for this logic that naturally extends the Kripke semantics of intuitionistic logic. We present a sequent calculus with novel structural rules, which entail a more elaborate procedure for cut elimination. Computationally, this system allows affine-linear interpretations of proofs to be combined with classical interpretations, such as the λμ calculus. We show how cut elimination must respect the boundaries between classical and non-classical modes of proof that correspond to delimited control effects.

scholarly journals Phase semantics for light linear logic

2003 ◽  
Vol 294 (3) ◽  
pp. 525-549 ◽  
Author(s):  
Max I Kanovich ◽  
Mitsuhiro Okada ◽  
Andre Scedrov
Keyword(s):  
Linear Logic ◽  
Phase Semantics

scholarly journals Generalized Bounded Linear Logic and its Categorical Semantics

2021 ◽  
pp. 226-246
Author(s):  
Yōji Fukihara ◽  
Shin-ya Katsumata
Keyword(s):  
Linear Logic ◽  
Cut Elimination ◽  
Grading System ◽  
Bounded Linear ◽  
The Core ◽  
Categorical Structure ◽  
Categorical Semantics

AbstractWe introduce a generalization of Girard et al.’s called (and its affine variant ). It is designed to capture the core mechanism of dependency in , while it is also able to separate complexity aspects of . The main feature of is to adopt a multi-object pseudo-semiring as a grading system of the !-modality. We analyze the complexity of cut-elimination in , and give a translation from with constraints to with positivity axiom. We then introduce indexed linear exponential comonads (ILEC for short) as a categorical structure for interpreting the $${!}$$ ! -modality of . We give an elementary example of ILEC using folding product, and a technique to modify ILECs with symmetric monoidal comonads. We then consider a semantics of using the folding product on the category of assemblies of a BCI-algebra, and relate the semantics with the realizability category studied by Hofmann, Scott and Dal Lago.

scholarly journals Possession as Linear Knowledge

10.29007/ntkm ◽  
2018 ◽  
Author(s):  
Frank Pfenning
Keyword(s):  
Distributed System ◽  
Epistemic Logic ◽  
Linear Logic ◽  
Expressive Power ◽  
Cut Elimination ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Ongoing Effort ◽  
Multi Agent ◽  
Localized Knowledge

Epistemic logic analyzes reasoning governing localized knowledge, and is thus fundamental to multi- agent systems. Linear logic treats hypotheses as consumable resources, allowing us to model evolution of state. Combining principles from these two separate traditions into a single coherent logic allows us to represent localized consumable resources and their flow in a distributed system. The slogan “possession is linear knowledge” summarizes the underlying idea. We walk through the design of a linear epistemic logic and discuss its basic metatheoretic properties such as cut elimination. We illustrate its expressive power with several examples drawn from an ongoing effort to design and implement a linear epistemic logic programming language for multi-agent distributed systems.

scholarly journals Phase Semantics for Light Linear Logic (Extended Abstract)

1997 ◽  
Vol 6 ◽  
pp. 221-234 ◽  
Author(s):  
Max I. Kanovich ◽  
Mitsuhiro Okada ◽  
Andre Scedrov
Keyword(s):  
Linear Logic ◽  
Phase Semantics

scholarly journals Reconciling Lambek’s restriction, cut-elimination and substitution in the presence of exponential modalities

2020 ◽  
Vol 30 (1) ◽  
pp. 239-256 ◽  
Author(s):  
Max Kanovich ◽  
Stepan Kuznetsov ◽  
Andre Scedrov
Keyword(s):  
Linear Logic ◽  
Cut Elimination ◽  
Lambek Calculus ◽  
Full Extent ◽  
Intuitionistic Linear Logic

Abstract The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called ‘Lambek’s restriction’, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek’s restriction. Interestingly enough, we show that for any system equipped with a reasonable exponential modality the following holds: if the system enjoys cut elimination and substitution to the full extent, then the system necessarily violates Lambek’s restriction. Nevertheless, we show that two of the three conditions can be implemented. Namely, we design a system with Lambek’s restriction and cut elimination and another system with Lambek’s restriction and substitution. For both calculi, we prove that they are undecidable, even if we take only one of the two divisions provided by the Lambek calculus. The system with cut elimination and substitution and without Lambek’s restriction is folklore and known to be undecidable.

scholarly journals On geometry of interaction for polarized linear logic

2017 ◽  
Vol 28 (10) ◽  
pp. 1639-1694
Author(s):  
MASAHIRO HAMANO ◽  
PHILIP SCOTT
Keyword(s):  
Proof Theory ◽  
Monoidal Category ◽  
Linear Logic ◽  
Cut Elimination ◽  
List Type ◽  
Monoidal Categories ◽  
Categorical Structure ◽  
Categorical Models ◽  
Focusing Property ◽  
Special Case

We present Geometry of Interaction (GoI) models for Multiplicative Polarized Linear Logic, MLLP, which is the multiplicative fragment of Olivier Laurent's Polarized Linear Logic. This is done by uniformly adding multi-points to various categorical models of GoI. Multi-points are shown to play an essential role in semantically characterizing the dynamics of proof networks in polarized proof theory. For example, they permit us to characterize the key feature of polarization, focusing, as well as being fundamental to our construction of concrete polarized GoI models.Our approach to polarized GoI involves following two independent studies, based on different categorical perspectives of GoI: (i)Inspired by the work of Abramsky, Haghverdi and Scott, a polarized GoI situation is defined in which multi-points are added to a traced monoidal category equipped with a reflexive object U. Using this framework, categorical versions of Girard's execution formula are defined, as well as the GoI interpretation of MLLP proofs. Running the execution formula is shown to characterize the focusing property (and thus polarities) as well as the dynamics of cut elimination.(ii)The Int construction of Joyal–Street–Verity is another fundamental categorical structure for modelling GoI. Here, we investigate it in a multi-pointed setting. Our presentation yields a compact version of Hamano–Scott's polarized categories, and thus denotational models of MLLP. These arise from a contravariant duality between monoidal categories of positive and negative objects, along with an appropriate bimodule structure (representing ‘non-focused proofs’) between them.Finally, as a special case of (ii) above, a compact model of MLLP is also presented based on Rel (the category of sets and relations) equipped with multi-points.

On categorical models of classical logic and the Geometry of Interaction

2007 ◽  
Vol 17 (5) ◽  
pp. 957-1027 ◽  
Author(s):  
CARSTEN FÜHRMANN ◽  
DAVID PYM
Keyword(s):  
Classical Logic ◽  
Disjoint Union ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Structural Theory ◽  
Cut Elimination ◽  
Categorical Models ◽  
Boolean Lattices ◽  
Deep Exploration ◽  
Straightforward Proof

It is well known that weakening and contraction cause naive categorical models of the classical sequent calculus to collapse to Boolean lattices. In previous work, summarised briefly herein, we have provided a class of models calledclassical categoriesthat is sound and complete and avoids this collapse by interpreting cut reduction by a poset enrichment. Examples of classical categories include boolean lattices and the category of sets and relations, where both conjunction and disjunction are modelled by the set-theoretic product. In this article, which is self-contained, we present an improved axiomatisation of classical categories, together with a deep exploration of their structural theory. Observing that the collapse already happens in the absence of negation, we start with negation-free models calledDummett categories. Examples of these include, besides the classical categories mentioned above, the category of sets and relations, where both conjunction and disjunction are modelled by the disjoint union. We prove that Dummett categories are MIX, and that the partial order can be derived from hom-semilattices, which have a straightforward proof-theoretic definition. Moreover, we show that the Geometry-of-Interaction construction can be extended from multiplicative linear logic to classical logic by applying it to obtain a classical category from a Dummett category.Along the way, we gain detailed insights into the changes that proofs undergo during cut elimination in the presence of weakening and contraction.

Sign in / Sign up

Export Citation Format

Share Document