Geometry of interaction explained

In proof theory, the Geometry of Interaction (GoI) was introduced by Jean-Yves Girard shortly after his work on linear logic. In linear logic, proofs can be seen as various kinds of networks as opposed to the flat tree structures of sequent calculus. To distinguish the real proof nets from all the possible networks, Girard devised a criterion involving trips in the network. Trips can in fact be seen as some kind of operator acting on the proof. Drawing from this observation, Girard[1] described directly this operator from the proof and has given a formula, the so-called execution formula, encoding the process of cut elimination at the level of operators. Subsequent constructions by Girard proposed variants in which proofs are represented as flows[2], or operators in von Neumann algebras[3] . Those models were later generalised by Seiller's Interaction Graphs models[4] .

One of the first significant applications of GoI was a better analysis[5] of Lamping's algorithm[6] for optimal reduction for the lambda calculus. GoI had a strong influence on game semantics for linear logic and PCF.

Beyond the dynamic interpretation of proofs, geometry of interaction constructions provide models of linear logic, or fragments thereof. This aspect has been extensively studied by Seiller[7] under the name of linear realisability, a version of realizability accounting for linearity.

GoI has been applied to deep compiler optimisation for lambda calculi.[8] A bounded version of GoI dubbed the Geometry of Synthesis has been used to compile higher-order programming languages directly into static circuits.[9]

Further reading

Notes and References

  1. Girard . Jean-Yves . 1989 . Geometry of interaction 1: Interpretation of System F . Studies in Logic and the Foundations of Mathematics . 127 . 221-260.
  2. Girard . Jean-Yves . 1995 . Geometry of Interaction III: accomodating the additives. London Mathematical Society Lecture Notes Series . 329-389.
  3. Girard . Jean-Yves . 2011 . Geometry of interaction V: logic in the hyperfinite factor . Theoretical Computer Science . 412 . 20 . 1860-1883.
  4. Seiller . Thomas . 2016 . Interaction graphs: Full linear logic . Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science.
  5. Book: Gonthier . G. . Abadi . M. N. . Lévy . J. J. . 10.1145/143165.143172 . The geometry of optimal lambda reduction . Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '92 . 15 . 1992 . 0897914538 . 7265545 .
  6. Book: Lamping . J. . An algorithm for optimal lambda calculus reduction . 10.1145/96709.96711 . Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90 . 16–30 . 1990 . 0897913434 . 16333787 .
  7. Seiller . Thomas . 2024 . Mathematical Informatics . Habilitation . Université Sorbonne Paris Nord .
  8. Book: Mackie . I. . The geometry of interaction machine . 10.1145/199448.199483 . Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '95 . 198–208 . 1995 . 0897916921 . 19000897 .
  9. Dan R. Ghica. Function Interface Models for Hardware Compilation. MEMOCODE 2011. http://www.cs.bham.ac.uk/~drg/papers/memocode11.pdf

This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "Geometry of interaction".

Except where otherwise indicated, Everything.Explained.Today is © Copyright 2009-2024, A B Cryer, All Rights Reserved. Cookie policy.