nLab Geometry of Interaction



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
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


Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products



Internal monoids



In higher category theory


physics, mathematical physics, philosophy of physics

Surveys, textbooks and lecture notes

theory (physics), model (physics)

experiment, measurement, computable physics



What has been called Geometry of Interaction (Girard 89) is a kind of semantics for linear logic/linear type theory that is however different in method from the usual categorical semantics in monoidal categories. Instead of interpreting a proof of a linear entailment ABA\vdash B as a morphism between objects AA and BB in a monoidal category as in categorical semantics, the Geometry of Interaction interprets it as an endomorphism on the object ABA\multimap B. This has been named operational semantics to contrast with the traditional denotational semantics.

That also the “operational semantics” of GoI has an interpretation in category theory, though, namely in compact closed categories induced from traced monoidal categories was first suggested in (Joyal-Street-Verity 96) and then developed in (Hines 97,Haghverdi 00, Abramsky-Haghverdi-Scott 02, Haghverdi-Scott 05). See (Shirahata) for a good review.


Relation to superoperators and quantum operations

We discuss a relation of the GoI to superoperators/quantum operations in quantum physics.

According to (Abramsky-Haghverdi-Scott 02, remark 5.8, Haghverdi 00b, section 6) all the standard and intended interpretations of the GoI take place in those compact closed categories Int(𝒞)Int(\mathcal{C}) free on a traced monoidal category 𝒞\mathcal{C} (as discussed there). In these references therefore the notation Int()Int(-) from (Joyal-Street-Verity 96) is changed to 𝒢()\mathcal{G}(-), for “Geometry of Interaction construction” (see Abramsky-Haghverdi-Scott 02, p. 11).

The objects of Int(𝒞)Int(\mathcal{C}) are pairs (A +,A )(A^+, A^-) of objects of 𝒞\mathcal{C}, a morphism (A +,A )(B +,B )(A^+ , A^-) \to (B^+ , B^-) in Int(𝒞)Int(\mathcal{C}) is given by a morphism in 𝒞\mathcal{C} of the form

A +B A B + \array{ A^+\otimes B^- \\ \downarrow \\ A^- \otimes B^+ }

in 𝒞\mathcal{C}, and composition of two such morphisms (A +,A )(B +,B )(A^+ , A^-) \to (B^+ , B^-) and (B +,B )(C +,C )(B^+ , B^-) \to (C^+ , C^-) is given by tracing out B +B^+ and B B^- in the evident way.

We observe now that subcategories of such Int(𝒞)Int(\mathcal{C}) are famous in quantum physics as “categories of superoperators” or “categories of quantum operations”, formalizing linear maps on spaces of operators on a Hilbert spaces that takes density matrices (hence mixed quantum states) to density matrices (“completely positive maps”).

First notice that if the traced monoidal category structure on 𝒞\mathcal{C} happens to be that induced by a compact closed category structure, then by compact closure the morphisms (A +,A )(B +,B )(A^+ , A^-) \to (B^+ , B^-) in Int(𝒞)Int(\mathcal{C}) above are equivalently morphisms in 𝒞\mathcal{C} of the form

(A ) *A +(B ) *B + (A^-)^\ast \otimes A^+ \longrightarrow (B^-)^\ast \otimes B^+

and if moreover one concentrates on the case where AA A +A \coloneqq A^- \simeq A^+ etc. then these are morphisms of the form

End(A)End(B). End(A) \longrightarrow End(B) \,.

Under this identification the somewhat curious-looking composition in Int(𝒞)Int(\mathcal{C}) given by tracing in 𝒞\mathcal{C} becomes just plain composition in 𝒞\mathcal{C}.

Subcategories (non-full) of Int(𝒞)Int(\mathcal{C}) consisting of morphisms of this form in some ambient 𝒞\mathcal{C} have been considered in (Selinger 05), there denoted CPM(𝒞)CPM(\mathcal{C}), and shown to formalize the concept of quantum operations in quantum physics. For a quick review of Selinger’s construction see for instance (Coecke-Heunen 11, section 2). Comments related to the relation between GoI and such constructions appear in (Abramsky-Coecke 02).

Now the CPM()CPM(-) construction requires and assumes that 𝒞\mathcal{C} has all dual objects (which in the standard model means to restrict to Hilbert spaces of quantum states with are of finite dimension). To generalize away from this requirement a more general definition of quantum operations in 𝒞\mathcal{C} is given in (Coecke-Heunen 11, def. 1), there denoted CP(𝒞)CP(\mathcal{C}). Direct inspection shows that CP(𝒞)CP(\mathcal{C}) is still a (non-full) subcategory of Int(𝒞)Int(\mathcal{C}).


The original references are

  • Jean-Yves Girard. Towards a geometry of interaction. In Categories in Computer Science and Logic, pages 69 – 108, Providence, 1989. American Mathematical Society. Proceedings of Symposia in Pure Mathematics n92.
  • Jean-Yves Girard. Geometry of interaction I: interpretation of system F. In Ferro, Bonotto, Valentini, and Zanardo, editors, Logic Colloquium ‘88, pages 221 – 260, Amsterdam, 1989. North-Holland.

  • Jean-Yves Girard. Geometry of interaction II : deadlock-free algorithms. In Martin-Löf and Mints, editors, Proceedings of COLOG 88, volume 417 of Lecture Notes in Computer Science, pages 76 – 93, Heidelberg, 1990. Springer-Verlag.

  • Jean-Yves Girard. Geometry of interaction III : accommodating the additives. In Girard, Lafont, and Regnier, editors, Advances in Linear Logic, pages 329 – 389, Cambridge, 1995. Cambridge University Press.

  • Jean-Yves Girard. Geometry of interaction IV : the feedback equation. In Stoltenberg-Hansen and Väänänen, editors, Logic Colloquium ‘03, pages 76 – 117. Association for Symbolic Logic, 2006.

  • Jean-Yves Girard. Geometry of interaction V : logic in the hyperfinite factor, in memoriam Claire Delaleu (1991-2009). Fully revised version (October 2009). (pdf)

  • Jean-Yves Girard. Geometry of Interaction VI: a blueprint for Transcendental Syntax, January 2013, revised August 28th 2013. (pdf)

Reviews include

  • Samson Abramsky, E. Haghverdi and P. Scott, “Geometry of Interaction and linear combinatory algebra,” Mathematical Structures in Computer Science (2002), vol. 12, pp. 625-665. (ps)

  • Samson Abramsky and R. Jagadeesan, “New Foundations for the Geometry of Interaction,” Proceedings 7th Annual IEEE Symp. on Logic in Computer Science, LICS’92, Santa Cruz, CA, USA, 22–25 June 1992. (pdf)

  • Harry G. Mairson, “From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple”, Proceedings of FST TCS 2002. (pdf)

  • Linear Logic Wiki, Geometry of Interaction

  • Daniel Murfet, section 5 of Logic and linear algebra: an introduction (arXiv:1407.2650)

The operational categorical semantics in traced monoidal categories is due to

  • Peter Hines?, The Algebra of Self-Similarity and its Applications, PhD Thesis, University of Wales, U.K. 1997 (pdf)
  • Esfandir Haghverdi, A Categorical Approach to Linear Logic, Geometry of Proofs and Full Completeness, PhD Thesis, University of Ottawa, Canada 2000.
  • Esfandir Haghverdi, Unique Decomposition Categories, Geometry of Interaction, and Combinatory Logic, Math. Struc. in Comp. Sci., 10, pp. 205-231.

Discussion of quantum operations/completely positive maps mentioned above is in

  • Peter Selinger, Dagger-compact closed categories and completely positive maps, Electronic Notes in Theoretical Computer

    Science (special issue: Proceedings of the 3rd International Workshop on Quantum Programming Languages). 2005 (pdf, ps)

Last revised on December 15, 2021 at 09:42:39. See the history of this page for a list of all contributions to it.