Войти
В информатике, лямбда-исчисления считаются имеющими явную замену, если они уделяют особое внимание формализации процесса подстановки. Это контрастирует со стандартным лямбда-исчислением, где подстановки выполняются с помощью бета-редукции неявным образом, который не выражается в исчислении. Концепция явных подстановок стала печально известной (несмотря на большое количество опубликованных в литературе исчислений явных подстановок с совершенно разными характеристиками), потому что это понятие часто встречается (неявно и явно) в формальных описаниях и реализации всех математических форм подстановка с участием переменных, например, в абстрактных машинах, логике предикатов и символьных вычислениях.
Простым примером лямбда-исчисления с явной заменой является «λx», который добавляет одну новую форму термина к лямбда-исчисление, а именно форма M⟨x: = N⟩, которая читается как «M, где x будет заменен на N». (Значение нового термина такое же, как и обычная идиома let x: = N в M из многих языков программирования.) Λx может быть записано с помощью следующей перезаписи правила:
Делая замену явной, эта формулировка по-прежнему сохраняет сложность лямбда-исчисления "соглашение о переменных", требуя произвольного переименования переменных во время сокращения, чтобы гарантировать, что условие "(x ≠ y and x not free in N)" в последнем правиле всегда доволен перед применением правила. Поэтому многие исчисления явной подстановки вообще избегают имен переменных, используя так называемую "безымянную" нотацию индекса Де Брейна.
Явные замены были набросаны в предисловии к книге Карри по комбинаторной логике и выросли из «уловки реализации», используемой, например, AUTOMATH, и стала респектабельной синтаксической теорией в лямбда-исчислении и теории переписывания. Хотя на самом деле она возникла у де Брюйна, идея особого исчисления, в котором подстановки являются частью объектного языка, а не неформальной метатеории, традиционно приписывается Абади, Карделли, Куриен и Леви. В их основополагающей статье об исчислении λσ объясняется, что реализации лямбда-исчисления должны быть очень осторожны при работе с подстановками. Без сложных механизмов для разделения структуры замены могут вызвать взрывной рост размера, и поэтому на практике замены задерживаются и явно записываются. Это делает соответствие между теорией и реализацией весьма нетривиальным, а правильность реализаций может быть трудно установить. Одно из решений - сделать замены частью исчисления, то есть иметь исчисление явных подстановок.
Однако, как только подстановка сделана явной, основные свойства подстановки меняются с семантических на синтаксические. Одним из наиболее важных примеров является «лемма о подстановке», которая с обозначением λx становится
Удивительный контрпример, сделанный Меллиесом, показывает, что способ кодирования этого правила в исходном исчислении явных подстановок не соответствует действительности. сильно нормализующий. После этого было описано множество исчислений, пытающихся предложить лучший компромисс между синтаксическими свойствами явных исчислений подстановки.
