nLab linear type theory

Idea

Linear type theory is the linear logic-version of type theory. In the definition of (Seely 89, prop. 1.5), following (Girard 87), this is the internal language of/has categorical semantics in star-autonomous categories.

More generally, the term “linear” (as in linear type theory) has over time come to connote internal type theories, and related logical frameworks (sequent calculi, natural deduction) that correspond to (usually symmetric) monoidal categories, where particularly the monoidal product is not assumed to be the cartesian product (reviews include Blute-Panangaden-Seely 94). Indeed, this general notion still faithfully follows the original motivation for the term “linear” as introduced in (Girard 87), since the non-cartesianness of the tensor product means the absence of a diagonal map and hence the impossibility of functions to depend on more than a single (linear) copy of their variables.

In the corresponding logical frameworks, the non-cartesianness means one drops the contraction and weakening rules of inference associated with cartesian structure, but retains the exchange rule corresponding to the symmetry constraint. This general type of “linear logic” takes on many flavors: in addition to the Girard-style language that is naturally interpreted in star-autonomous categories, one has languages for monoidal biclosed categories, symmetric monoidal closed categories, compact closed categories, and others, collectively representing the “multiplicative” core of linear logic as understood in this general sense.

In addition to this “multiplicative” core, one also often studies modalities (comonads) which relate these symmetric monoidal products to cartesian products and coproducts (so-called “additive” operations in linear logic).

Extending these considerations, the dependent type theory-version of linear type theory should be dependent linear type theory.

Linear (dependent) type theory can be argued to be the proper type theory for quantum logic. In this context the linearity of the type theory, hence the absence of diagonal maps in its categorical semantics, corresponds to the no-cloning theorem in quantum physics.

Properties

Categorical semantics

(…)

In star-autonomous categories.

Conjunctive operator	$\leftarrow$de Morgan duality $\rightarrow$	Disjunctive operator
$\top$		$0$
$1$		$\bot$
$\&$		$\oplus$
$\otimes$		$\parr$
$^\bot$		$^\bot$
$\bigwedge$		$\bigvee$
$!$		$?$

(…)

The canonical co-modality

The original axiomatics for linear type theory in (Girard 87) contain in addition to the structures corresponding to a (star-autonomous) symmetric closed monoidal category a certain (co-)modality traditionally denoted “$!$”, the exponential modality. In (Benton 95, Bierman 95) it is noticed (reviewed in (Barber 97, p. 21 (26))) that a natural categorical semantics for this modality identifies it with the comonad that is induced from a strong monoidal adjunction

$$(\Sigma \dashv R) \;\colon\; \mathcal{C} \stackrel{\overset{\Sigma}{\leftarrow}}{\underset{R}{\longrightarrow}} S$$

between the closed symmetric monoidal category $\mathcal{C}$ which interprets the given linear type theory and a cartesian monoidal category $S$.

If there is only the strong monoidal functor $\Sigma \;\colon\; S \longrightarrow \mathcal{C}$ without possibly a right adjoint, then (Barber 97, p. 21 (27)) speaks of the structural fragment of linear type theory.

In (Ponto-Shulman 12) it is observed that this in turn is canonically induced if $\mathcal{C} \simeq \mathcal{C}_\ast$ is the linear type theory over the trivial context of a dependent linear type theory/indexed closed monoidal category with category of contexts being $S$. See at indexed monoidal (infinity,1)-category – Exponential modality and Fock spaces for more on this.

History of linear categorical semantics

There is a long history of logical frameworks of “linear type” and their categorical semantics in various doctrines of monoidal and closed monoidal categories, even though much of the early history predates Girard’s introduction of linear logic (and which therefore do not bear the term “linear”). We give a thumbnail sketch of some of this below.

The founding father could be said to be Joachim Lambek, who was the first to apply deductive systems and particularly the method of Gentzen cut-elimination to what we would now recognize as categorifications of various fragments of propositional logic. It is noteworthy that one of the various first applications of this categorified cut-elimination was to the (linear) doctrine of monoidal biclosed categories, in which Lambek was interested in connection with his linguistic research (Lambek 58); see (Lambek 68, Lambek 69). A principal goal in these papers was to study (and partially solve) the coherence problem for such structures.

Remark

Kelly and Mac Lane then adapted the essential cut-elimination techniques of Lambek to study the (difficult) coherence problem for closed symmetric monoidal categories, in their landmark study KM. Their work cleverly avoided the explicit introduction of logical equipment, presumably in the service of greater self-containment or greater categorical readership, although the debt to Lambek’s pioneering work is clear enough (and is made explicit).

By the late 1970’s, the connections between proof theory, coherence theory, and the categorical semantics of deductive systems had been well elaborated, and again it is noteworthy that there was especial focus on categorical doctrines of general linear type. A largish batch of various fragments of classical logic, particularly in sequent calculus form, together with their categorical semantics, was collected in a book-length study (Szabo 78) by Manfred Szabo, who had been Lambek’s student. (While the categorical semantics of various deductive systems were carefully spelled out in Szabo’s book, this work was unfortunately tainted by overly ambitious claims by Szabo regarding his purported solutions to the relevant coherence problems, in terms of normalization algorithms which turned out not to be Church-Rosser; see Jay 90a.)

Nor were the logical frameworks restricted to those of sequent calculus type. In particular, the Soviet logician Minc and his students had also developed a type theory whose semantics is naturally valued in closed monoidal categories; see Minc 77. This too was in view of coherence problems.

Interest in these problems was of course reawakened and reinvigorated in the light of Girard’s extraordinarily insightful 1987 paper Linear Logic. The connection with closed symmetric monoidal categories and $\ast$-autonomous categories was picked up in very short order by the categorical community; an early account of this connection was given by Seely 89. It was not long before Girard’s very fruitful exposition of linear proof theory and cut-elimination in terms of proof nets, specifically for the multiplicative fragment MLL which is the basic technical core of Girard’s work, was seen as closely related to “extranaturality” graphs (aka KM-graphs) used by Kelly-Mac Lane in their work on the coherence theory for closed symmetric monoidal categories – as well as by other “Australian category theorists” who had developed Kelly’s theory of clubs (which again tended to be most successful for doctrines of linear type).

These aspects are covered in (Blute 91), who treated a number of coherence problems and particularly the method of Lambek/Kelly-Mac Lane as efficiently streamlined through the method of proof nets with connection given to KM-graphs and clubs. Note that all of those applications were towards various fragments of MLL or doctrines of linear type.

From approximately the same time period we also have some work of Barry Jay, who had developed a calculus of terms and their normalization to study coherence for closed monoidal categories. See for instance (Jay 89, Jay 90b). (This does not seem to owe allegiance to Girard’s methods particularly, but it does indicate some contemporaneous thinking on linear types, terms, and their categorical semantics.)

Remark

It should be noted that the “classical” techniques developed by Lambek, Kelly-Mac Lane, and Blute merely yield partial coherence results, in effect evading the notorious “problem of the unit” which had made the full coherence problem for closed monoidal categories seem fearsomely difficult. However, Trimble in his (unpublished) 1994 thesis showed how to re-interpret Girard’s proof nets so that they naturally took the unit into account, and was then able to give a full coherence result for MILL by arranging cut-free nets into a strongly normalizing and confluent rewrite system. Note that while full coherence results for this case had also been proposed by Voreadou and Dole (students of Mac Lane), by Minc and Jay, and also incorrectly by Szabo, none of these earlier approaches were in a position to take advantage of the proof net formalism. For another account of this sort of formalism, specifically for the case of $\ast$-autonomous categories, weakly distributive categories, and full coherence thereof, see Blute-Cockett-Seely-Trimble96.

Meanwhile, the type theory and its categorical semantics for full linear logic, going beyond MLL and taking into account the modalities and the “additive” operations of LL, was also advanced during this time period. A comprehensive description is given in Benton-Bierman-de Paiva-Hyland 92, with an important antecedent in de Paiva’s work on the Dialectica interpretation de Paiva 89. See also Hyland-de Paiva 93, Bierman 95, Barber 97

See also Schalk 04, Melliès 09. Schalk and Melliès have also worked on game-theoretic semantics of theories of linear type – which itself has a long and intricate history.

Finally, in addition to these usual “denotational” categorical semantics, linear logic also has an “operational” categorical semantics, called the Geometry of Interaction, in traced monoidal categories.

Related concepts

• quantum logic, quantum programming

• quantum lambda-calculus

• dependent linear type theory

• propositions as projections

• modal type theory

• geometric homotopy type theory

• stable homotopy type

References

General

The original article on linear logic is

• Jean-Yves Girard, Linear logic, Theoretical Computer Science 50:1, 1987. (pdf)

reviewed in:

• Jean-Yves Girard, part III of Lectures on Logic, European Mathematical Society 2011

Linear type theory as such is made explicit in:

• Simon John Ambler, First Order Linear Logic in Symmetric Monoidal Closed Categories, PhD thesis, Edinburgh (1991) [ECS-LFCS-92-194, pdf, pdf]

  (with categorical semantics in symmetric closed monoidal categories)

• Masahito Hasegawa. Logical predicates for intuitionistic linear type theories, Typed Lambda Calculi and Applications: 4th International Conference, TLCA ‘99, ed. J.-Y. Girard, Lecture Notes in Computer Science 1581, Springer, Berlin, 1999 (pdf)

• pdf

• Daniel Mihályi, Valerie Novitzká, What about Linear Logic in Computer Science?, Acta Polytechnica Hungarica 10 4 (2013) 147-160 [pdf, pdf]

Exposition:

• Philip Wadler, Linear Types can Change the World!, Programming concepts and methods 3, North Holland (1990) [pdf]

Lambek’s syntactic calculus

Several decades before Girard’s article on linear logic, Lambek introduced a sequent calculus without weakening, contraction, or exchange, and described its applications to modeling aspects of natural language (generalizing previous work by Ajdukiewicz and Bar-Hillel on categorial grammar):

• Joachim Lambek. The mathematics of sentence structure . American mathematical monthly, 154-170, 1958. link

Lambek called his system the “syntactic calculus”, while nowadays it is often called Lambek calculus in linguistics.

In “Towards a geometry of interaction” (1989), Girard references Lambek’s 1958 article, and writes that “this work must be acknowledged as a true ancestor to linear logic; its connection to linguistics can be seen as the first serious evidence against the exclusive focus on mathematics” (p.81). On the other hand, Lambek later wrote that his original motivations were actually in homological algebra:

I would now call this system “bilinear logic”, meaning “non-commutative linear logic” or “logic without Gentzen’s three structural rules”. My original name had been “syntactic calculus”, because of its intended application to linguistics; but actually it had been developed in collaboration with George Findlay [1955] in an attempt to understand some basic homological algebra. Alas, our paper was rejected on the grounds that most of our results were to appear in a book by Cartan and Eilenberg [1956], the publication of which had been delayed because of a paper shortage. (Lambek, “Bilinear logic in algebra and linguistics”, Advances in Linear Logic, CUP, 1995)

Categorical semantics

The following articles are about “logics of linear type” and their categorical semantics, although they predate the use of the word “linear” in Girard’s sense. Most have a view motivated in part by categorical coherence problems.

• Joachim Lambek, Deductive systems and categories, Mathematical Systems Theory 2 (1968), 287-318.

• Joachim Lambek, Deductive systems and categories II, Lecture Notes in Math. 86, Springer-Verlag (1969), 76-122.

• G.E. Minc, Closed categories and the theory of proofs, translated from an article in Russian in Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Mat. Instituta im. V.A. Steklova AN SSSR 68 (1977), 83-114. Republished in Grigorii E. Mints, Selected Papers in Proof Theory, Bibliopolis (1992).

• M.E. Szabo, Algebra of Proofs, Studies in Logic and the Foundations of Mathematics, vol. 88 (1978), North-Holland.

• C.B. Jay, Languages for monoidal categories, JPAA 59 (1989), 61-85.

• C.B. Jay, Coherence in category theory and the Church-Rosser property. Unpublished preprint (1990), cited in the following reference.

• C.B. Jay, The structure of free closed categories, JPAA 66 (1990), 271-285.

The categorical semantics of linear type theory in star-autonomous categories was first described in

• R. A. G. Seely, Linear logic, $\ast$-autonomous categories and cofree coalgebras, Contemporary Mathematics 92, 1989. (pdf, ps.gz)

with the first non-syntactic, mathematical categorical model in the same volume:

• Valeria de Paiva, The Dialectica Categories, Contemporary Mathematics 92, 1989. (web)

As mentioned above, generalization of this semantics, restricted to the “multiplicative fragment” but covering doctrines of more general symmetric monoidal closed type (with specific reference to Girard’s work) is given in

• Richard Blute, Linear logic, coherence, and dinaturality, Dissertation, University of Pennsylvania 1991, published in Theoretical Computer Science archive Volume 115 Issue 1, (July 5, 1993) 3-41.

Blute’s thesis derives coherence theorems for various doctrines of “linear type”, including a coherence theorem for symmetric monoidal closed categories due to Kelly and Mac Lane:

• Max Kelly, Saunders MacLane, Coherence in closed categories, JPAA 1 (1971), 97-140 (web)

An decent review of some of this is in

• Richard Blute, Prakash Panangaden, R. A. G. Seely, Fock Space: A Model of Linear Exponential Types (1994) (web)

Extensions of the coherence-theoretic applications of proof nets in Blute’s thesis, to give full solutions to coherence problems, were given in

• Todd Trimble, Linear Logic, Bimodules, and Full Coherence for Autonomous Categories, Rutgers 1994

• Richard Blute, Cockett, R. A. G. Seely, Todd Trimble, Natural deduction and coherence for weakly distributive categories, JPAA 113 (1996), 229-296. (web)

Type theory for full linear logic, together with its categorical interpretation, was developed in

• Nick Benton, Gavin Bierman, Valeria de Paiva, Martin Hyland, Term assignments for intuitionistic linear logic. Technical report 262, Cambridge 1992 (citeseer)

• Martin Hyland, Valeria de Paiva, Full Intuitionistic Linear Logic (extended abstract). Annals of Pure and Applied Logic, 64(3), pp.273-291, 1993. (pdf)

• Andrew Graham Barber, Linear Type Theories, Semantics and Action Calculi, PhD Thesis, Edinburgh 1997 (web, pdf)

Further review and discussion is in

• Gavin M. Bierman, What is a categorical model of intuitionistic linear logic? (web)

The more general case of general symmetric monoidal categories is reviewed and further discussed in

• Andrea Schalk, What is a categorical model for linear logic? (pdf)

• Richard Blute, Philip Scott, Category theory for linear logicians, in: Linear Logic in Computer Science, Cambridge University Press (2004) 3-64 [doi:10.1017/CBO9780511550850.002, pdf]

• Paul-André Melliès , Categorial Semantics of Linear Logic, in Interactive models of computation and program behaviour, Panoramas et synthèses 27, 2009 (pdf)

The interpretation of Girard’s $!$-modality as the comonad induced from a monoidal adjunction between the closed symmetric monoidal category and a cartesian closed category is due to

• G. Bierman, On Intuitionistic Linear Logic PhD thesis, Computing Laboratory, University of Cambridge, 1995 (pdf)

• Nick Benton, A mixed linear and non-linear logic: Proofs, terms and models, in Computer Science Logic. CSL 1994, Lecture Notes in Computer Science 933 [doi:10.1007/BFb0022251, pdf]

Interpretation of this in dependent linear type theory is in

• Kate Ponto, Mike Shulman, Duality and traces for indexed monoidal categories, Theory and Applications of Categories 26 23 (2012) 582-659 [arXiv:1211.1555, tac:26-23]

Further discussion of linear type theory is for instance in

• Chapter 7, Linear type theory pdf

• Anders Schack-Nielsen, Carsten Schürmann, Linear contextual modal type theory pdf

• Bernardo Toninho, Luís Caires, Frank Pfenning, Dependent Session Types via Intuitionistic Linear Type Theory pdf

• Iliano Cervesato, Frank Pfenning, A Linear Logical Framework, 1996, (web)

Discussion of application of linear logic to quantum logic, quantum computing and generally to quantum physics includes

• Vaughan Pratt, Linear logic for generalized quantum mechanics, in Proceedings of Workshop on Physics and Computation (PhysComp’92) (1992) 166-180 [doi:10.1109/PHYCMP.1992.615518, pdf, pdf]

• Ross Duncan, Types for quantum mechanics (2006) [pdf, pdf]

• Gianpiero Cattaneo, Maria Luisa Dalla Chiara, Roberto Giuntini and Francesco Paoli, section 9 of Quantum Logic and Nonclassical Logics, p. 127 in Kurt Engesser, Dov M. Gabbay, Daniel Lehmann (eds.) Handbook of Quantum Logic and Quantum Structures: Quantum Logic, 2009 North Holland

• Ugo Dal Lago, Claudia Faggian, On Multiplicative Linear Logic, Modality and Quantum Circuits (arXiv:1210.0613)

Discussion of linear type theory without units is in

• Robin Houston, Linear Logic without Units (arXiv:1305.2231)

Discussion of inductive types in the context of linear type theory is in

• Stéphane Gimenez, Towards Generic Inductive Constructions in Systems of Nets (pdf)