Предположим, у нас определено Розовое дерево, а также соответствующая складка по типу данных.
data RTree a = Node a [RTree a]
foldRTree :: (a -> [b] -> b) -> RTree a -> b
foldRTree f (Node x xs) = f x (map (foldRTree f) xs)
Рекурсивное определение первого обхода глубины такой структуры будет:
dft :: RTree a -> [a]
dft (Node x xs) = x : concat (map dft xs)
Мы можем выразить dft как складку над деревьями роз, и, в частности, мы можем вывести такую складку алгебраически.
// Suppose dft = foldRTree f
// Then foldRTree f (Node x xs) = f x (map (foldRTree f) xs) (definition of foldRTree)
// But also foldRTree f (Node x xs) = dft (Node x xs) (by assumption)
// = x : concat (map dft xs) (definition of dft)
// So we deduce that f x (map (foldRTree f) xs) = x : concat (map dft xs)
// Hence f x (map dft xs) = x : concat (map dft xs) (by assumption)
// So we now see that f x y = x : concat y
Я полагаю, что причина, по которой мы можем это сделать, заключается в том, что foldRTree фиксирует общую структуру рекурсиичерез RTrees, что приводит меня к моему запросу о развертывании.
Мы определяем развертывание следующим образом:
unfold :: (a -> Bool) -> (a -> b) -> (a -> a) -> a -> [b]
unfold n h t x | n x = []
| otherwise = h x : unfold n h t (t x)
// Or Equivalently
unfold' n h t = map h . takeWhile (not.n) . iterate t
Мы можем выразить первый обход глубины как развертывание следующим образом:
dft (Node x xs) = x : unfold null h t xs
where h ((Node a xs) : ys) = a
t ((Node a xs) : ys) = xs ++ ys
Я изо всех сил стараюсь найти способ алгебраического вычисления функций nht так же, как и cons.В частности, есть гениальный шаг в развитии раскрытия, который заключается в том, чтобы понять, что последний аргумент для раскрытия должен быть типа [RTree a], а не только RTree a.Поэтому аргумент, заданный для dft, не передается прямо в развёртывание, и поэтому мы сталкиваемся с препятствиями в рассуждениях об этих двух функциях.
Я был бы чрезвычайно благодарен любому, кто мог бы предоставить математический способ рассуждения оразвернуть таким образом, чтобы вычислить требуемые функции nh и t при выражении рекурсивной функции (то есть, естественно, сгиба) как раскрытия (возможно, с использованием некоторых законов, связывающих сложение и развертывание?).Тогда возникает естественный вопрос: какими методами мы должны доказать такое отношение?