В λ-численні, підстановка визначається структурною індукцією. Для деяких об'єктів , та деякої змінної результат зміни деякого вільного входження в вважається підстановкою та визначається індукцією по створенню :
базис:: об'єкт є самий як змінна . Тоді ;
базис:: об'єкт є самий як константа . Тоді для деяких атомарних ;
крок:: об'єкт неатомарний і має вигляд аплікації . Тоді ;
крок:: об'єкт неатомарний та є -абстракцією . Тоді [;
крок:: об'єкт неатомарний та є -абстракцією , причому . Тоді: