User loginNavigation |
An impure solution to the problem of matching fansSome 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 By Anton Salikhmetov at 2018-01-01 17:08 | LtU Forum | previous forum topic | next forum topic | other blogs | 6157 reads
|
Browse archivesActive forum topics |
Recent comments
8 weeks 2 days ago
8 weeks 4 days ago
8 weeks 5 days ago
15 weeks 5 days ago
21 weeks 3 days ago
21 weeks 4 days ago
22 weeks 3 days ago
25 weeks 1 day ago
26 weeks 4 days ago
26 weeks 5 days ago