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

[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

[deni-ok.livejournal.com]

Моя ~> означает "редуцируется к". Рекурсивных определений у нас нет, см. определение data Term = ..., однако любое рекурсивное определение можно свести к использованию комбинатору неподвижной точки над подходящим термом. Вот цепочка выкладок для получения нерекурсивного определения f:

f x y = y x f
f = \x y -> y x f
f = (\z x y -> y x z) f

То что в скобках теперь неподвижная точка для f, используя, например, Y-комбинатор fixY = \p -> (\q -> p (q q)) (\q -> p (q q)) имеем:

f = fixY (\z x y -> y x z) 

То есть f и, следовательно, f f f будут термами фиксированной конечной длины, поэтому проблема не в зависании проверялки.

[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).