Підстановка

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

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

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

1. базис: $Q\equiv x$: об'єкт $Q$ є самий як змінна $x$. Тоді $[P/x]x\equiv P$;
2. базис: $Q\equiv c$: об'єкт $Q$ є самий як константа $c$. Тоді $[P/x]c\equiv c$ для деяких атомарних $c\equiv ̸x$;
3. крок: $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)$;
4. крок: $Q\equiv \lambda x.M$: об'єкт $Q$ неатомарний та є $x$-абстракцією $\lambda x.M$. Тоді [$P/x](\lambda x.M)\equiv \lambda x.M$;
5. крок: $Q\equiv \lambda y.M$: об'єкт $Q$ неатомарний та є $y$-абстракцією $\lambda y.M$, причому $y\equiv ̸x$. Тоді:

   $[P/x](\lambda y.M)\equiv (\lambda y.[P/x]M)$ для $y\equiv ̸x$ та $y\notin P$ або $x\notin M$;

   $(\lambda z.[P/x][z/y]M)$ для $y\equiv ̸x$ та $y\in P$ та $x\in M$.

Див. також

• Асоціативне числення
• Лямбда-числення

Література

• Вольфенгаген В.Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. -- М.: JurInfoR Ltd., АО “Центр ЮрИнфоР”, 2004. -- xvi+789 с. ISBN 5-89158-100-0. -- В серії Шаблон:Webarchive "Компьютерные науки и информационные технологии" .

Шаблон:Math-stub Шаблон:Compu-stub Шаблон:Refimprove