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

[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]

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

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

[deni-ok.livejournal.com]

Не, дело совсем не в этом. Это я просто писал ни разу не запуская, кода reduce под рукой не было. Там достаточно поменять в последней строке на Just (next, next) и у нас будет опять не хватать, но уже изначального терма, который у пользователя и так есть.

Тут есть другая бяка в схеме, которую, кстати, непонятно каким test suit'ом ловить. Эта схема врёт на одном достаточно просто устроенном терме.

[kodt-rsdn.livejournal.com]

Хотелось бы узнать, какого рода враньё.
Я предполагаю, что оно может возникнуть по 4 причинам:
1) баг в alphaEq, который некоторые эквивалентные термы не считает таковыми
2) баг в reduce, приводящий к циклу длиной более 1 либо к "как это будет редукция наоборот"
3) терм, описывающий рекурсивное выражение, который при редукции не сокращается, а раскрывается всё больше и больше
4) подлинно рекурсивный терм, вида let t = App t t in t - для которого синтаксическое дерево анализировать бесполезно, нужна редукция на графе

[deni-ok.livejournal.com]

Ближе всего третье, хотя не в точности :)

[kodt-rsdn.livejournal.com]

Не томи, покажи этот терм.

Может, дело в порядке подстановки? Что-то типа

const = \x . \y . x
bigboom = \x . какая-то-адская-рекурсивная-фигня
fortytwo = \x . const 42 (bigboom x)

[deni-ok.livejournal.com]

Нет, ничего адского, всё очень чинно, немного автоаппликации, типа Y-комбинатора, но несколько проще.

[sassa-nf.livejournal.com]

поскольку reduceToNF проверяет только две смежные редукции, нужно найти такую форму, где редукции повторяются с бОльшим шагом.

f x y = y x f
f f f

[deni-ok.livejournal.com]

горячо, но не до конца понятно. Если бы было

x ~> y ~> z ~> x ~> y ~> z ~> x ~> ...

то это была бы бесконечная цепочка редукций, которую наша схема правильно бы воспроизвела.

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

[kodt-rsdn.livejournal.com]

Ну хорошо, чинная рекурсивная фигня. Мне просто влом её сочинять, особенно, не видя реализации reduce и не зная её уязвимого места.
Кстати, отсюда мораль: вместо детерминированной редукции, которая может пойти по дороге в ад, надо недетерминированную: строить дерево всех одношаговых редукций и останавливаться на любом нередуцируемом терме (поиск вширь, а не вглубь). Ну или для приличия сделать ещё несколько попыток для нахождения второго нередуцируемого терма...
монадическая
reduce :: Term -> [Term]
и пусть она возвращает только редукции, а не оригинал.
Т.е. вместо if canReduce t then doReduce t
там будет t'<-allReduces t
Возможно, прямо в недрах делать отсеивание опасностей...

[deni-ok.livejournal.com]

Уязвимость не в reduce, reduce всё делает правильно)

[kodt-rsdn.livejournal.com]

Ну расскажи уже, что там на самом деле-то? Заинтриговал донельзя.

Если редукция идёт по единственному пути и делает всё правильно;
если функция построения списка итераций до первого равенства смежных элементов делает всё правильно;
то остаётся уязвимость в alphaEq.
Тогда это не уязвимость, а баг.
Потому что для редукции известны несколько разных стратегий, дающих существенно разные результаты; а для итераций - проблема остановки. То есть там глюки возможны в штатном режиме.

[deni-ok.livejournal.com]

(\x -> x x) (\x -> x x)

Этот терм не имеет нормальной формы, превращаясь сам в себя при бета-редукции единственного редекса. И при этом не меняясь ни капли.

[sassa-nf.livejournal.com]

ну. reduceToNF, насколько я понимаю, обнаружит этот случай и остановится. То есть, результат работы reduceToNF не всегда NF. Ладно, но другие термы тоже могут не иметь NF, но редуцироваться в термы, которые не равны терму на предыдущем или следующем шаге редукции, и, в частности, повесят проверялку.

[sassa-nf.livejournal.com]

можно и попроще что-то написать, вроде (\x -> x (x x))(\x -> x x)

[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]

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

[sassa-nf.livejournal.com]

reduceToNF = foldr f [] . iterate reduce where
  f p n = p: if p `alphaEq` (head n) then [] else n