Поиск

Инструменты

На других языках

English

Подстановка

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

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

Содержание

1 Определения и обозначения
2 Подстановка переменной в λ-исчислении
3 Подстановка переменной в программировании
4 См. также
5 Ссылки

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

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

-абстракцией

λ x . M

. Тогда [ $P/x](\lambda x.M) \equiv \lambda x.M$ ;

(v) шаг: $Q \equiv \lambda y.M$ : объект

Q

неатомарный и является

y

-абстракцией

λ 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$ ;

(λ z .[P / x][z / y] M)

для $y \not\equiv x$ и $y \in P$ и $x \in M$ .

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

Подстановка переменной (англ. substitution) в аппликативном программировании понимается следующим образом. Для вычисления значения функции f на аргументе v применяется запись f(v)}, где f определена конструкцией f(x) = e. Запись f(v) в этом случае означает, что в выражении e происходит замещение, или подстановка переменной x на v. Выполнение замещения происходит в соответствии с семантикой вычислений.
Подстановка переменной (англ. assignment) в программировании понимается как присваивание. Оператор присваивания является проявлением эффекта «горла бутылки» фон Нейманна для традиционных языков программирования^[1]. От этого свободны аппликативные вычислительные системы.