Abstract

Linear Logic was introduced by Girard [3] as a resource-sensitive refinement of classical logic. Lincoln, Mitchell, Scedrov, and Shankar [13] have proved the undecidability of full propositional Linear Logic. This implies that Linear Logic is more expressive than traditional classical or intuitionistic logic, even if we consider the modalized versions of those logics. In [9, 10] we prove that standard many-counter Minsky machines [17] can be simulated directly in propositional Linear Logic. Here we are going to present a more transparent and fruitful simulation of many-counter Minsky machines in Linear Logic.

Simulating one system of concepts in terms of another system is known to consist of two procedures: (A) Suggesting an encoding of the first system in terms of the second one, and (B) Proving that the encoding suggested is correct and fair.

Here, based on a computational interpretation of Linear Logic [9, 10], we present: (A) A direct and natural encoding of many-counter Minsky machines in Linear Logic, and (B) Transparent proof of the correctness and fairness of this encoding.

As a corollary, we prove that all partial recursive relations are directly definable in propositional Linear Logic.

Introduction and Summary

Linear Logic was introduced by Girard [3] as a resource-sensitive refinement of classical logic. Lincoln, Mitchell, Scedrov, and Shankar [13] have proved the undecidability of full propositional Linear Logic. In [13] the proof of undecidability of propositional Linear Logic consists of a reduction from the Halting Problem for And-Branching Two Counter Machines Without Zero-Test (specified in the same [13]) to a decision problem in Linear Logic.

Introduction

If we consider the interpretation of proofs as programs, say in intuitionistic logic, the question of equality between proofs becomes crucial: The syntax introduces meaningless distinctions whereas the (denotational) semantics makes excessive identifications. This question does not have a simple answer in general, but it leads to the notion of proof-net, which is one of the main novelties of linear logic. This has been already explained in [Gir87] and [GLT89].

The notion of interaction net introduced in [Laf90] comes from an attempt to implement the reduction of these proof-nets. It happens to be a simple model of parallel computation, and so it can be presented independently of linear logic, as in [Laf94]. However, we think that it is also useful to relate the exact origin of interaction nets, especially for readers with some knowledge in linear logic. We take this opportunity to give a survey of the theory of proof-nets, including a new proof of the sequentialization theorem.

Multiplicatives

First we consider the kernel of linear logic, with only two connectives: ⊗ (times or tensor product) and its dual ℘ (par or tensor sum). The first one can be seen as a conjunction and the second one as a disjunction. Each atom has a positive form p and a negative one p⊥ (the linear negation of p).

This volume is based to a large extent on the Linear Logic Workshop held June 14–18, 1993 at the MSI and partially supported by the US Army Research Office and the US Office of Naval Research. The workshop was attended by about 70 participants from the USA, Canada, Europe, and Japan. The workshop program committee was chaired by A. Scedrov (University of Pennsylvania) and included S. Abramsky (Imperial College, London), J.-Y. Girard (CNRS, Marseille), D. Miller (University of Pennsylvania), and J. Mitchell (Stanford). The principal speakers at the workshop were J.-M. Andreoli, A. Blass, V. Danos, J.-Y. Girard, A. Joyal, Y. Lafont, J. Lambek, P. Lincoln, M. Moortgat, R. Pareschi, and V. Pratt. There were also a number of invited 30 minute talks and several software demonstration sessions.

Our intention was not only to publish a volume of proceedings. We also wanted to give an overview of a topic that started almost 10 years ago and that is of interest for mathematicians as well as for computer scientists. For these reasons, the book is divided into 5 parts:

1. Categories and Semantics

2. Complexity and Expressivity

3. Proof Theory

4. Proof Nets

5. Geometry of Interaction

The five parts are preceded by a general introduction to Linear Logic by J.-Y. Girard. Furthermore, parts 2 and 4 start with survey papers by P. Lincoln and Y. Lafont. We hope this book can be useful for those who work in this area as well as for those who want to learn about it. All papers have been refereed and the editors are grateful to A. Scedrov who took care of the refereeing process for the papers written by the the editors themselves.

Abstract

We present a model of classical linear logic based on the notion of strong stability that was introduced in [BE], a work about sequentiality written jointly with Antonio Bucciarelli.

Introduction

The present article is a new version of an article already published, with the same title, in Mathematical Structures in Computer Science (1993), vol. 3, pp. 365–385. It is identical to this previous version, except for a few minor details.

In the denotational semantics of purely functional languages (such as PCF [P, BCL]), types are interpreted as objects and programs as morphisms in a cartesian closed category (CCC for short). Usually, the objects of this category are at least Scott domains, and the morphisms are at least continuous functions. The goal of denotational semantics is to express, in terms of “abstract” properties of these functions, some interesting computational properties of the language.

One of these abstract properties is “continuity”. It corresponds to the basic fact that any computation that terminates can use only a finite amount of data. The corresponding semantics of PCF is the continuous one, where objects are Scott domains, and morphisms continuous functions.

But the continuous semantics does not capture an important property of computations in PCF, namely “determinism”. Vuillemin and Milner are at the origin of the first (equivalent) definitions of sequentiality, a semantic notion corresponding to determinism. Kahn and Plotkin ([KP]) generalized this notion of sequentiality. More precisely, they defined a category of “concrete domains” (represented by “concrete data structures”) and of sequential functions.

Abstract

Girard's execution formula (given in [Gir88a]) is a decomposition of usual β-reduction (or cut-elimination) in reversible, local and asynchronous elementary moves. It can easily be presented, when applied to a λ-term or a net, as the sum of maximal paths on the λ-term/net that are not cancelled by the algebra L* (as was done in [Dan90, Reg92]).

It is then natural to ask for a characterization of those paths, that would be only of geometric nature. We prove here that they are exactly those paths that have residuals in any reduct of the λ-term/net. Remarkably, the proof puts to use for the first time the interpretation of λ-terms/nets as operators on the Hilbert space.

Presentation

λ-Calculus is simple but not completely convincing as a real machine-language. Real machine instructions have a fixed run-time; a β-reduction step does not. Some implementations do map-reductions into sequences of real elementary steps (as in environment machines for example) but they use a global time to achieve this. The “geometry of interaction” (GOI) is an attempt to find a low-level combinatorial code within which β-reduction could be implemented and such that:

• elementary reduction steps are local;

• parallelism shows up and global time disappears;

• some mathematics dealing with syntax is uncovered.

— Goal and organization of this paper.

A persistent path is a path on a λ-term which survives the action of any reduction (defined in [Reg92]). A regular path is a path which is not cancelled by Girard's algebraic device L* (defined in [Gir88a]).

Abstract

We present natural deduction systems for fragments of intuitionistic linear logic obtained by dropping weakening and contractions also on!-prefixed formulas. The systems are based on a two-dimensional generalization of the notion of sequent, which accounts for a clean formulation of the introduction/elimination rules of the modality. Moreover, the different subsystems are obtained in a modular way, by simple conditions on the elimination rule for!. For the proposed systems we introduce a notion of reduction and we prove a normalization theorem.

Introduction

Proof theory of modalities is a delicate subject. The shape of the rules governing the different modalities in the overpopulated world of modal logics is often an example of what a good rule should not be. In the context of sequent calculus, if we want cut elimination, we are often forced to accept rules which are neither left nor right rules, and which completely destroy the deep symmetries the calculus is based upon. In the context of natural deduction the situation is even worse, since we have to admit deduction trees whose subtrees are not deductions, or, in the best case, elimination rules containing in their premise(s) the eliminated connective. On top of this, any such rule do not characterize (in a universal way, as category theoreticians would say) the modality it “defines”: two different modality with the same rules bear no relation among each other (cf. Section 4.1).

Abstract

The paper expounds geometry of interaction, for the first time in the full case, i.e. for all connectives of linear logic, including additives and constants. The interpretation is done within a C*-algebra which is induced by the rule of resolution of logic programming, and therefore the execution formula can be presented as a simple logic programming loop. Part of the data is public (shared channels) but part of it can be viewed as private dialect (defined up to isomorphism) that cannot be shared during interaction, thus illustrating the theme of communication without understanding. One can prove a nilpotency (i.e. termination) theorem for this semantics, and also its soundness w.r.t. a slight modification of familiar sequent calculus in the case of exponential-free conclusions.

Introduction

Towards a monist duality

Geometry of interaction is a new form of semantics. In order to understand what is achieved, one has to discuss the more traditional forms of semantics.

Classical model theory

The oldest view about logic is that of an external observer : there is a preexisting reality (mathematical, let us say) that we try to understand (e.g. by proving theorems). This form of dualism is backed by the so-called completeness theorem of Gödel (1930), which says that a formula is provable iff it is true in all models (i.e. in all realizations). There is strong heterogeneity in the duality world/observer (or model/proof) proposed by model-theory, since the latter is extremely finite whereas the former is infinite. Hilbert's attempt at reducing the gap between the two actors failed because of the renowned incompleteness theorems, also due to Godel (1931), whose basic meaning is that infinity cannot be eliminated.

There has been some disagreement about when circles (or closed curves) began being used for representing classical syllogisms. They seem to have first been put to this use in the Middle Ages. However, there seems to be agreement that it was Leonhrad Euler, in the eighteenth century, who proposed using circles to illustrate relations between classes. This diagrammatic method of Euler's was greatly improved by a nineteenth century logician John Venn. And in this century, it was Charles Peirce who made a great contribution to the further development of Venn diagrams.

This chapter explores the essence of Euler diagrams and their descendants, and will serve to prepare the reader for my approach to Venn diagrams presented in the following chapters. In each section, along with the main ideas of each system and its limits, I focus on how some of the main limits of one system are overcome by the following system. That is, the Venn system solves some of the main problems that the Euler system has. This improvement was significant enough to make necessary a distinction between Euler diagrams and Venn diagrams. I will show that Peirce's revolutionary ideas about diagrams not only overcame some important defects of Venn diagrams but opened the way to a totally new horizon for logical diagrams. This last aspect will be discussed in detail in the third section. I will also point out where this new horizon stopped, and will claim that my approach to Venn diagrams (in Chapters 3 and 4) is the natural completion of these predecessors' incomplete projects.

In this chapter, I claim that Venn-II is equivalent to a first-order language ℒ0, which I will specify in the first section. This claim is supported by two subclaims. One is that for every diagram D of Venn-II, there is a sentence ϕ of ℒ0 such that the set assignments that satisfy D are isomorphic to the structures that satisfy ϕ. The other is that for every sentence ϕ of ℒ0, there is a diagram D of Venn-II such that the structures that satisfy ϕ are isomorphic to the set assignments that satisfy D.

The language of ℒ0

Our first-order language ℒ0 is as follows:

A. Logical Symbols

1. Parentheses: (,)

2. Sentential connective symbols: ¬, ∧, ∨

3. Variables: x1, x2, x3, …

4. Equality: No

B. Parameters

1. Quantifier symbols: ∀, ∃

2. Predicate symbols: 1-place predicate symbols, P1, P2, …

3. Constant symbols: None

4. Function symbols: None

From set assignments to structures

In this section, we want to show that there is an isomorphism between the set of set assignments for Venn-II and the set of structures for ℒ0.

Because we have only one closed curve type and one rectangle, we need an extra mechanism in the semantics of this Venn system. That is a counterpart relation among tokens of a closed curve or among tokens of a rectangle. Before we make a mapping between sets and structures, we need to deal with these cp-related regions.

We are about to formalize a way of using Venn diagrams. Before we present a formalism for this system (we call this system Venn-I), let us see how Venn diagrams are used to test the validity of syllogisms:

1. Draw diagrams to represent the facts that the two premises of a syllogism convey. (Let us call one D1 and the other D2.)

2. Draw a diagram to represent the fact that the conclusion of the syllogism conveys. (Let us call this diagram D.)

3. See if we can read off diagram D from diagram D1 and diagram D2.

4. If we can, then this syllogism is valid.

5. If we cannot, then this syllogism is invalid.

Let us try to be more precise about each step. Step (1) and step (2) raise the following question: How is it possible for a diagram drawn on a piece of paper to represent the information that a premise or a conclusion conveys? These two steps are analogous to the translation from English to a first-order language. Suppose that we test the validity of a syllogism by using a first-order language. How does this translation take place? First of all, we need to know the syntax and the semantics of each language – English and the first-order language. We want to translate an English sentence into a first-order sentence whose meaning is the same as the meaning of the English sentence.