Efficient and single-steppable ULC (untyped lambda calculus) evaluation algorithm
The algorithm mainly comes from the following PEPM '17 paper:
Berezun, Daniil & Jones, Neil. (2017). Compiling untyped lambda calculus to lower-level code by game semantics and partial evaluation (invited paper). 1-11. 10.1145/3018882.3020004.
Specifically, Semantics 1 through 3 from Chapter 3 of the paper are implemented with certain modifications, in Haskell.
The main objectives of this development are:
- Directly work with de Bruijn indexes from the start.
- Avoid cloning and modifying substructures of a ULC expression (semi-compositionality).
- Allow single-stepping at the algorithm level (tail recursion).
- Evaluate the normal form, if it exists.
- Avoid any tricks related to lazy evaluation, so it can be easily ported to other languages (especially imperative ones).
It was highly non-trivial to modify the presented algorithms to the ones that actually evaluate the normal form, but I finally did it by following the incremental transformations as presented in the paper. And the last one,
semantic3, avoids all lazy shenanigans like infinite lists and composed functions inside a data structure, so that it can be ported to more imperative languages.
Regarding performance, a (somewhat suboptimal) factorial function was used (
fix is the fixpoint combinator, and other named functions are known ones for Church numerals):
fac = fix facFix where facFix = \f n. (iszero n) (\f x. f x) (mult n (f (pred n)))
Naive repeated beta reduction takes multiple hundred milliseconds to evaluate
semantic2 avoids cloning substructures, and takes under 10 milliseconds for the same input. (Exact timings vary wildly, but I observed around x50 ~ x100 speedup.) Further modifications do not improve in terms of execution time in Haskell (
semantic3 is 2~4 times slower than
semantic2), but they are essential in recovering the "single-steppability" and portability.