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

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

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

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

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

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

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

(i) базис:  : объект   совпадает с переменной  . Тогда  ;
(ii) базис:  : объект   совпадает с константой  . Тогда   для произвольных атомарных  ;
(iii) шаг:  : объект   неатомарный и имеет вид аппликации  . Тогда  ;
(iv) шаг:  : объект   неатомарный и является  -абстракцией  . Тогда [ ;
(v) шаг:  : объект   неатомарный и является  -абстракцией  , причем  . Тогда:
  для   и   или  ;
  для   и   и  .

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

Ссылки править