A fine-grained computational interpretation of Girard’s intuitionistic proof-nets

This paper introduces a functional term calculus, called pn, that captures the essence of the operational semantics of Intuitionistic Linear Logic Proof-Nets with a faithful degree of granularity, both statically and dynamically. On the static side, we identify an equivalence relation on pn-terms which is sound and complete with respect to the classical notion of structural equivalence for proof-nets. On the dynamic side, we show that every single (exponential) step in the term calculus translates to a different single (exponential) step in the graphical formalism, thus capturing the original Girard’s granularity of proof-nets but on the level of terms. We also show some fundamental properties of the calculus such as confluence, strong normalization, preservation of β-strong normalization and the existence of a strong bisimulation that captures pairs of pn-terms having the same graph reduction.

Download Full-text

A new deconstructive logic: linear logic

Journal of Symbolic Logic ◽

10.2307/2275572 ◽

1997 ◽

Vol 62 (3) ◽

pp. 755-807 ◽

Cited By ~ 75

Author(s):

Vincent Danos ◽

Jean-Baptiste Joinet ◽

Harold Schellinx

Keyword(s):

Classical Logic ◽

Sequent Calculus ◽

Predicate Logic ◽

Linear Logic ◽

Second Order ◽

Main Concern ◽

Simple Pattern ◽

Strong Normalization ◽

Viable Systems ◽

Proof Nets

AbstractThe main concern of this paper is the design of a noetherian and confluent normalization for LK2 (that is, classical second order predicate logic presented as a sequent calculus).The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD ([10, 12, 32, 36]), delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of ‘programming-with-proofs’ ([26, 27]) to classical logic; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic (for non-additive proof nets, to be precise) using appropriate embeddings (so-called decorations); it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making.A comparison of our method to that of embedding LK into LJ (intuitionistic sequent calculus) brings to the fore the latter's defects for these ‘deconstructive purposes’.

Download Full-text

SN and CR for free-style LKtq: linear decorations and simulation of normalization

Journal of Symbolic Logic ◽

10.2178/jsl/1190150036 ◽

2002 ◽

Vol 67 (1) ◽

pp. 162-196 ◽

Cited By ~ 1

Author(s):

Jean-Baptiste Joinet ◽

Harold Schellinx ◽

Lorenzo Tortora De Falco

Keyword(s):

Classical Logic ◽

Sequent Calculus ◽

Linear Logic ◽

Present Report ◽

Point Of View ◽

Strong Normalization ◽

Structural Rules ◽

Specific Combination ◽

Proof Nets ◽

Classical Proof

AbstractThe present report is a, somewhat lengthy, addendum to [4], where the elimination of cuts from derivations in sequent calculus for classical logic was studied ‘from the point of view of linear logic’. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives.The main novelty here is the observation that this type-distinction is not essential: we can allow classical sequent derivations to use any combination of additive and multiplicative introduction rules for each of the connectives, and still have strong normalization and confluence of tq-reductions.We give a detailed description of the simulation of tq-reductions by means of reductions of the interpretation of any given classical proof as a proof net of PN2 (the system of second order proof nets for linear logic), in which moreover all connectives can be taken to be of one type, e.g., multiplicative.We finally observe that dynamically the different logical cuts, as determined by the four possible combinations of introduction rules, are independent: it is not possible to simulate them internally, i.e.. by only one specific combination, and structural rules.

Download Full-text

Multiple conclusion linear logic: cut elimination and more

Journal of Logic and Computation ◽

10.1093/logcom/exaa006 ◽

2020 ◽

Vol 30 (1) ◽

pp. 157-174 ◽

Cited By ~ 1

Author(s):

Harley Eades III ◽

Valeria de Paiva

Keyword(s):

Sequent Calculus ◽

Linear Logic ◽

Direct Proof ◽

Cut Elimination ◽

Tensor Model ◽

Double Negation ◽

Proof Nets ◽

Small Change ◽

Definition Of ◽

Intuitionistic Linear Logic

Abstract Full intuitionistic linear logic (FILL) was first introduced by Hyland and de Paiva, and went against current beliefs that it was not possible to incorporate all of the linear connectives, e.g. tensor, par and implication, into an intuitionistic linear logic. Bierman showed that their formalization of FILL did not enjoy cut elimination as such, but Bellin proposed a small change to the definition of FILL regaining cut elimination and using proof nets. In this note we adopt Bellin’s proposed change and give a direct proof of cut elimination for the sequent calculus. Then we show that a categorical model of FILL in the basic dialectica category is also a linear/non-linear model of Benton and a full tensor model of Melliès’ and Tabareau’s tensorial logic. We give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor. Lastly, we introduce a new library to be used in the proof assistant Agda for proving properties of dialectica categories.

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

Concurrent programming as proof net construction

Mathematical Structures in Computer Science ◽

10.1017/s0960129598002655 ◽

1998 ◽

Vol 8 (6) ◽

pp. 681-710

Author(s):

G. PERRIER

Keyword(s):

Proof Theory ◽

Linear Logic ◽

Concurrent Programming ◽

Process Calculus ◽

Concurrent Process ◽

First Order ◽

Proof Nets ◽

Intuitionistic Linear Logic

We propose a concurrent process calculus, called Calcul Parallèle Logique (CPL), based on the paradigm of computation as proof net construction in linear logic. CPL uses a fragment of first-order intuitionistic linear logic where formulas represent processes and proof nets represent successful computations. In these computations, communication is expressed in an asynchronous way by means of axiom links. We define testing equivalences for processes, which are based on a concept of interface, and use the power of proof theory in linear logic.

Download Full-text

Jump from parallel to sequential proofs: exponentials

Mathematical Structures in Computer Science ◽

10.1017/s0960129516000414 ◽

2016 ◽

Vol 28 (7) ◽

pp. 1204-1252

Author(s):

PAOLO DI GIAMBERARDINO

Keyword(s):

Distinctive Feature ◽

Linear Logic ◽

The Other ◽

Cut Elimination ◽

Strong Normalization ◽

Structural Rules ◽

New Class ◽

Game Semantics ◽

Proof Nets

In previous works, by importing ideas from game semantics (notably Faggian–Maurel–Curien'sludics nets), we defined a new class of multiplicative/additive polarized proof nets, calledJ-proof nets. The distinctive feature of J-proof nets with respect to other proof net syntaxes, is the possibility of representing proof nets which are partially sequentialized, by usingjumps(that is, untyped extra edges) as sequentiality constraints. Starting from this result, in the present work, we extend J-proof nets to the multiplicative/exponential fragment, in order to take into account structural rules: More precisely, we replace the familiar linear logic notion of exponential box with a less restricting one (calledcone) defined by means of jumps. As a consequence, we get a syntax for polarized nets where, instead of a structure of boxes nested one into the other, we have one of cones which can bepartially overlapping. Moreover, we define cut-elimination for exponential J-proof nets, proving, by a variant of Gandy's method, that even in case of ‘superposed’ cones, reduction enjoys confluence and strong normalization.

Download Full-text

A lambda calculus for quantum computation with classical control

Mathematical Structures in Computer Science ◽

10.1017/s0960129506005238 ◽

2006 ◽

Vol 16 (3) ◽

pp. 527-552 ◽

Cited By ~ 68

Author(s):

PETER SELINGER ◽

BENOIT VALIRON

Keyword(s):

Linear Logic ◽

Operational Semantics ◽

Type System ◽

Lambda Calculus ◽

Quantum Computers ◽

Safety Properties ◽

Control Paradigm ◽

Flow Charts ◽

Classical Control ◽

Intuitionistic Linear Logic

In this paper we develop a functional programming language for quantum computers by extending the simply-typed lambda calculus with quantum types and operations. The design of this language adheres to the ‘quantum data, classical control’ paradigm, following the first author's work on quantum flow-charts. We define a call-by-value operational semantics, and give a type system using affine intuitionistic linear logic. The main results of this paper are the safety properties of the language and the development of a type inference algorithm.

Download Full-text