Geometry of Interaction

The Geometry of Interaction (GoI) is a research programme initiated by Jean-Yves Girard. The idea of GoI is to mathematically study the fine algorithmic of Gentzen-style cut elimination.

Many of the reductions or rewrites involved in a cut elimination proof have a strongly algorithmic feel, as they cause a "movement of information." If we are able to capture this intuition precisely, then we would be able to reason about invariants of proofs. Viewing proofs as algorithms, this would mean reasoning about invariants of computation.

Such invariants may seem to be captured by the categorical semantics of proofs. But these are very coarse: if for two proofs M and N of A \vdash B we have a reduction M \rightarrow N, then it is usually the case that \llbracket M \rrbracket = \llbracket N \rrbracket : \llbracket A \rrbracket \to \llbracket B \rrbracket as morphisms of the relevant category. In short: cuts are mathematically invisible!

The GoI program aims to model invariants and properties of syntax that are finer than that. The basic idea is to keep cuts visible, and model them as feedback loops, induced by notions of traced monoidal categories. (Unrelated to traces in concurrency theory.)

As an implementation technique

Ian Mackie proposed a view of GoI as an implementation technique for functional languages in his 1994 thesis and a POPL 1995 paper Mackie 1994, 1995.

This work has been carried forward through the work of researchers such as Dan Ghica, and Koko Muroya.

Please expand.

References

A tutorial introduction to GoI from the categorical aspect is given in

Haghverdi, Esfandiar, and Philip Scott. 2010. ‘Geometry of Interaction and the Dynamics of Proof Reduction: A Tutorial’. In New Structures for Physics, edited by Bob Coecke, 813:357–417. Lecture Notes in Physics. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12821-9_5. pdf

@incollection{haghverdi_geometry_2010,
	series = {Lecture {Notes} in {Physics}},
	title = {Geometry of {Interaction} and the {Dynamics} of {Proof} {Reduction}: {A} {Tutorial}},
	volume = {813},
	url = {http://www.site.uottawa.ca/~phil/papers/HS.GoI-tut.33.pdf},
	booktitle = {New {Structures} for {Physics}},
	publisher = {Springer, Berlin, Heidelberg},
	author = {Haghverdi, Esfandiar and Scott, Philip},
	editor = {Coecke, Bob},
	year = {2010},
	doi = {10.1007/978-3-642-12821-9_5},
	pages = {357--417}
}

GoI was introduced in a series of articles by Girard:

Girard, Jean-Yves. 1989. ‘Geometry of Interaction 1: Interpretation of System F’. In Logic Colloqium ’88, edited by R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo, 221–60. Studies in Logic and the Foundations of Mathematics 127. Elsevier. https://doi.org/10.1016/S0049-237X(08)70271-4.

@incollection{girard_geometry_1989,
	series = {Studies in {Logic} and the {Foundations} of {Mathematics}},
	title = {Geometry of {Interaction} 1: {Interpretation} of {System} {F}},
	number = {127},
	booktitle = {Logic {Colloqium} '88},
	publisher = {Elsevier},
	author = {Girard, Jean-Yves},
	editor = {Ferro, R. and Bonotto, C. and Valentini, S. and Zanardo, A.},
	year = {1989},
	doi = {10.1016/S0049-237X(08)70271-4},
	pages = {221--260}
}

The geometry of interaction machine, as well as the idea of using GoI as an implementation technique, were presented in

Mackie, Ian Craig. 1994. ‘The Geometry of Implementation’. PhD thesis, Imperial College of Science, Technology and Medicine. https://spiral.imperial.ac.uk/handle/10044/1/46072.

@phdthesis{mackie_geometry_1994,
	type = {{PhD} thesis},
	title = {The {Geometry} of {Implementation}},
	url = {https://spiral.imperial.ac.uk/handle/10044/1/46072},
	school = {Imperial College of Science, Technology and Medicine},
	author = {Mackie, Ian Craig},
	year = {1994}
}

Mackie, Ian. 1995. ‘The Geometry of Interaction Machine’. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’95, 198–208. ACM Press. https://doi.org/10.1145/199448.199483.

@inproceedings{mackie_geometry_1995,
	title = {The geometry of interaction machine},
	doi = {10.1145/199448.199483},
	booktitle = {Proceedings of the 22nd {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}  - {POPL} '95},
	publisher = {ACM Press},
	author = {Mackie, Ian},
	year = {1995},
	pages = {198--208}
}}