Ну хорошо, чинная рекурсивная фигня. Мне просто влом её сочинять, особенно, не видя реализации reduce и не зная её уязвимого места.
Кстати, отсюда мораль: вместо детерминированной редукции, которая может пойти по дороге в ад, надо недетерминированную: строить дерево всех одношаговых редукций и останавливаться на любом нередуцируемом терме (поиск вширь, а не вглубь). Ну или для приличия сделать ещё несколько попыток для нахождения второго нередуцируемого терма...
монадическая
reduce :: Term -> [Term]
и пусть она возвращает только редукции, а не оригинал.
Т.е. вместо if canReduce t then doReduce t
там будет t'<-allReduces t
Возможно, прямо в недрах делать отсеивание опасностей...