Геометрия взаимодействия (ГОИ) был представлен Жан-Ив Жирар вскоре после его работы на линейной логике . В линейной логике доказательства можно рассматривать как различные типы сетей, в отличие от плоских древовидных структур последовательного исчисления . Чтобы отличить настоящие сети доказательства от всех возможных сетей, Жирар разработал критерий, включающий поездки в сети. На самом деле поездки можно рассматривать как своего рода оператор [ требуется пояснение ], действующий на доказательство. Основываясь на этом наблюдении, Жирар прямо описал этот оператор из доказательства и дал формулу, так называемую формулу выполнения , кодирующую процессустранение порезов на уровне операторов.
Одним из первых значительных приложений GoI был улучшенный анализ [1] алгоритма Лэмпинга [2] для оптимального сокращения для лямбда-исчисления . GoI оказал сильное влияние на семантику игр для линейной логики и PCF .
GoI был применен для глубокой оптимизации компилятора для лямбда-исчислений. [3] Ограниченная версия GoI, получившая название Geometry of Synthesis , использовалась для компиляции языков программирования более высокого порядка непосредственно в статические схемы. [4]
Рекомендации
- ^ Gonthier, G .; Абади, Миннесота; Леви, Дж. Дж. (1992). «Геометрия оптимального лямбда-редукции». Материалы 19-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '92 . п. 15. DOI : 10,1145 / 143165,143172 . ISBN 0897914538.
- ^ Лэмпинг, Дж. (1990). «Алгоритм оптимальной редукции лямбда-исчисления». Материалы 17-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '90 . п. 16. DOI : 10,1145 / 96709,96711 . ISBN 0897913434.
- ^ Маки, И. (1995). «Геометрия машины взаимодействия». Материалы 22-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '95 . п. 198. DOI : 10,1145 / 199448,199483 . ISBN 0897916921.
- ^ Дэн Р. Гика. Модели функционального интерфейса для аппаратной компиляции. MEMOCODE 2011. [1]
дальнейшее чтение
- Учебное пособие по GoI, данное в Сиене 07 Лораном Ренье на семинаре по линейной логике, [2]
- Геометрия взаимодействия в nLab