Перепост с dxdy.ru (интересно мнение здешней публики).
Поскольку λ-исчисление минимально по форме, то, по логике, на его примере должна быть наиболее хорошо видна суть того или иного базового понятия из computer science. Вот, пока что удалось разглядеть:
1) значение < — > всякий λ-терм в нормальной форме (относительно βη-редукции), например, λf.λx.x := 0, λf.λx.f x := 1 2) выражение <-> всякий λ-терм 3) вычисление выражения <-> алгоритмически заданный процесс преобразования исходного выражения к значению; 4) аппликативная/нормальная стратегия вычисления <-> вычисления с аппликативным/нормальным порядком редукции; 5) программа/исходные данные программы <-> λ-терм/значение к которому он будет применяться 6) декларирование (связывание идентификатора x с некоторым объектом) <-> констатация по терму вида (λx.P)V того факта, что в терме P при β-редукции вхождения связанной переменной x будут замещаться связанным с ней термом (объектом) V.
Пример. Конструкцию (λa.(λx.ax))1 можно, например, воспринимать как аналог let a = 1 in λx.ax.
7) передача аргумента по значению <-> бета редукция с предварительной редукцией "аргумента" (то, к чему применяется абстракция) к нормальной форме; 8) передача аргумента по имени <-> бета редукция без предварительной редукции аргумента к нормальной форме; 9) статическое (лексическое) связывание <-> требование "неприкосновенности деклараций" при β-редукции, что выражается в требовании особым обрзом осуществлять подстановку, разводя путем α-редукции пересекающиеся имена переменных, если это может привести к изменению их декларативной связи с объектом.
Пример. С точки зрения λ-исчисления корректна такая последовательность редукций
