В информатике говорят , что лямбда-исчисления имеют явные подстановки , если они уделяют особое внимание формализации процесса подстановки . Это контрастирует со стандартным лямбда-исчислением , где подстановки выполняются бета-редукциями неявным образом, который не выражается в исчислении; условия «свежести» в таких неявных исчислениях являются печально известным источником ошибок. [1] Эта концепция появилась в большом количестве опубликованных статей в совершенно разных областях, таких как абстрактные машины , предикатная логика и символьные вычисления .
Простым примером лямбда-исчисления с явной подстановкой является «λx», которое добавляет одну новую форму термина в лямбда-исчисление , а именно форму M⟨x:=N⟩, которая читается как «M, где x будет заменен на N». (Значение нового термина такое же, как и распространенная идиома let x:=N в M из многих языков программирования.) λx можно записать с помощью следующих правил переписывания :
Хотя эта формулировка делает подстановку явной, она все еще сохраняет сложность "переменной конвенции" лямбда-исчисления , требуя произвольного переименования переменных во время редукции, чтобы гарантировать, что условие "(x≠y и x не свободны в N)" в последнем правиле всегда выполняется до применения правила. Поэтому многие исчисления явной подстановки вообще избегают имен переменных, используя так называемую "свободную от имени" индексную нотацию Де Брейна .
Явные подстановки были набросаны в предисловии к книге Карри по комбинаторной логике [2] и выросли из «трюка реализации», используемого, например, AUTOMATH , и стали уважаемой синтаксической теорией в лямбда-исчислении и теории переписывания . Хотя на самом деле она возникла у де Брейна [3], идея конкретного исчисления, где подстановки являются частью объектного языка, а не неформальной метатеории, традиционно приписывается Абади , Карделли , Курьену и Леви. Их основополагающая статья [4] по исчислению λσ объясняет, что реализации лямбда-исчисления должны быть очень осторожны при работе с подстановками. Без сложных механизмов для совместного использования структур подстановки могут вызвать взрывной рост размера, и поэтому на практике подстановки задерживаются и явно записываются. Это делает соответствие между теорией и реализацией крайне нетривиальным, а правильность реализаций может быть трудно установить. Одним из решений является включение подстановок в исчисление, то есть создание исчисления явных подстановок.
Однако, как только замена сделана явной, основные свойства замены меняются с семантических на синтаксические. Одним из наиболее важных примеров является «лемма замены», которая с обозначением λx становится
Удивительный контрпример, предложенный Мельесом [5], показывает, что способ, которым это правило закодировано в исходном исчислении явных подстановок, не является строго нормализующим . После этого было описано множество исчислений, пытающихся предложить наилучший компромисс между синтаксическими свойствами исчислений явных подстановок. [6] [7] [8]