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

[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 x y = y x f
f f f

будет редуцироваться так:

(upd: ~> наверное, что-то своё означают, напишу-ка, как знаю)

(x -> y -> y x f) f f
(y -> y f f) f
f f f = (x -> y -> y x f) f f
(y -> y f f) f
...

Поскольку проверялка будет сравнивать (x -> y -> y x f) f f и (y -> y f f) f, она просто никогда не остановится.

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