Re:Show HN: Eole, a Lévy-optimal lambda calculus evaluator w...
by danharaj on Monday October 21, 2019 @08:43AM
(#21311588)
Did you demonstrate that your trick is sound and optimal? Optimal reduction is a tricky beast and you might need to use a very high order function to find a counterexample.
[ Parent
| on HN ]
Re:Show HN: Eole, a Lévy-optimal lambda calculus evaluator w...
by HerrmannM on Monday October 21, 2019 @07:19PM
(#21318665)
A tricky beast indeed!
No, the formal proof is a work in progress, so I'm also looking for counter-examples. And since posting on hackernews, someone found some problems (thank you so much Ekdohibs). However, there is for sure an implementation issue so they do not count as counter-examples yet. I'll investigate and fix that asap, then we'll see...