La geometría de la Interacción (GOI) fue presentado por Jean-Yves Girard poco después de su trabajo en la lógica lineal . En lógica lineal, las demostraciones pueden verse como varios tipos de redes en contraposición a las estructuras de árbol plano del cálculo secuencial . Para distinguir las redes de prueba reales de todas las redes posibles, Girard ideó un criterio de viajes en la red. De hecho, los viajes pueden verse como una especie de operador [ aclaración necesaria ] que actúa sobre la prueba. A partir de esta observación, Girard describió directamente este operador de la demostración y ha dado una fórmula, la llamada fórmula de ejecución , que codifica el proceso deEliminación de recortes a nivel de operadores.
Una de las primeras aplicaciones significativas de GoI fue un mejor análisis [1] del algoritmo de Lamping [2] para la reducción óptima del cálculo lambda . GoI tuvo una gran influencia en la semántica del juego para la lógica lineal y PCF .
GoI se ha aplicado a la optimización profunda del compilador para cálculos lambda. [3] Se ha utilizado una versión limitada de GoI denominada Geometry of Synthesis para compilar lenguajes de programación de orden superior directamente en circuitos estáticos. [4]
Referencias
- ^ Gonthier, G .; Abadi, MN; Lévy, JJ (1992). "La geometría de la reducción lambda óptima". Actas del XIX simposio ACM SIGPLAN-SIGACT sobre Principios de lenguajes de programación - POPL '92 . pag. 15. doi : 10.1145 / 143165.143172 . ISBN 0897914538.
- ^ Lamping, J. (1990). "Un algoritmo para la reducción óptima del cálculo lambda". Actas del 17º simposio ACM SIGPLAN-SIGACT sobre Principios de lenguajes de programación - POPL '90 . pag. 16. doi : 10.1145 / 96709.96711 . ISBN 0897913434.
- ^ Mackie, I. (1995). "La geometría de la máquina de interacción". Actas del 22º simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación - POPL '95 . pag. 198. doi : 10.1145 / 199448.199483 . ISBN 0897916921.
- ^ Dan R. Ghica. Modelos de interfaz de función para compilación de hardware. MEMOCODE 2011. [1]
Otras lecturas
- Tutorial de GoI impartido en Siena 07 por Laurent Regnier, en el taller de Lógica Lineal, [2]
- Geometría de interacción en nLab