Підстановка — довільна функція з однієї скінченної множини в іншу: . Часто , якщо ж при цьому — бієкція, то називають перестановкою.
Підстановка змінної в лямбда-численні
В λ-численні, підстановка визначається структурною індукцією. Для деяких об'єктів , та деякої змінної результат зміни деякого вільного входження в вважається підстановкою та визначається індукцією по створенню : базис: : об'єкт є самий як змінна . Тоді ; базис: : об'єкт є самий як константа . Тоді для деяких атомарних ; крок: : об'єкт неатомарний і має вигляд аплікації . Тоді ; крок: : об'єкт неатомарний та є -абстракцією . Тоді [; крок: : об'єкт неатомарний та є -абстракцією , причому . Тоді: для та або ; для та та .
Див. також Асоціативне числення Лямбда-числення
Література
Вольфенгаген В.Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. -- М.: JurInfoR Ltd., АО “Центр ЮрИнфоР”, 2004. -- xvi+789 с. ISBN 5-89158-100-0. -- В серії "Компьютерные науки и информационные технологии" .