Подстановка

Материал из Seo Wiki - Поисковая Оптимизация и Программирование

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

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

Содержание

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

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

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

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

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

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

(i) базис: <math>Q \equiv x</math>: объект <math>Q</math> совпадает с переменной <math>x</math>. Тогда <math>[P/x]x \equiv P</math>;
(ii) базис: <math> Q \equiv c</math>: объект <math>Q</math> совпадает с константой <math>c</math>. Тогда <math>[P/x]c \equiv c</math> для произвольных атомарных <math>c \not\equiv x</math>;
(iii) шаг: <math>Q \equiv (Q_1\,Q_2)</math>: объект <math>Q</math> неатомарный и имеет вид аппликации <math>(Q_1\,Q_2)</math>. Тогда <math>[P/x](Q_1\, Q_2) \equiv ([P/x]Q_1)([P/x]Q_2)</math>;
(iv) шаг: <math>Q \equiv \lambda x.M</math>: объект <math>Q</math> неатомарный и является <math>x</math>-абстракцией <math>\lambda x.M</math>. Тогда [<math>P/x](\lambda x.M) \equiv \lambda x.M</math>;
(v) шаг: <math>Q \equiv \lambda y.M</math>: объект <math>Q</math> неатомарный и является <math>y</math>-абстракцией <math>\lambda y.M</math>, причем <math>y \not\equiv x</math>. Тогда:
<math> [P/x](\lambda y.M) \equiv (\lambda y.[P/x]M)</math> для <math>y \not\equiv x</math> и <math>y \notin P</math> или <math>x \notin M</math>;
<math>(\lambda z.[P/x][z/y]M)</math> для <math>y \not\equiv x</math> и <math>y \in P</math> и <math>x \in M</math>.

Подстановка переменной в программировании

См. также

Ссылки

Личные инструменты

Served in 0.120 secs.