Эта статья — о подстановке как о синтаксической операции над термами. О подстановках в комбинаторике см.
перестановка.
В математике и информатике подстановка — это операция синтаксической замены подтермов данного терма другими термами, согласно определённым правилам. Обычно речь идёт о подстановке терма вместо переменной.
Определения и обозначения
Для подстановки не существует универсальной, согласованной нотации, равно как и стандартного определения. Понятие подстановки варьируется не только в рамках разделов, но и на уровне отдельных публикаций. В целом, можно выделить контекстную подстановку и подстановку «вместо». В первом случае место в терме, где происходит замена, задаётся контекстом, то есть частью терма, «окружающего» это место. В частности, такое понятие подстановки используется в переписывании. Второй вариант более распространён. В этом случае подстановка обычно задаётся некоторой функцией
из множества переменных в множество термов. Для обозначения действия подстановки, как правило, используют постфиксную нотацию. Например,
означает результат действия подстановки
на терм
.
В подавляющем большинстве случаев требуется, чтобы подстановка имела конечный носитель, то есть чтобы множество
было конечным. В таком случае её можно задать простым перечислением пар «переменная-значение». Поскольку каждую такую подстановку можно свести к последовательности подстановок, замещающих всего по одной переменной каждая, не ограничивая общности, можно считать, что подстановка задаётся одной парой «переменная-значение», что обычно и делается.
Последнее определение подстановки является, видимо, самым типичным и часто используемым. Однако и для него не существует единой общепринятой нотации. Наиболее часто для обозначения подстановки a вместо x в t используется запись t[a/x], t[x:=a] или t[x←a].
В λ-исчислении подстановка определяется структурной индукцией. Для произвольных объектов
,
и произвольной переменной
результат замещения произвольного свободного вхождения
в
считается подстановкой и определяется индукцией по построению
:
- (i) базис:
: объект
совпадает с переменной
. Тогда
;
- (ii) базис:
: объект
совпадает с константой
. Тогда
для произвольных атомарных
;
- (iii) шаг:
: объект
неатомарный и имеет вид аппликации
. Тогда
;
- (iv) шаг:
: объект
неатомарный и является
-абстракцией
. Тогда [
;
- (v) шаг:
: объект
неатомарный и является
-абстракцией
, причем
. Тогда:
для
и
или
;
для
и
и
.
См. также
Ссылки
![Перейти к шаблону «Логика»](//upload.wikimedia.org/wikipedia/commons/thumb/c/c9/Wikipedia_interwiki_section_gear_icon.svg/14px-Wikipedia_interwiki_section_gear_icon.svg.png) |
---|
|
Группы логик | | |
---|
Компоненты | |
---|
|