![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Entry tags:
Трудности с простыми лямбда-калькуляторами
А вот, кстати, при проверке лямбда-калькуляторов, написанных студентами, возникла такая задачка.
Пускай мы реализовали на Хаскелле лямбда-термы
Если мы теперь хотим реализовать многошаговую бета-редукцию до нормальной формы, мы можем итерировать, делая шаг редукции до тех пор, пока терм не перестанет меняться. Ну, например, так
Не видите ли вы червоточины в этой схеме?
Пускай мы реализовали на Хаскелле лямбда-термы
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)
Не видите ли вы червоточины в этой схеме?
no subject
no subject
no subject
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).
no subject
Тут есть другая бяка в схеме, которую, кстати, непонятно каким test suit'ом ловить. Эта схема врёт на одном достаточно просто устроенном терме.
no subject
Я предполагаю, что оно может возникнуть по 4 причинам:
1) баг в alphaEq, который некоторые эквивалентные термы не считает таковыми
2) баг в reduce, приводящий к циклу длиной более 1 либо к "как это будет редукция наоборот"
3) терм, описывающий рекурсивное выражение, который при редукции не сокращается, а раскрывается всё больше и больше
4) подлинно рекурсивный терм, вида let t = App t t in t - для которого синтаксическое дерево анализировать бесполезно, нужна редукция на графе
no subject
no subject
Может, дело в порядке подстановки? Что-то типа
no subject
no subject
f x y = y x f
f f f
no subject
то это была бы бесконечная цепочка редукций, которую наша схема правильно бы воспроизвела.
no subject
Я так понимаю, что
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, она просто никогда не остановится.
no subject
То что в скобках теперь неподвижная точка для f, используя, например, Y-комбинатор fixY = \p -> (\q -> p (q q)) (\q -> p (q q)) имеем:
То есть f и, следовательно, f f f будут термами фиксированной конечной длины, поэтому проблема не в зависании проверялки.
no subject
no subject
Кстати, отсюда мораль: вместо детерминированной редукции, которая может пойти по дороге в ад, надо недетерминированную: строить дерево всех одношаговых редукций и останавливаться на любом нередуцируемом терме (поиск вширь, а не вглубь). Ну или для приличия сделать ещё несколько попыток для нахождения второго нередуцируемого терма...
монадическая
reduce :: Term -> [Term]
и пусть она возвращает только редукции, а не оригинал.
Т.е. вместо if canReduce t then doReduce t
там будет t'<-allReduces t
Возможно, прямо в недрах делать отсеивание опасностей...
no subject
no subject
Если редукция идёт по единственному пути и делает всё правильно;
если функция построения списка итераций до первого равенства смежных элементов делает всё правильно;
то остаётся уязвимость в alphaEq.
Тогда это не уязвимость, а баг.
Потому что для редукции известны несколько разных стратегий, дающих существенно разные результаты; а для итераций - проблема остановки. То есть там глюки возможны в штатном режиме.
no subject
no subject
no subject
no subject
Что он не равен сам себе?!
no subject
Просто функция reduceToNF названа неправильно.
Из неподвижной точки r == reduce r не следует, что это нормальная форма (импликация там в обратную сторону, из нормальности следует неподвижность).
Отсюда, таки, мораль! reduce должна возвращать монаду - Maybe или [], по вкусу. Смысл которой - "мне удалось что-то внутри редуцировать".
Тогда и reduceToNF будет простой донельзя: unfoldr reduceMaybe.
И проверка альфа-эквивалентности не нужна.
no subject
ни о чём не говорит. (\x -> x x)(\x -> x x) мне всегда удастся что-то внутри редуцировать.
no subject
А вот в этом списке уже можно будет отдельными силами выявить циклы длиной 1, 2, сколько угодно.
Потому как
(\x->x x)(\x->x x)ничем не лучше вышеупомянутогоfixY (\z x y -> y x z)Или вдруг коварный Денис предложит студентам написать на лямбда-исчислении и на числах Чёрча вычислитель 3x+1. Который для крендильона первых натуральных чисел циклится с периодом 3 (1-4-2-1), но до конца в этом никто не уверен.
Кстати, Денис! Тема же для студней, э? :))
no subject
no subject
Тогда мне нужно перестать думать, что reduceToNF задумано было как останавливающаяся, когда обнаружен цикл. Наоборот, факт, что оно останавливается на (\x -> x x)(\x -> x x) и есть баг.
no subject
no subject
no subject