Геометрия взаимодействия - Geometry of interaction

В Геометрия взаимодействия (GoI) был представлен Жан-Ив Жирар вскоре после его работы над линейная логика. В линейной логике доказательства можно рассматривать как различные типы сетей, в отличие от плоских древовидных структур последовательное исчисление. Чтобы отличить настоящую сети доказательства Из всех возможных сетей Жирар разработал критерий, включающий поездки в сети. Поездки на самом деле можно рассматривать как своего рода оператор[требуется разъяснение ] действуя на основании доказательства. Основываясь на этом наблюдении, Жирар непосредственно описал этот оператор из доказательства и дал формулу, так называемую формула исполнения, кодируя процесс вырезать устранение на уровне операторов.

Одним из первых значительных приложений GoI был лучший анализ[1] алгоритма Лэмпинга[2] для оптимального сокращения лямбда-исчисление. GoI оказал сильное влияние на семантика игры для линейная логика и PCF.

GoI был применен для глубокой оптимизации компилятора для лямбда-исчислений.[3] Ограниченная версия Go I под названием Геометрия синтеза был использован для компиляции языков программирования высшего порядка непосредственно в статические схемы.[4]

использованная литература

  1. ^ Gonthier, G .; Abadi, M. N .; Леви, Дж. Дж. (1992). «Геометрия оптимального лямбда-редукции». Материалы 19-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '92. п. 15. Дои:10.1145/143165.143172. ISBN  0897914538.
  2. ^ Лэмпинг, Дж. (1990). «Алгоритм оптимальной редукции лямбда-исчисления». Материалы 17-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '90. п. 16. Дои:10.1145/96709.96711. ISBN  0897913434.
  3. ^ Маки, И. (1995). «Геометрия машины взаимодействия». Материалы 22-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '95. п. 198. Дои:10.1145/199448.199483. ISBN  0897916921.
  4. ^ Дэн Р. Гика. Модели функционального интерфейса для аппаратной компиляции. МЕМОКОД 2011. [1]

дальнейшее чтение