Підстановка

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

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

В λ-численні, підстановка визначається структурною індукцією. Для деяких об'єктів $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\not \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\not \equiv x$. Тоді:

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

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

Див. також

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

Література

• Вольфенгаген В.Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. -- М.: JurInfoR Ltd., АО “Центр ЮрИнфоР”, 2004. -- xvi+789 с. ISBN 5-89158-100-0. -- В серії [[https://web.archive.org/web/20090117063950/http://jurinfor.ru/library/ser.php?SERID=CS Архівовано 17 січня 2009 у Wayback Machine.] "Компьютерные науки и информационные технологии" ].