Підстановка

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

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

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

1. базис: ${\displaystyle \ Q\equiv x}$: об'єкт ${\displaystyle Q}$ є самий як змінна ${\displaystyle x}$. Тоді ${\displaystyle [P/x]x\equiv P}$;
2. базис: ${\displaystyle \ Q\equiv c}$: об'єкт ${\displaystyle Q}$ є самий як константа ${\displaystyle c}$. Тоді ${\displaystyle [P/x]c\equiv c}$ для деяких атомарних ${\displaystyle c\not \equiv x}$;
3. крок: ${\displaystyle Q\equiv (Q_{1}\,Q_{2})}$: об'єкт ${\displaystyle Q}$ неатомарний і має вигляд аплікації ${\displaystyle (Q_{1}\,Q_{2})}$. Тоді ${\displaystyle [P/x](Q_{1}\,Q_{2})\equiv ([P/x]Q_{1})([P/x]Q_{2})}$;
4. крок: ${\displaystyle \ Q\equiv \lambda x.M}$: об'єкт ${\displaystyle Q}$ неатомарний та є ${\displaystyle x}$-абстракцією ${\displaystyle \lambda x.M}$. Тоді [${\displaystyle P/x](\lambda x.M)\equiv \lambda x.M}$;
5. крок: ${\displaystyle \ Q\equiv \lambda y.M}$: об'єкт ${\displaystyle Q}$ неатомарний та є ${\displaystyle y}$-абстракцією ${\displaystyle \lambda y.M}$, причому ${\displaystyle y\not \equiv x}$. Тоді:

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

   ${\displaystyle (\lambda z.[P/x][z/y]M)}$ для ${\displaystyle y\not \equiv x}$ та ${\displaystyle y\in P}$ та ${\displaystyle 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.] "Компьютерные науки и информационные технологии" ].