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 (socalled "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 20180101 17:08  LtU Forum  previous forum topic  next forum topic  other blogs  3790 reads

Browse archivesActive forum topicsNew forum topics 
Recent comments
16 hours 39 min ago
2 days 17 hours ago
3 days 16 hours ago
4 days 10 hours ago
4 days 19 hours ago
6 days 15 hours ago
6 days 21 hours ago
1 week 8 hours ago
1 week 8 hours ago
1 week 3 days ago