Подстановка

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

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

Определения и обозначенияПравить

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

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

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

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

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

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

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

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

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

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

$[P/x](\mathrm{\lambda <!--\; \lambda \; -->}y.M)\equiv <!--\; \equiv \; -->(\mathrm{\lambda <!--\; \lambda \; -->}y.[P/x]M)$$[P/x](\lambda y.M)\equiv (\lambda y.[P/x]M)$  для $y\not\equiv x$$y\not \equiv x$  и $y\notin <!--\; \notin \; -->P$$y\notin P$  или $x\notin <!--\; \notin \; -->M$$x\notin M$ ;

$(\mathrm{\lambda <!--\; \lambda \; -->}z.[P/x][z/y]M)$$(\lambda z.[P/x][z/y]M)$  для $y\not\equiv x$$y\not \equiv x$  и $y\in <!--\; \in \; -->P$$y\in P$  и $x\in <!--\; \in \; -->M$$x \in M$ .

См. такжеПравить

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