There's no substitute for linear logic

Philip Wadler

University of Glasgow?

24 December 1991

Abstract

Surprisingly, there is not a good fit between a syntax for linear logic in the style of Abramsky, and a semantics in the style of Seely. Notably, the Substitution Lemma is valid if and only if !A and !!A are isomorphic in a canonical way. An alternative syntax is proposed, that has striking parallels to Moggi's language for monads. In the old syntax, some terms look like the identity that should not, and vice versa; the new syntax eliminates this awkwardness.

1 Introduction

This paper has two purposes: to show that linear logic has no substitute, and to propose one.

The first part presents a standard syntax and semantics for linear logic, and notes some resulting difficulties. The linear logic is that of Girard [Gir87]. The syntax is based on lambda terms, following in the footsteps of Abramsky [Abr90]: the four rules associated with the `of course' type, Weakening, Contraction, Dereliction, and Promotion, are each represented by a separate term form. The semantics is based on category theory, following in the footsteps of Seely [See89]: Weakening and Contraction are modelled by a comonoid, while Dereliction and Promotion are modelled by a comonad.

Surprisingly, when you combine a syntax like Abramsky's with a semantics like Seely's, various problems arise. For one thing, there is a term that looks as if it denotes the identity, though it does not; and a term that does not look as if it denotes the identity, though it does. For another, the Substitution Lemma does not hold!

The Substitution Lemma is essential: it guarantees that ((>=x : b) a) and b[a=x ] have the same meaning. Fortunately, there is a simple fix. A necessary and sufficient condition for The Substitution Lemma to holds is that !A and !!A be isomorphic in a canonical way. This explains the occurrence of similar restrictions in the work of O'Hearn [O'He91] and Filinski [Fil92].

?Author's address: Department of Computing Science, University of Glasgow, G12 8QQ, Scotland. Electronic mail: [email protected]. Phone: +44 41 330 4966. Fax: +44 41 330 4913.