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

[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

[sassa-nf.livejournal.com]

хм. Ну, то, что они фиксированной и конечной длины, понятно. Но в f f f всегда можно будет что-то редуцировать, как в примере с (\x -> x x)(\x -> x x). В отличие от (\x -> x x)(\x -> x x), f f f будет генерировать термы, "соседи" которых (т.е. термы, полученные не предыдущем и последующем шагах) не равны, но при этом вести себя в точности как (\x -> x x)(\x -> x x).