Lectures on linear logic.

*(English)*Zbl 0942.03535
CSLI Lecture Notes. 29. Stanford, CA: Stanford University, Center for the Study of Language and Information. x, 200 p. (1992).

This book constitutes a valuable addition to the literature on the linear logic of J.-Y. Girard [Theor. Comput. Sci. 50, No. 1, 1-102 (1987; Zbl 0625.03037)] and subsumes much of his original work, together with further developments by other authors in a self-contained and accessible form. The volume originated from a one-semester course given by the author at the University of Amsterdam in the spring of 1991 and in her words aims at “giving an all-around introduction” (but potentially much more than that). The author does not strive for great generality or completeness but deals with the more “classical” parts of the theory, which are presented in a brilliant style. Special attention is paid to the various formalisms of linear logic, the connection with certain types of categories, the “formulas-as-types” paradigm for linear logic and associated computational interpretations, and Girard’s proof nets for classical linear logic as an analogue of natural deduction. A significant part of the book is devoted to implications of linear logic for other topics, such as coherence theorems in category theory, the theory of Petri nets, and abstract computing machines without garbage collection. On the other hand, the volume does not treat topics such as bounded linear logic, most of the work on decidability problems and Girard’s “geometry of interaction”. Nevertheless, the book is very useful for people who wish to learn linear logic, and it is also likely to be of great interest to specialists in this area, who could derive much inspiration from it.

The book is divided in to 21 chapters. The text is augmented by numerous nontrivial exercises and supplementary notes mentioning additional important topics or giving historical comments. In the introductory chapter, the author starts with two formulations of the “baby example” of the pure theory of conjunction (sequent calculi with left and right introduction rules, and natural deduction with introduction and elimination rules), and then moves on to the “formulas-as-types” idea and the categorical approach, which leads up to a link with parallel computation. To illustrate the latter, there is a brief description of the connection between the theory of Petri nets and the pure theory of tensors. The next four chapters deal with classical and intuitionistic linear logic as collections of derivable sequents and formulas from a syntactical point of view, establish their embeddings into linear logic and contain some comments on types of linear logic and other substructural logics. Chapter 6 contains a discussion of deduction calculus and the “formulas-as-types” idea for intuitionistic linear logic, and Chapter 7, headed “Hilbert-type systems”, gives an axiomatization of linear logic comparable to the well-known axiomatizations of classical logic based on modus ponens and generalization as the only rules. Chapter 8 is concerned with the categorical semantics, and Chapter 9 describes versions of classical and intuitionistic linear logic and certain of their purely propositional subsystems inspired by the connections between linear logic and the theory of \(*\)-autonomous categories initiated by M. Barr [\(*\)-autonomous categories (Lect. Notes Math. 752, Springer, Berlin) (1979; Zbl 0415.18008)], and gives a “minimal” interpretation of the exponential operation “!” in categorical semantics as a comonad with some additional properties, while Chapter 12 proposes another interpretation of it (the abstract categorical interpretation according to Y. Lafont). Chapter 10 expounds an interesting type-theoretical model, the model of Girard domains, also called coherence spaces, and Chapter 11 is concerned with the coherence problem for symmetric monoidal categories corresponding to the tensor fragment of linear logic. Chapters 13-15 give a computational interpretation for an “intuitionistic” fragment of linear logic via a suitable term calculus with evaluation rules corresponding to normalization steps on deductions, while Chapter 16 shows how to implement the evaluations by (abstract) machines. Chapter 17 introduces Girard’s notion of proof nets, and Chapter 18 gives an algorithmic interpretation of cut elimination for them by means of permutations. Chapter 19 discusses and generalizes the notion of multiplicative operator, and Chapter 20 shows that linear logic is undecidable. The last chapter, contributed by D. Roorda, contains a proof of “strong normalization” for cut elimination in linear logic.

The book is divided in to 21 chapters. The text is augmented by numerous nontrivial exercises and supplementary notes mentioning additional important topics or giving historical comments. In the introductory chapter, the author starts with two formulations of the “baby example” of the pure theory of conjunction (sequent calculi with left and right introduction rules, and natural deduction with introduction and elimination rules), and then moves on to the “formulas-as-types” idea and the categorical approach, which leads up to a link with parallel computation. To illustrate the latter, there is a brief description of the connection between the theory of Petri nets and the pure theory of tensors. The next four chapters deal with classical and intuitionistic linear logic as collections of derivable sequents and formulas from a syntactical point of view, establish their embeddings into linear logic and contain some comments on types of linear logic and other substructural logics. Chapter 6 contains a discussion of deduction calculus and the “formulas-as-types” idea for intuitionistic linear logic, and Chapter 7, headed “Hilbert-type systems”, gives an axiomatization of linear logic comparable to the well-known axiomatizations of classical logic based on modus ponens and generalization as the only rules. Chapter 8 is concerned with the categorical semantics, and Chapter 9 describes versions of classical and intuitionistic linear logic and certain of their purely propositional subsystems inspired by the connections between linear logic and the theory of \(*\)-autonomous categories initiated by M. Barr [\(*\)-autonomous categories (Lect. Notes Math. 752, Springer, Berlin) (1979; Zbl 0415.18008)], and gives a “minimal” interpretation of the exponential operation “!” in categorical semantics as a comonad with some additional properties, while Chapter 12 proposes another interpretation of it (the abstract categorical interpretation according to Y. Lafont). Chapter 10 expounds an interesting type-theoretical model, the model of Girard domains, also called coherence spaces, and Chapter 11 is concerned with the coherence problem for symmetric monoidal categories corresponding to the tensor fragment of linear logic. Chapters 13-15 give a computational interpretation for an “intuitionistic” fragment of linear logic via a suitable term calculus with evaluation rules corresponding to normalization steps on deductions, while Chapter 16 shows how to implement the evaluations by (abstract) machines. Chapter 17 introduces Girard’s notion of proof nets, and Chapter 18 gives an algorithmic interpretation of cut elimination for them by means of permutations. Chapter 19 discusses and generalizes the notion of multiplicative operator, and Chapter 20 shows that linear logic is undecidable. The last chapter, contributed by D. Roorda, contains a proof of “strong normalization” for cut elimination in linear logic.

Reviewer: R.Gylys (MR 93i:03083)