Some time ago, I found an impure solution to the problem of matching fans in Lamping's abstract algorithm. It is described in [1] and implemented in [2], the essential part of source code being available in [3].

My understanding is that the algorithm effectively eliminates the need in bookkeeping nodes (so-called "oracle") for optimal reduction in case of arbitrary untyped λ-terms. Although I have no formal proof for its correctness yet, the amount of testing [4, 5] that have already been done leaves little room for counterexamples.

Questions remaining open are: how to (dis)prove correctness of the algorithm as well as how to simplify and improve the algorithm? Any help would be highly appreciated.

[1] https://arxiv.org/abs/1710.07516

[2] https://codedot.github.io/lambda/

[3] https://github.com/codedot/lambda/blob/master/encoding/abstract/template.txt

[4] https://gist.github.com/codedot/721469173df8dd197ba5bddbe022c487

[5] https://www.npmjs.com/package/@alexo/lambda (the "Benchmarks" section)

## Recent comments

23 hours 43 min ago

6 days 6 hours ago

1 week 1 day ago

2 weeks 5 days ago

3 weeks 4 days ago

4 weeks 4 days ago

6 weeks 2 days ago

6 weeks 5 days ago

7 weeks 6 days ago

8 weeks 2 days ago