Перейти до вмісту

Підстановка

Матеріал з Вікіпедії — вільної енциклопедії.

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

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

[ред. | ред. код]
Докладніше: лямбда-числення

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

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

Див. також

[ред. | ред. код]

Література

[ред. | ред. код]