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

[deniok]

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

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

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)

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

Comments

[codedot.livejournal.com]

А не для того ли типы, чтобы на червоточины указывать?

[kodt-rsdn.livejournal.com]

Пока натурный эксперимент не поставил, не увидел червоточины.
reduceToNF показывает все итерации, кроме последней :))
Ведь это имеется в виду, да?

reduceToNF term = unfoldr step (term,True) where
  step t,False = Nothing
  step t,True  = let next = reduce t in
                 Just(t, not $ t `alphaEq` next)

После чего сразу захотелось плюнуть на unfoldr и сделать то же самое на iterate / takeWhile...
Тем более, что она по смыслу более точно подходит: у нас список итераций.

reduceToNF reduce equal = map fst . takeWhile snd . iterate (step . fst) . (,True)
  where
    step t =
      let n = reduce t in
    (t, not $ t `alphaEq` n)

Ибо, один чёрт мы заворачиваем-выворачиваем значения, только вместо Maybe Term здесь (Term,Bool).