stringtranslate.com

Geometría de la interacción

En teoría de pruebas , 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 pruebas pueden verse como varios tipos de redes en oposición a las estructuras de árbol planas del cálculo secuencial . Para distinguir las redes de prueba reales de todas las redes posibles, Girard ideó un criterio que involucra viajes en la red. De hecho, los viajes pueden verse como algún tipo de operador [ aclaración necesaria ] que actúa sobre la prueba. A partir de esta observación, Girard [1] describió directamente este operador a partir de la prueba y ha dado 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 pruebas se representan como flujos [2] u operadores en álgebras de von Neumann [3] . Estos modelos fueron generalizados más tarde 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 lógica lineal y PCF .

Más allá de la interpretación dinámica de las pruebas, las construcciones de geometría de interacción proporcionan modelos de lógica lineal o fragmentos de ella. Este aspecto ha sido estudiado extensamente por Seiller [7] bajo el nombre de realizabilidad lineal, una versión de la realizabilidad que da cuenta de la linealidad.

GoI se ha aplicado a la optimización profunda del compilador 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]

Referencias

  1. ^ Girard, Jean-Yves (1989). "Geometría de la interacción 1: interpretación del sistema F". Estudios de lógica y fundamentos de las matemáticas . 127 : 221–260.
  2. ^ Girard, Jean-Yves (1995). "Geometría de la interacción III: acomodación de los aditivos". Serie de notas de conferencias de la London Mathematical Society : 329–389.
  3. ^ Girard, Jean-Yves (2011). "Geometría de la interacción V: lógica en el factor hiperfinito". Ciencias de la Computación Teórica . 412 (20): 1860–1883.
  4. ^ Seiller, Thomas (2016). "Gráficos de interacción: lógica lineal completa". Actas del 31.º Simposio anual ACM/IEEE sobre lógica en informática .
  5. ^ Gonthier, G.; Abadi, MN; Lévy, JJ (1992). "La geometría de la reducción lambda óptima". Actas del 19.º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación - POPL '92 . pág. 15. doi :10.1145/143165.143172. ISBN 0897914538.S2CID 7265545  .
  6. ^ 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 . págs. 16-30. doi :10.1145/96709.96711. ISBN 0897913434. Número de identificación del sujeto  16333787.
  7. ^ Seiller, Thomas (2024). Informática Matemática (Tesis de Habilitación). Universidad Sorbona París Norte.
  8. ^ 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 . pp. 198–208. doi :10.1145/199448.199483. ISBN 0897916921.S2CID 19000897  .
  9. ^ Dan R. Ghica. Modelos de interfaz de funciones para compilación de hardware. MEMOCODE 2011. [1]

Lectura adicional