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

[deni_ok]

А вот, кстати, при проверке лямбда-калькуляторов, написанных студентами, возникла такая задачка.
Пускай мы реализовали на Хаскелле лямбда-термы
data Term = Var String | App Term Term | Lam String Term проверку их альфа-эквивалентности (можно и точное совпадение, для наших целей не важно):
alphaEq :: Term -> Term -> Bool и

Comments

[kodt_rsdn]

Пока натурный эксперимент не поставил, не увидел червоточины.
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]

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

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

[kodt_rsdn]

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

[deni_ok]

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

[kodt_rsdn]

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

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

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

[deni_ok]

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

[sassa_nf]

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

f x y = y x f
f f f

[deni_ok]

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

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

[sassa_nf]

ну, правильно воспроизвела - это одно, а не сможет остановиться при проверке - это другое. В чём смысл проверки на альфа-эквивалентность двух шагов редукции? Чтобы ловить зацикленную проверялку или ещё что-то?

Я так понимаю, что

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]

Моя ~> означает "редуцируется к". Рекурсивных определений у нас нет, см. определение 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]

хм. Ну, то, что они фиксированной и конечной длины, понятно. Но в 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]

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

[deni_ok]

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

[kodt_rsdn]

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

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

[deni_ok]

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

[sassa_nf]

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