Подстановка (Hk;vmgukftg)

Эта статья — о подстановке как о синтаксической операции над термами. О подстановках в комбинаторике см. перестановка.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

См. также

• Аппликативное программирование
• λ-исчисление
• λ-исчисление с типами
• Стратегия вычисления