Підстановка

В λ-численні, підстановка визначається структурною індукцією. Для деяких об'єктів ${\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. -- В серії "Компьютерные науки и информационные технологии" .