nLab linear type theory

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products

Semisimplicity

Morphisms

Internal monoids

Examples

Theorems

In higher category theory

Linear algebra

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology

Introductions

Definitions

Paths and cylinders

Homotopy groups

Basic facts

Theorems

Contents

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\leftarrowde Morgan duality \rightarrowDisjunctive operator
\top00
11\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

(ΣR):𝒞RΣS (\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 SS.

If there is only the strong monoidal functor Σ:S𝒞\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 SS. 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.

References

General

The original article on linear logic is

reviewed in:

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]

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:

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:

An decent review of some of this is in

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

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

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

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

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

Discussion of linear type theory without units is in

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)

Last revised on August 17, 2023 at 17:18:37. See the history of this page for a list of all contributions to it.