## StepULC

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 `fac 4`

. `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.