Явная подстановка
-
Явные подстановки в лямбда-исчислении
- Явные подстановки акцентируют внимание на формализации процесса подстановки в лямбда-исчислении.
- Стандартное лямбда-исчисление использует неявные замены, что может привести к ошибкам из-за «свежести» условий.
- Явные подстановки были описаны в различных областях, включая абстрактные машины и логику предикатов.
-
Пример явной подстановки
- «λx» добавляет в лямбда-исчисление форму M⟨x:=N⟩, где x заменяется на N.
- Правила перезаписи для явной подстановки включают переписывание с использованием «трюка с реализацией» и безымянной индексной нотации Де Брейна.
-
История и развитие
- Явные замены были описаны в книге Карри по комбинаторной логике и стали частью лямбда-исчисления и теории перезаписи.
- Идея явных подстановок возникла у де Брюйна, но обычно приписывается Абади, Карделли, Кюриену и Леви.
- В статье, посвященной λσ-исчислению, подчеркивается важность осторожности при работе с заменами для избежания увеличения размера вычислений.
-
Проблемы и решения
- Явные подстановки могут привести к увеличению размера вычислений и задержкам в реализации.
- Лемма о подстановке изменяется с семантических на синтаксические свойства при явном представлении.
- Меллиес показал, что исходное исчисление явных подстановок не является строго нормализующим.
- Были предложены различные вычисления для улучшения компромисса между синтаксическими свойствами и точностью явных подстановок.
Полный текст статьи: