Seonglae ChoThe Computational and Experimental World of Lambda Calculus
Analyzing the complex behavioral patterns of lambda through empirical computational experiments rather than traditional mathematical formalism
When the simple process of β reduction is repeated, very complex and unpredictable behavior emerges.
By enumerating small lambda expressions and analyzing their evolution patterns, some terminate immediately while others exhibit diverse dynamics such as infinite growth or periodic (looping) repetition. The halting problem is generally undecidable, and the non-halting of certain lambdas may be unprovable within Peano arithmetic (related to Gödel and Goodstein sequences).
The evaluation process of lambda expressions was visualized using multiway graphs and causal graphs, exploring differences according to various evaluation strategies (left-outermost priority, depth-first, etc.).
Linear lambdas (where each variable appears only once) always terminate finitely and have a simple diamond-shaped graph structure. Lambda calculus and combinators (S, K) are computationally equivalent, following the same Principle of Computational Equivalence in terms of complexity, non-determinism, pattern diversity, and more.
To predict the result, there is no choice but to directly execute it" → Computational Irreducibility, viewing lambda calculus as a universe of computational complexity emerging from simple rules, connecting it to the fundamental Irreducibility of nature, mathematics, and logic
