Lambda Calculus – Animated Beta Reduction of Lambda Diagrams
Лямбда-исчисление — фундаментальная модель вычислений, где всё сводится к анонимным функциям: абстракциям (λx.M), приложениям (M N) и переменным. Система Тьюринга-полна, способна симулировать любую машину Тьюринга без циклов или переменных состояния, полагаясь только на подстановку (β-редукцию).
Статья предлагает интерактивный интерпретатор и визуализатор: вводите выражения вроде λx.x (идентичность), λx.λy.x (константа), λf.λx.f (f x) (применение дважды). Примеры: Y-комбинатор для рекурсии (λf.(λx.f (x x)) (λx.f (x x))), числа Чёрча (0=λf.λx.x, 1=λf.λx.f x, succ=λn.λf.λx.f (n f x)). Графики редукций показывают шаги нормализации, подчёркивая church-россы (λx y.f x = λy.f) и η-равенство. Полезно для понимания функционального программирования и доказательств.