Давайте выдвинем гипотезу о более сильном свойстве и просто посчитаем, не задумываясь, и посмотрим, куда оно нас приведет.А именно, тем более сильным свойством будет то, что всякий раз, когда xs
не является пустым, мы имеем:
flatten (reverseflatten xs) = xs
Из определения reverseflatten
следует рассмотреть четыре случая.Во-первых, это:
flatten (reverseflatten [x]) = [x]
flatten (Leaf x) = [x]
Далее:
flatten (reverseflatten [x,y]) = [x,y]
flatten (UNode x (Leaf y)) = [x,y]
Затем:
flatten (reverseflatten [x,y,z]) = [x,y,z]
flatten (Node (Leaf x) y (Leaf z)) = [x,y,z]
Наконец:
flatten (reverseflatten (x:y:xs)) = x:y:xs
flatten (revflat2 (x:y:xs)) = x:y:xs
Поскольку предыдущийпаттерны охватили ситуации, когда xs
соответствует []
или [_]
, нам нужно рассмотреть только один случай revflat2
, а именно тот, где xs
имеет как минимум два элемента.
flatten (revflat2 (x:y:w:z:xs)) = x:y:w:z:xs
flatten (Node (Leaf x) y (revflat2 (z:w:xs))) = x:y:w:z:xs
Aha!Чтобы это работало, было бы неплохо иметь помощника с новым свойством, а именно:
flatten2 (revflat2 (z:w:xs)) = w:z:xs
(на самом деле мы будем использовать имена x
и y
вместо w
иz
, конечно.) Еще раз давайте посчитаем, не задумываясь.Есть три случая для xs
, а именно []
, [_]
и более.Когда xs
равно []
:
flatten2 (revflat2 [x,y]) = [y,x]
flatten2 (UNode y (Leaf x)) = [y,x]
Для [_]
:
flatten2 (revflat2 [x,y,z]) = [y,x,z]
flatten2 (Node (Leaf x) y (Leaf z)) = [y,x,z]
И дольше:
flatten2 (revflat2 (x:y:w:z:xs)) = y:x:w:z:xs
flatten2 (Node (Leaf x) y (revflat2 (z:w:xs))) = y:x:w:z:xs
По предположению индукции мыиметь flatten2 (revflat2 (z:w:xs)) = w:z:xs
, так что это последнее уравнение может стать:
flatten2 (Node (Leaf x) y rest) = y:x:flatten2 rest
Теперь мы можем просто взять все последние строки каждого из этих случаев, и они составляют программу:
flatten (Leaf x) = [x]
flatten (UNode x (Leaf y)) = [x,y]
flatten (Node (Leaf x) y (Leaf z)) = [x,y,z]
flatten (Node (Leaf x) y rest) = x:y:flatten2 rest
flatten2 (UNode y (Leaf x)) = [y,x]
flatten2 (Node (Leaf x) y (Leaf z)) = [y,x,z]
flatten2 (Node (Leaf x) y rest) = y:x:flatten2 rest
Это лучшая программа?Нет!В частности, это частично - у вас есть несколько бесплатных вариантов того, что должны делать flatten
и flatten2
, когда первый аргумент дерева для Node
или UNode
не является Leaf
(но не имеет значениякакой выбор вы сделаете, это не повлияет на интересующую вас собственность) и на то, что flatten2
следует делать с листьями.Вероятно, если вы сделаете правильный выбор, вы можете объединить многие шаблоны.
Но что хорошо в этом процессе, так это то, что он полностью механический: вы можете взять интересующее вас имущество, повернутьпровернуть, и получить функцию с этим свойством (или противоречивые уравнения, которые говорят вам, что это невозможно и почему).Только когда у вас есть что-то, что работает, вам нужно смотреть и думать о том, что сделало бы это красивее или лучше.Уууууууу!