А, понял твою шутку. Просто функция reduceToNF названа неправильно. Из неподвижной точки r == reduce r не следует, что это нормальная форма (импликация там в обратную сторону, из нормальности следует неподвижность).
Отсюда, таки, мораль! reduce должна возвращать монаду - Maybe или [], по вкусу. Смысл которой - "мне удалось что-то внутри редуцировать".
Тогда и reduceToNF будет простой донельзя: unfoldr reduceMaybe. И проверка альфа-эквивалентности не нужна.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2013-03-28 03:22 pm (UTC)Просто функция reduceToNF названа неправильно.
Из неподвижной точки r == reduce r не следует, что это нормальная форма (импликация там в обратную сторону, из нормальности следует неподвижность).
Отсюда, таки, мораль! reduce должна возвращать монаду - Maybe или [], по вкусу. Смысл которой - "мне удалось что-то внутри редуцировать".
Тогда и reduceToNF будет простой донельзя: unfoldr reduceMaybe.
И проверка альфа-эквивалентности не нужна.