Proof nets for multiplicative cyclic linear logic and Lambek calculus

AbstractThis paper presents a simple and intuitive syntax for proof nets of the multiplicative cyclic fragment (McyLL) of linear logic (LL). The main technical achievement of this work is to propose a correctness criterion that allows for sequentialization (recovering a proof from a proof net) for all McyLL proof nets, including those containing cut links. This is achieved by adapting the idea of contractibility (originally introduced by Danos to give a quadratic time procedure for proof nets correctness) to cyclic LL. This paper also gives a characterization of McyLL proof nets for Lambek Calculus and thus a geometrical (i.e., non-inductive) way to parse phrases or sentences by means of Lambek proof nets.

Download Full-text

Causal dependencies in multiplicative linear logic with MIX

Mathematical Structures in Computer Science ◽

10.1017/s0960129500000797 ◽

1995 ◽

Vol 5 (3) ◽

pp. 351-380 ◽

Cited By ~ 6

Author(s):

Andrea Asperti

Keyword(s):

Distributed Systems ◽

Linear Logic ◽

Correctness Criterion ◽

Proof Nets ◽

Original Interpretation ◽

Flow Of Information

A new correctness criterion for discriminating Proof Nets among Proof Structures of Multiplicative Linear Logic with the MIX rule is provided. This criterion is inspired by an original interpretation of Proof Structures as distributed systems, and logical formulae as processes. The computation inside a system corresponds to the logical flow of information inside a proof, that is, roughly speaking, a distributed version of Girard's token trip. Proof Nets are then characterised as deadlock free Proof Structures (deadlock free distributed systems). This result follows by explicitly considering the causal dependencies among logical formulae inside proofs, and it provides a new understanding of notions such as acyclicity, chains and empires in terms of concurrent computations.

Download Full-text

A new correctness criterion for the proof nets of non-commutative multiplicative linear logics

Journal of Symbolic Logic ◽

10.2307/2694960 ◽

2001 ◽

Vol 66 (4) ◽

pp. 1524-1542 ◽

Cited By ~ 1

Author(s):

Misao Nagayama ◽

Mitsuhiro Okada

Keyword(s):

Linear Time ◽

Linear Logic ◽

Time Algorithm ◽

Affirmative Answer ◽

Correctness Criterion ◽

Correctness Checking ◽

Proof Nets ◽

Open Question

Abstract.This paper presents a new correctness criterion for marked Danos-Reginer graphs (D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL.As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.

Download Full-text

Minimality of the correctness criterion for multiplicative proof nets

Mathematical Structures in Computer Science ◽

10.1017/s096012959800262x ◽

1998 ◽

Vol 8 (6) ◽

pp. 543-558 ◽

Cited By ~ 2

Author(s):

DENIS BECHET

Keyword(s):

Linear Logic ◽

Cut Elimination ◽

Correctness Criterion ◽

Proof Nets ◽

Static Criterion

Almost a decade ago, Girard invented linear logic with the notion of a proof-net. Proof-nets are special graphs built from formulas, links and boxes. However, not all nets are proof-nets. First, they must be well constructed (we say that such graphs are proof-structures). Second, a proof-net is a proof-structure that corresponds to a sequential proof. It must satisfy a correctness criterion. One may wonder what this static criterion means for cut-elimination. We prove that every incorrect proof-structure (without cut) can be put in an environment where reductions lead to two kinds of basically wrong configurations: deadlocks and disconnected proof-structures. Thus, this proof says that there does not exist a bigger class of proof-structures than proof-nets where normalization does not lead to obviously bad configurations.

Download Full-text

Subnets of proof-nets in multiplicative linear logic with MIX

Mathematical Structures in Computer Science ◽

10.1017/s0960129597002326 ◽

1997 ◽

Vol 7 (6) ◽

pp. 663-669 ◽

Cited By ~ 7

Author(s):

GIANLUIGI BELLIN

Keyword(s):

Linear Logic ◽

First Order ◽

Correctness Criterion ◽

Order Case ◽

Proof Nets ◽

Concurrent Processes ◽

Propositional Constants ◽

Intuitionistic Linear Logic ◽

General Method

This paper studies the properties of the subnets of a proof-net for first-order Multiplicative Linear Logic without propositional constants (MLL−), extended with the rule of Mix: from [vdash ]Γ and [vdash ]Δ infer [vdash ]Γ, Δ. Asperti's correctness criterion and its interpretation in terms of concurrent processes are extended to the first-order case. The notions of kingdom and empire of a formula are extended from MLL− to MLL−+MIX. A new proof of the sequentialization theorem is given. As a corollary, a system of proof-nets is given for De Paiva and Hyland's Full Intuitionistic Linear Logic with Mix; this result gives a general method for translating Abramsky-style term assignments into proof-nets, and vice versa.

Download Full-text

Interpolation in fragments of classical linear logic

Journal of Symbolic Logic ◽

10.2307/2275398 ◽

1994 ◽

Vol 59 (2) ◽

pp. 419-444 ◽

Cited By ~ 4

Author(s):

Dirk Roorda

Keyword(s):

Intuitionistic Logic ◽

Linear Logic ◽

Quantum Graphs ◽

Lambek Calculus ◽

Structural Rule ◽

Proof Nets

AbstractWe study interpolation for elementary fragments of classical linear logic. Unlike in intuitionistic logic (see [Renardel de Lavalette, 1989]) there are fragments in linear logic for which interpolation does not hold. We prove interpolation for a lot of fragments and refute it for the multiplicative fragment (→, +), using proof nets and quantum graphs. We give a separate proof for the fragment with implication and product, but without the structural rule of permutation. This is nearly the Lambek calculus. There is an appendix explaining what quantum graphs are and how they relate to proof nets.

Download Full-text

Lambek Calculus and Linear Logic: Proof Nets as Parse Structures

The Logic of Categorial Grammars - Lecture Notes in Computer Science ◽

10.1007/978-3-642-31555-8_6 ◽

2012 ◽

pp. 193-238

Author(s):

Richard Moot ◽

Christian Retoré

Keyword(s):

Linear Logic ◽

Lambek Calculus ◽

Proof Nets

Download Full-text

Proof nets and semi-star-autonomous categories

Mathematical Structures in Computer Science ◽

10.1017/s0960129514000395 ◽

2014 ◽

Vol 26 (5) ◽

pp. 789-828 ◽

Cited By ~ 1

Author(s):

WILLEM HEIJLTJES ◽

LUTZ STRAßBURGER

Keyword(s):

Linear Logic ◽

Proof Nets

In this paper, it is proved that Girard's proof nets for multiplicative linear logic characterize free semi-star-autonomous categories.

Download Full-text

A specification logic for concurrent object-oriented programming

Mathematical Structures in Computer Science ◽

10.1017/s0960129599002789 ◽

1999 ◽

Vol 9 (3) ◽

pp. 253-286 ◽

Cited By ~ 4

Author(s):

G. DELZANNO ◽

D. GALMICHE ◽

M. MARTELLI

Keyword(s):

Logic Programming ◽

Programming Languages ◽

Linear Logic ◽

Operational Semantics ◽

Object Oriented ◽

Object Oriented Programming ◽

Higher Order Logic ◽

Specification Logic ◽

Theoretic Characterization

This paper focuses on the use of linear logic as a specification language for the operational semantics of advanced concepts of programming such as concurrency and object-orientation. Our approach is based on a refinement of linear logic sequent calculi based on the proof-theoretic characterization of logic programming. A well-founded combination of higher-order logic programming and linear logic will be used to give an accurate encoding of the traditional features of concurrent object-oriented programming languages, whose corner-stone is the notion of encapsulation.

Download Full-text