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

[deni_ok]

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

Comments

[deni_ok]

Типы дают частичные спецификации, предупреждая возникновение определенных классов червоточин. Обсуждаемая, кстати, ни в одной известной мне типизированной версии лямбда исчисления не имеет места (кроме тех, конечно, в которых все термы имеют тип).

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

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