Geometría de interacción

En la teoría de la demostración , la Geometría de Interacción (GdI) fue introducida por Jean-Yves Girard poco después de su trabajo sobre lógica lineal . En lógica lineal, las demostraciones pueden verse como diversos tipos de redes, en contraposición a las estructuras de árbol planas del cálculo de secuentes . Para distinguir las redes de demostración reales de todas las redes posibles, Girard ideó un criterio que involucra viajes en la red. Los viajes pueden verse, de hecho, como una especie de operador que actúa sobre la demostración. Partiendo de esta observación, Girard ^{[ 1 ]} describió directamente este operador a partir de la demostración y proporcionó una fórmula, la llamada fórmula de ejecución , que codifica el proceso de eliminación de cortes a nivel de operadores. Construcciones posteriores de Girard propusieron variantes en las que las demostraciones se representan como flujos ^{[ 2 ]} u operadores en álgebras de von Neumann ^{[ 3 ]} . Estos modelos fueron generalizados posteriormente por los modelos de Grafos de Interacción de Seiller ^{[ 4 ] .}

Una de las primeras aplicaciones significativas de GoI fue un mejor análisis ^{[ 5 ]} del algoritmo de Lamping ^{[ 6 ]} para la reducción óptima del cálculo lambda . GoI tuvo una fuerte influencia en la semántica de juegos para la lógica lineal y PCF .

Más allá de la interpretación dinámica de las demostraciones, la geometría de las construcciones de interacción proporciona modelos de lógica lineal , o fragmentos de la misma. Este aspecto ha sido estudiado exhaustivamente por Seiller ^{[ 7 ]} bajo el nombre de realizabilidad lineal, una versión de la realizabilidad que tiene en cuenta la linealidad.

GoI se ha aplicado a la optimización profunda de compiladores para cálculos lambda . ^{[ 8 ]} Una versión limitada de GoI, denominada Geometría de Síntesis, se ha utilizado para compilar lenguajes de programación de orden superior directamente en circuitos estáticos. ^{[ 9 ]}

• Tutorial de GoI impartido en Siena 07 por Laurent Regnier, en el taller de Lógica Lineal,
• Geometría de la interacción en el laboratorio n