Геометрия взаимодействия
В теории доказательств геометрия взаимодействия (GoI) была введена Жаном-Ивом Жираром вскоре после его работы по линейной логике . В линейной логике доказательства можно рассматривать как различные виды сетей, в отличие от плоских древовидных структур секвенциального исчисления . Чтобы отличить настоящие сети доказательства от всех возможных сетей, Жирар разработал критерий, включающий отключения в сети. На самом деле поездки можно рассматривать как своего рода оператор. [ нужны разъяснения ] действуя на основании доказательства. Опираясь на это наблюдение, Жирар [1] описал непосредственно этот оператор из доказательства и дал формулу, так называемую формулу выполнения , кодирующую процесс исключения разреза на уровне операторов. Последующие конструкции Жирара предлагали варианты, в которых доказательства представляются в виде потоков. [2] , или операторы в алгебрах фон Неймана [3] . Эти модели позже были обобщены . моделями графов взаимодействия Зейллера [4] .
Одним из первых значительных применений GoI был лучший анализ. [5] алгоритма Лэмпинга [6] для оптимального сокращения лямбда-исчисления . GoI оказал сильное влияние на семантику игр для линейной логики и PCF .
Помимо динамической интерпретации доказательств, геометрия конструкций взаимодействия предоставляет модели линейной логики или ее фрагменты. Этот аспект был подробно изучен Зейллером. [7] под названием линейной реализуемости — вариант реализуемости, учитывающий линейность.
GoI был применен для глубокой оптимизации компилятора для лямбда-исчислений . [8] Ограниченная версия GoI, получившая название «Геометрия синтеза», использовалась для компиляции языков программирования более высокого порядка непосредственно в статические схемы. [9]
Ссылки
[ редактировать ]- ^ Жирар, Жан-Ив (1989). «Геометрия взаимодействия 1: Интерпретация системы F». Исследования по логике и основам математики . 127 : 221–260.
- ^ Жирар, Жан-Ив (1995). «Геометрия взаимодействия III: размещение добавок». Серия конспектов лекций Лондонского математического общества : 329–389.
- ^ Жирар, Жан-Ив (2011). «Геометрия взаимодействия V: логика в гиперконечном факторе». Теоретическая информатика . 412 (20): 1860–1883.
- ^ Зайллер, Томас (2016). «Графы взаимодействия: полная линейная логика». Материалы 31-го ежегодного симпозиума ACM/IEEE по логике в информатике .
- ^ Гонтье, Г.; Абади, Миннесота; Леви, Джей-Джей (1992). «Геометрия оптимального снижения лямбды». Материалы 19-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '92 . п. 15. дои : 10.1145/143165.143172 . ISBN 0897914538 . S2CID 7265545 .
- ^ Лампинг, Дж. (1990). «Алгоритм оптимального сокращения лямбда-исчисления». Материалы 17-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '90 . стр. 16–30. дои : 10.1145/96709.96711 . ISBN 0897913434 . S2CID 16333787 .
- ^ Зайллер, Томас (2024). Математическая информатика (кандидатская диссертация). Университет Сорбонны Париж-Норд.
- ^ Маки, И. (1995). «Геометрия машины взаимодействия». Материалы 22-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '95 . стр. 198–208. дои : 10.1145/199448.199483 . ISBN 0897916921 . S2CID 19000897 .
- ^ Дэн Р. Гика. Модели функционального интерфейса для компиляции аппаратного обеспечения. МЕМОКОД 2011. [1]
Дальнейшее чтение
[ редактировать ]- Учебное пособие по GoI, данное Лораном Ренье в Сиене 07 на семинаре по линейной логике, [2]
- Геометрия взаимодействия в n Lab