Подстановка

В математике и информатике подстановка — это операция синтаксической замены подтермов данного терма другими термами, согласно определённым правилам. Обычно речь идёт о подстановке терма вместо переменной.

Определения и обозначения

Для подстановки не существует универсальной, согласованной нотации, равно как и стандартного определения. Понятие подстановки варьируется не только в рамках разделов, но и на уровне отдельных публикаций. В целом, можно выделить контекстную подстановку и подстановку «вместо». В первом случае место в терме, где происходит замена, задаётся контекстом, то есть частью терма, «окружающего» это место. В частности, такое понятие подстановки используется в переписывании. Второй вариант более распространён. В этом случае подстановка обычно задаётся некоторой функцией [math]\displaystyle{ \sigma:X\to T }[/math] из множества переменных в множество термов. Для обозначения действия подстановки, как правило, используют постфиксную нотацию. Например, [math]\displaystyle{ t\sigma }[/math] означает результат действия подстановки [math]\displaystyle{ \sigma }[/math] на терм [math]\displaystyle{ t }[/math].

В подавляющем большинстве случаев требуется, чтобы подстановка имела конечный носитель, то есть чтобы множество [math]\displaystyle{ \{x\mid x\neq\sigma x\} }[/math] было конечным. В таком случае её можно задать простым перечислением пар «переменная-значение». Поскольку каждую такую подстановку можно свести к последовательности подстановок, замещающих всего по одной переменной каждая, не ограничивая общности, можно считать, что подстановка задаётся одной парой «переменная-значение», что обычно и делается.

Последнее определение подстановки является, видимо, самым типичным и часто используемым. Однако и для него не существует единой общепринятой нотации. Наиболее часто для обозначения подстановки a вместо x в t используется запись t[a/x], t[x:=a] или t[x←a].

Подстановка переменной в λ-исчислении

В λ-исчислении подстановка определяется структурной индукцией. Для произвольных объектов [math]\displaystyle{ P }[/math], [math]\displaystyle{ Q }[/math] и произвольной переменной [math]\displaystyle{ x }[/math] результат замещения произвольного свободного вхождения [math]\displaystyle{ x }[/math] в [math]\displaystyle{ Q }[/math] считается подстановкой и определяется индукцией по построению [math]\displaystyle{ Q }[/math]:

(i) базис: [math]\displaystyle{ Q \equiv x }[/math]: объект [math]\displaystyle{ Q }[/math] совпадает с переменной [math]\displaystyle{ x }[/math]. Тогда [math]\displaystyle{ [P/x]x \equiv P }[/math];

(ii) базис: [math]\displaystyle{ Q \equiv c }[/math]: объект [math]\displaystyle{ Q }[/math] совпадает с константой [math]\displaystyle{ c }[/math]. Тогда [math]\displaystyle{ [P/x]c \equiv c }[/math] для произвольных атомарных [math]\displaystyle{ c \not\equiv x }[/math];

(iii) шаг: [math]\displaystyle{ Q \equiv (Q_1\,Q_2) }[/math]: объект [math]\displaystyle{ Q }[/math] неатомарный и имеет вид аппликации [math]\displaystyle{ (Q_1\,Q_2) }[/math]. Тогда [math]\displaystyle{ [P/x](Q_1\, Q_2) \equiv ([P/x]Q_1)([P/x]Q_2) }[/math];

(iv) шаг: [math]\displaystyle{ Q \equiv \lambda x.M }[/math]: объект [math]\displaystyle{ Q }[/math] неатомарный и является [math]\displaystyle{ x }[/math]-абстракцией [math]\displaystyle{ \lambda x.M }[/math]. Тогда [[math]\displaystyle{ P/x](\lambda x.M) \equiv \lambda x.M }[/math];

(v) шаг: [math]\displaystyle{ Q \equiv \lambda y.M }[/math]: объект [math]\displaystyle{ Q }[/math] неатомарный и является [math]\displaystyle{ y }[/math]-абстракцией [math]\displaystyle{ \lambda y.M }[/math], причем [math]\displaystyle{ y \not\equiv x }[/math]. Тогда:

[math]\displaystyle{ [P/x](\lambda y.M) \equiv (\lambda y.[P/x]M) }[/math] для [math]\displaystyle{ y \not\equiv x }[/math] и [math]\displaystyle{ y \notin P }[/math] или [math]\displaystyle{ x \notin M }[/math];

[math]\displaystyle{ (\lambda z.[P/x][z/y]M) }[/math] для [math]\displaystyle{ y \not\equiv x }[/math] и [math]\displaystyle{ y \in P }[/math] и [math]\displaystyle{ x \in M }[/math].

См. также

Ссылки