Трудности с простыми лямбда-калькуляторами

А вот, кстати, при проверке лямбда-калькуляторов, написанных студентами, возникла такая задачка.

Пускай мы реализовали на Хаскелле лямбда-термы

data Term = 
    Var String
  | App Term Term
  | Lam String Term        

проверку их альфа-эквивалентности (можно и точное совпадение, для наших целей не важно):

alphaEq :: Term -> Term -> Bool

и одношаговую бета-редукцию (нормальную, для определенности, хотя это тоже не важно):

reduce :: Term -> Term

В последнем случае при отсутствии редексов просто возвращается исходный терм.

Если мы теперь хотим реализовать многошаговую бета-редукцию до нормальной формы, мы можем итерировать, делая шаг редукции до тех пор, пока терм не перестанет меняться. Ну, например, так

reduceToNF :: Term -> [Term]
reduceToNF = unfoldr step where 
  step t = 
      let next = reduсe t in 
    if t `alphaEq` next 
    then Nothing 
    else Just (t, next)

Не видите ли вы червоточины в этой схеме?