Auswahl der wissenschaftlichen Literatur zum Thema „Multiplicative-additive linear logic“

Even though the multiplicative–additive fragment of linear logic forbids structural rules in general, is does admit a bounded form of exponential modalities enjoying a bounded form of structural rules. The approximation theorem, originally proved by Girard, states that if full linear logic proves a propositional formula, then the multiplicative–additive fragment proves every bounded approximation of it. This may be understood as the fact that multiplicative–additive linear logic is somehow dense in full linear logic. Our goal is to give a technical formulation of this informal remark. We introduce a Cauchy-complete space of infinitary affine term-proofs and we show that it yields a fully complete model of multiplicative exponential polarised linear logic, in the style of Girard's ludics. Moreover, the subspace of finite term-proofs, which is a model of multiplicative polarised linear logic, is dense in the space of all term-proofs.

AbstractRecently, Lincoln, Scedrov and Shankar showed that the multiplicative fragment of second order intuitionistic linear logic is undecidable, using an encoding of second order intuitionistic logic. Their argument applies to the multiplicative-additive fragment, but it does not work in the classical case, because second order classical logic is decidable. Here we show that the multiplicative-additive fragment of second order classical linear logic is also undecidable, using an encoding of two-counter machines originally due to Kanovich. The faithfulness of this encoding is proved by means of the phase semantics.

AbstractWe introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers and which arise from observing restrictions on structural rules on the level of terms as well as propositions. We discuss computational interpretations, based on sharing, at both the propositional and predicate levels.

Subexponential logic is a variant of linear logic with a family of exponential connectives – called subexponentials – that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that a classical propositional multiplicative subexponential logic (MSEL) with one unrestricted and two linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable. We then show how the additive connectives can be directly simulated by giving an encoding of propositional multiplicative additive linear logic (MALL) in an MSEL with one unrestricted and four linear subexponentials.

HyLL (Hybrid Linear Logic) is an extension of intuitionistic linear logic (ILL) that has been used as a framework for specifying systems that exhibit certain modalities. In HyLL, truth judgements are labelled by worlds (having a monoidal structure) and hybrid connectives (at and ↓) relate worlds with formulas. We start this work by showing that HyLL's axioms and rules can be adequately encoded in linear logic (LL), so that one focused step in LL will correspond to a step of derivation in HyLL. This shows that any proof in HyLL can be exactly mimicked by a LL focused derivation. Another extension of LL that has extensively been used for specifying systems with modalities is Subexponential Linear Logic (SELL). In SELL, the LL exponentials (!, ?) are decorated with labels representing locations, and a pre-order on such labels defines the provability relation. We propose an encoding of HyLL into SELL⋒ (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. More precisely, we identify worlds as locations, and show that a flat subexponential structure is sufficient for representing any world structure in HyLL. This shows that HyLL's monoidal structure is not reflected in LL derivations, hence not increasing the expressiveness of LL, from a proof theoretical point of view. We conclude by proposing the notion of fixed points in multiplicative additive HyLL (μHyMALL), which can be encoded into multiplicative additive linear logic with fixed points (μMALL). As an application, we propose encodings of Computational Tree Logic (CTL) into both μMALL and μHyMALL. In the former, states are represented as atoms in the linear context, hence reflecting a more operational view of CTL connectives. In the latter, worlds represent states of the transition system, thus exhibiting a pleasant similarity with the semantics of CTL.

AbstractRecently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic (MALL) and for affine logic (LLW), i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL (which we call IMALL), and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model property for contractive linear logic (LLC), i.e., linear logic with contraction. and for its intuitionistic version (ILLC). The finite model property for related substructural logics also follow by our method. In particular, we shall show that the property holds for all of FL and GL−-systems except FLc and of Ono [11], that will settle the open problems stated in Ono [12].

AbstractWe construct a geometry of interaction (GoI: dynamic modelling of Gentzen-style cut elimination) for multiplicative-additive linear logic (MALL) by employing Bucciarelli–Ehrhard indexed linear logic MALL(I) to handle the additives. Our construction is an extension to the additives of the Haghverdi–Scott categorical formulation (a multiplicative GoI situation in a traced monoidal category) for Girard’s original GoI 1. The indices are shown to serve not only in their original denotational level, but also at a finer grained dynamic level so that the peculiarities of additive cut elimination such as superposition, erasure of subproofs, and additive (co-) contraction can be handled with the explicit use of indices. Proofs are interpreted as indexed subsets in the category Rel, but without the explicit relational composition; instead, execution formulas are run pointwise on the interpretation at each index, with respect to symmetries of cuts, in a traced monoidal category with a reflexive object and a zero morphism. The sets of indices diminish overall when an execution formula is run, corresponding to the additive cut-elimination procedure (erasure), and allowing recovery of the relational composition. The main theorem is the invariance of the execution formulas along cut elimination so that the formulas converge to the denotations of (cut-free) proofs.

Cette thèse s'intéresse à l'égalité des preuves et des formules en logique linéaire, avec des contributions en particulier dans le fragment multiplicatif-additif de cette logique. En logique linéaire, et dans de nombreuses autres logiques (telle que la logique intuitionniste), on dispose de deux transformations sur les preuves : l'élimination des coupures et l'expansion des axiomes. On souhaite très souvent identifier deux preuves reliées par ces transformations, étant donné qu'elles le sont sémantiquement (dans un modèle catégorique par exemple). Cette situation est similaire à celle du λ-calcul où les termes sont identifiés à β-réduction et η-expansion près, opérations qui, par le prisme de la correspondance de Curry-Howard, se rapportent respectivement à l'élimination des coupures et à l'expansion des axiomes. Nous montrons ici que cette identification des preuves correspond exactement à l'identification des preuves à commutation de règle près, qui est une troisième opération sur les preuves bien connue et plus facile à manipuler. Notre démonstration considère uniquement la logique linéaire multiplicative-additive, même si nous conjecturons que ce résultat est vrai pour la logique linéaire dans son entièreté.Non seulement des preuves peuvent être identifiées à élimination des coupures et expansion des axiomes près, mais aussi des formules. Deux formules sont isomorphes si elles sont reliées par des preuves dont les compositions donnent l'identité, toujours à élimination des coupures et expansion des axiomes près. Ces formules sont alors réellement considérées comme les mêmes, et toute utilisation de l'une peut être remplacée par une utilisation de l'autre. Nous donnons une théorie équationnelle caractérisant exactement les formules isomorphes dans la logique linéaire multiplicative-additive. Un problème généralisant les isomorphismes est celui des rétractions, qui intuitivement correspondent aux couples de formules où la première peut être remplacée par la seconde - mais pas nécessairement la seconde par la première, contrairement aux isomorphismes. Étudier les rétractions est bien plus complexe, et nous avons caractérisé les rétractions des atomes dans le fragment multiplicatif de la logique linéaire.Pour l'étude des deux problèmes précédents, la syntaxe usuelle des preuves du calcul des séquents semble mal adaptée, car on considère des preuves à commutation de règle prés. Une partie de la logique linéaire possède une meilleure syntaxe dans ce cas : les réseaux de preuve, qui sont des graphes représentant des preuves quotientées par les commutations de règle. Cette syntaxe fut un outil indispensable pour caractériser isomorphismes et rétractions. Malheureusement, les réseaux de preuve ne sont pas (ou mal) définis en présence des unités. Pour nos problèmes, cette restriction conduit à une étude du cas sans unité dans les réseaux avec le coeur de la démonstration, précédé d'un travail en calcul des séquents pour prendre en compte les unités.Cette thèse développe par ailleurs une partie de la théorie des réseaux de preuve en fournissant une simple preuve du théorème de séquentialisation, qui relie les deux syntaxes des réseaux de preuve et du calcul des séquents, justifiant qu'elles décrivent les mêmes objets sous-jacents. Cette nouvelle démonstration s'obtient comme corollaire d'une généralisation du théorème de Yeo. Ce dernier résultat s'exprime entièrement dans la théorie des graphes aux arêtes colorées, et permet de déduire des preuves de sequentialisation pour différentes définitions de réseaux de preuve. Enfin, nous avons aussi formalisé les réseaux de preuve du fragment multiplicatif de la logique linéaire dans l'assistant de preuve Coq, avec en particulier une implémentation de notre nouvelle preuve de séquentialisation
This study is concerned with the equality of proofs and formulas in linear logic, with in particular contributions for the multiplicative-additive fragment of this logic. In linear logic, and as in many other logics (such as intuitionistic logic), there are two transformations on proofs: cut-elimination and axiom-expansion. One often wishes to identify two proofs related by these transformations, as it is the case semantically (in a categorical model for instance). This situation is similar to the one in the λ-calculus where terms are identified up to β-reduction and η-expansion, operations that, through the prism of the Curry-Howard correspondence, are related respectively to cut-elimination and axiom-expansion. We show here that this identification corresponds exactly to identifying proofs up to rule commutation, a third well-known operation on proofs which is easier to manipulate. We prove so only in multiplicative-additive linear logic, even if we conjecture such a result holds in full linear logic.Not only proofs but also formulas can be identified up to cut-elimination and axiom-expansion. Two formulas are isomorphic if there are proofs between them whose compositions yield identities, still up to cut-elimination and axiom-expansion. These formulas are then really considered to be the same, and every use of one can be replaced with one use of the other. We give an equational theory characterizing exactly isomorphic formulas in multiplicative-additive linear logic. A generalization of an isomorphism is a retraction, which intuitively corresponds to a couple of formulas where the first can be replaced by the second -- but not necessarily the other way around, contrary to an isomorphism. Studying retractions is more complicated, and we characterize retractions to an atom in the multiplicative fragment of linear logic.When studying the two previous problems, the usual syntax of proofs from sequent calculus seems ill-suited because we consider proofs up to rule commutation. Part of linear logic can be expressed in a better adapted syntax in this case: proof-nets, which are graphs representing proofs quotiented by rule commutation. This syntax was an instrumental tool for the characterization of isomorphisms and retractions. Unfortunately, proof-nets are not (or badly) defined with units. Concerning our issues, this restriction leads to a study of the unit-free case by means of proof-nets with the crux of the demonstration, preceded by a work in sequent calculus to handle the units. Besides, this thesis also develops part of the theory of proof-nets by providing a simple proof of the sequentialization theorem, which relates the two syntaxes of proof-net and sequent calculus, substantiating that they describe the same underlying objects. This new demonstration is obtained as a corollary of a generalization of Yeo's theorem. This last result is fully expressed in the theory of edge-colored graphs, and allows to recover proofs of sequentialization for various definitions of proof-nets. Finally, we also formalized proof-nets for the multiplicative fragment of linear logic in the proof assistant Coq, with notably an implementation of our new sequentialization proof

AbstractMechanisation of programming language research is of growing interest, and the act of mechanising type systems and their metatheory is generally becoming easier as new techniques are invented. However, state-of-the-art techniques mostly rely on structurality of the type system — that weakening, contraction, and exchange are admissible and variables can be used unrestrictedly once assumed. Linear logic, and many related subsequent systems, provide motivations for breaking some of these assumptions.We present a framework for mechanising the metatheory of certain substructural type systems, in a style resembling mechanised metatheory of structural type systems. The framework covers a wide range of simply typed syntaxes with semiring usage annotations, via a metasyntax of typing rules. The metasyntax for the premises of a typing rule is related to bunched logic, featuring both sharing and separating conjunction, roughly corresponding to the additive and multiplicative features of linear logic. We use the uniformity of syntaxes to derive type system-generic renaming, substitution, and a form of linearity checking.