Haskell - Выражение Глубины Первого обхода Розового Дерева в качестве примера раскрытия, вывод его алгебраически
Предположим, у нас есть определенное Розовое дерево, а также соответствующая складка над типом данных.
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 так же, как и против. В частности, есть гениальный шаг в разработке разворачивания, который заключается в осознании того, что последний аргумент для разворачивания должен быть типа [RTree a], а не только RTree a. Поэтому аргумент, заданный для dft, не передается прямо в развёртывание, и поэтому мы сталкиваемся с препятствиями в отношении рассуждений об этих двух функциях.
Я был бы чрезвычайно благодарен любому, кто мог бы предоставить математический способ рассуждения о развертывании таким образом, чтобы вычислить требуемые функции nh и t при выражении рекурсивной функции (которая, естественно, является сгибом), как развертывание (возможно, с использованием некоторых законов связывать складывать и разворачивать?). Тогда возникает естественный вопрос: какими методами мы должны доказать такое отношение?