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

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

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

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

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

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

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

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

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

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

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

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

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

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

См. также

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

Ссылки