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.

Connecting Sequent Calculi with Lorenzen-Style Dialogue Games

Lorenzen has introduced his dialogical approach to the foundations of logic in the late 1950s to justify intuitionistic logic with respect to first principles about constructive reasoning. In the decades that have passed since, Lorenzen-style dialogue games turned out to be an inspiration for a more pluralistic approach to logical reasoning that covers a wide array of nonclassical logics. In particular, the close connection between (single-sided) sequent calculi and dialogue games is an invitation to look at substructural logics from a dialogical point of view. Focusing on intuitionistic linear logic, we illustrate that intuitions about resource-conscious reasoning are well served by translating sequent calculi into Lorenzen-style dialogue games. We suggest that these dialogue games may be understood as games of information extraction, where a sequent corresponds to the claim that a certain information package can be systematically extracted from a given bundle of such packages of logically structured information. As we will indicate, this opens the field for exploring new logical connectives arising by consideration of further forms of storing and structuring information.

COMPLEXITY OF THE INFINITARY LAMBEK CALCULUS WITH KLEENE STAR

We consider the Lambek calculus, or noncommutative multiplicative intuitionistic linear logic, extended with iteration, or Kleene star, axiomatised by means of an $\omega $ -rule, and prove that the derivability problem in this calculus is $\Pi _1^0$ -hard. This solves a problem left open by Buszkowski (2007), who obtained the same complexity bound for infinitary action logic, which additionally includes additive conjunction and disjunction. As a by-product, we prove that any context-free language without the empty word can be generated by a Lambek grammar with unique type assignment, without Lambek’s nonemptiness restriction imposed (cf. Safiullin, 2007).

Cofree coalgebras and differential linear logic

We prove that the semantics of intuitionistic linear logic in vector spaces which uses cofree coalgebras is also a model of differential linear logic, and that the Cartesian closed category of cofree coalgebras is a model of the simply typed differential λ-calculus.

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

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.

Multiple conclusion linear logic: cut elimination and more

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.

Hybrid linear logic, revisited

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.