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

[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

[kodt-rsdn.livejournal.com]

Ну и что нам говорит alphaEq по этому поводу?
Что он не равен сам себе?!

[kodt-rsdn.livejournal.com]

А, понял твою шутку.
Просто функция reduceToNF названа неправильно.
Из неподвижной точки r == reduce r не следует, что это нормальная форма (импликация там в обратную сторону, из нормальности следует неподвижность).

Отсюда, таки, мораль! reduce должна возвращать монаду - Maybe или [], по вкусу. Смысл которой - "мне удалось что-то внутри редуцировать".

Тогда и reduceToNF будет простой донельзя: unfoldr reduceMaybe.
И проверка альфа-эквивалентности не нужна.

[sassa-nf.livejournal.com]

"мне удалось что-то внутри редуцировать"

ни о чём не говорит. (\x -> x x)(\x -> x x) мне всегда удастся что-то внутри редуцировать.

[kodt-rsdn.livejournal.com]

Ну и правильно: reduceToNF честно родит бесконечный список.
А вот в этом списке уже можно будет отдельными силами выявить циклы длиной 1, 2, сколько угодно.

Потому как (\x->x x)(\x->x x) ничем не лучше вышеупомянутого fixY (\z x y -> y x z)
Или вдруг коварный Денис предложит студентам написать на лямбда-исчислении и на числах Чёрча вычислитель 3x+1. Который для крендильона первых натуральных чисел циклится с периодом 3 (1-4-2-1), но до конца в этом никто не уверен.

Кстати, Денис! Тема же для студней, э? :))

[sassa-nf.livejournal.com]

ну а чем тогда монадный способ отличается от сейчашнего?

[sassa-nf.livejournal.com]

а, тьфу! В оригинале же и написано: "В последнем случае при отсутствии редексов просто возвращается исходный терм."

Тогда мне нужно перестать думать, что reduceToNF задумано было как останавливающаяся, когда обнаружен цикл. Наоборот, факт, что оно останавливается на (\x -> x x)(\x -> x x) и есть баг.

[deni-ok.livejournal.com]

Ага.

[deni-ok.livejournal.com]

Да, всё так. При возможной неудаче (в данном случае - отсутствии редукции), нам нужна явная сигнализация об этом, а не реагирование по косвенным признакам.