Подстановка

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск
Это статья о подстановке как о синтаксической операции над термами. Возможно, вас интересует перестановка.

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

Определения и обозначения[править | править вики-текст]

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

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

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

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

В λ-исчислении, подстановка определяется структурной индукцией. Для произвольных объектов 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.

См. также[править | править вики-текст]

Ссылки[править | править вики-текст]