Явная замена
 | Эта статья может быть слишком технической для понимания большинства читателей . ( Май 2023 г. ) |
В информатике , что лямбда-исчисления говорят имеют явные замены , если они уделяют особое внимание формализации процесса замены . В этом отличие от стандартного лямбда-исчисления , в котором замены выполняются путем бета-сокращений неявным образом, который не выражается в исчислении; условия «свежести» в таких неявных исчислениях являются печально известным источником ошибок. [1] Эта концепция появилась в большом количестве опубликованных статей в самых разных областях, например, в абстрактных машинах , логике предикатов и символьных вычислениях .
Обзор [ править ]
Простым примером лямбда-исчисления одну новую форму термина с явной заменой является «λx», который добавляет к лямбда-исчислению , а именно форму M⟨x:=N⟩, которая читается как «M, где x будет заменен на N». . (Значение нового термина такое же, как и распространенная идиома let x:=N в M из многих языков программирования.) λx можно записать с использованием следующих правил переписывания :
- (λx.M) N → M⟨x:=N⟩
- x⟨x:=N⟩ → N
- x⟨y:=N⟩ → x (x≠y)
- (M 1 M 2 ) ⟨x:=N⟩ → (M 1 ⟨x:=N⟩) (M 2 ⟨x:=N⟩)
- (λx.M) ⟨y:=N⟩ → λx.(M⟨y:=N⟩) (x≠y и x не свободны в N)
Несмотря на явную замену, эта формулировка по-прежнему сохраняет сложность «соглашения о переменных» лямбда-исчисления , требуя произвольного переименования переменных во время сокращения, чтобы гарантировать, что условие «(x≠y и x не свободно в N)» в последнем правиле всегда удовлетворен перед применением правила. Поэтому многие исчисления явной подстановки вообще избегают имен переменных, используя так называемую «безименную» индексную нотацию Де Брейна .
История [ править ]
Явные замены были описаны в предисловии к книге Карри по комбинаторной логике. [2] и выросла из «трюка реализации», использованного, например, AUTOMATH , и стала респектабельной синтаксической теорией в лямбда-исчислении и теории переписывания . Хотя на самом деле оно исходило от де Брейна , [3] Идея специфического исчисления, в котором замены являются частью объектного языка, а не неформальной метатеории, традиционно приписывают Абади , Карделли , Кюрьену и Леви. Их основополагающий документ [4] по исчислению λσ объясняет, что реализации лямбда-исчисления должны быть очень осторожны при работе с заменами. Без сложных механизмов совместного структурирования замены могут вызвать взрывной рост размеров, и поэтому на практике замены задерживаются и явно фиксируются. Это делает соответствие между теорией и реализацией весьма нетривиальным, и корректность реализаций может быть трудно установить. Одно из решений — сделать замены частью исчисления, то есть иметь исчисление явных замен.
Однако как только замена становится явной, ее основные свойства из семантических переходят в синтаксические. Одним из наиболее важных примеров является «лемма о замене», которая с обозначением λx становится
- (M⟨x:=N⟩)⟨y:=P⟩ = (M⟨y:=P⟩)⟨x:=(N⟨y:=P⟩)⟩ (где x≠y и x не свободны в P )
Удивительный контрпример, предложенный Мельесом: [5] показывает, что способ, которым это правило закодировано в исходном исчислении явных подстановок, не является строго нормализующим . После этого было описано множество исчислений, пытающихся предложить наилучший компромисс между синтаксическими свойствами исчислений явной замены. [6] [7] [8]
См. также [ править ]
Ссылки [ править ]
- ^ Клаустон, Ранальд; Бизяк, Алеш; Гратволь, Ганс; Биркедал, Ларс (27 апреля 2017 г.). «Защищенное лямбда-исчисление: программирование и рассуждения с защищенной рекурсией для коиндуктивных типов». Логические методы в информатике . 12 (3): 36. arXiv : 1606.09455 . дои : 10.2168/LMCS-12(3:7)2016 .
- ^ Карри, Хаскелл; Фейс, Роберт (1958). Комбинаторная логика, том I. Амстердам: Издательство Северной Голландии.
- ^ NG de Bruijn: лямбда-исчисление без имен с возможностью внутреннего определения выражений и сегментов. Технологический университет Эйндховена, Нидерланды, математический факультет, (1978), (TH-Report), номер 78-WSK-03.
- ^ М. Абади, Л. Карделли, PL. Курьен и Джей-Джей. Леви, Явные замены, Журнал функционального программирования 1, 4 (октябрь 1991 г.), 375–416.
- ^ ПА. Мельес: Типизированные лямбда-исчисления с явными заменами не могут завершиться. ТЛКА 1995: 328–334.
- ^ П. Лесканн, От λσ к λυ: путешествие по исчислениям явных замен, POPL 1994, стр. 60–69.
- ^ К. Х. Роуз, Явная замена – Учебное пособие и обзор, BRICS LS-96-3, сентябрь 1996 г. ( ps.gz ).
- ^ Делия Кеснер: Теория явных замен с безопасным и полным составом. Логические методы в информатике 5 (3) (2009)