Підстановка — довільна функція з однієї скінченної множини в іншу: . Часто , якщо ж при цьому бієкція, то називають перестановкою.

Підстановка змінної в лямбда-численніРедагувати

Докладніше: лямбда-числення

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

  1. базис:  : об'єкт   є самий як змінна  . Тоді  ;
  2. базис:  : об'єкт   є самий як константа  . Тоді   для деяких атомарних  ;
  3. крок:  : об'єкт   неатомарний і має вигляд аплікації  . Тоді  ;
  4. крок:  : об'єкт   неатомарний та є  -абстракцією  . Тоді [ ;
  5. крок:  : об'єкт   неатомарний та є  -абстракцією  , причому  . Тоді:
      для   та   або  ;
      для   та   та  .

Див. такожРедагувати

ЛітератураРедагувати