Уравнение из «Программирования жемчуга» - кто-нибудь может мне объяснить? - PullRequest
Новая
       1

Уравнение из «Программирования жемчуга» - кто-нибудь может мне объяснить?

8 голосов
/ 01 ноября 2011

У меня такое чувство, что я застрял, друзья мои. Может кто-нибудь объяснить мне, выбрать уравнения из "Жемчужины функционального алгоритма", глава 11 ("Не максимальная сумма сегмента")

Вот проблема (немного упрощенная) Пусть у нас есть несколько состояний с заданными переходами: 

data State = E | S | M | N 
                deriving (Show, Eq) 

step E False = E 
step E True = S 
step S False = M 
step S True = S 
step M False = M 
step M True = N 
step N False = N 
step N True = N

Теперь давайте определим выбор: 

 pick q = map snd . filter ((== q) . fst) . map (\a -> (foldl step E a, a))

Автор утверждает, что выполняются следующие семь уравнений: 

pick E xs = [[]]
pick S [ ] = [ ]
pick S (xs ++ [x]) = map (++[x ]) (pick S xs ++ pick E xs)
pick M [ ] = [ ]
pick M (xs ++ [x ]) = pick M xs ++ pick S xs
pick N [ ] = [ ]
pick N (xs ++ [x]) = pick N xs ++ map (++[x]) (pick N xs ++ pick M xs)

Может кто-нибудь объяснить мне простыми словами, почему эти уравнения верны, как мы можем доказать очевидное доказательство? Я чувствую, что почти понимаю S-уравнения, но в целом это остается неясным.

1 Ответ

18 голосов
/ 01 ноября 2011

Хорошо, мне нужно визуализировать ваш график состояний:

q7967337

И дать подпись типа для pick :: State -> [[Bool]] -> [(State, [Bool]).

Теперь это не совпадает с вашим первым уравнением pick E xs = [[]] - это должно быть pick E xs = [(E,[])].

Возможно, вы хотели определить pick так: 

pick :: State -> [[Bool]] -> [[Bool]]
pick q = map snd . filter ((== q) . fst) . map (\a -> (foldl step E a, a))

Принимая это определение, первое уравнение теперь имеет смысл. Он утверждает, что если вы начнете с E, единственная последовательность логических значений в xs, которая оканчивается на E, это пустой список.

Обратите внимание, что это предполагает, что [] & isin; xs.

Кроме того, если ys = replicate n False, pick E [ys] = [ys], то это означает, что & forall; n, ys & notin; xs.

Второе, четвертое и шестое уравнения имеют форму pick _ [ ] = [ ], что тривиально верно по определению map и filter.

Третье уравнение, pick S (xs ++ [x]) = map (++[x ]) (pick S xs ++ pick E xs) тоже не имеет смысла. Я предполагаю, что он пытается сказать: 

pick S (map (++[True] xs) = map (++[True]) (pick S xs ++ pick E xs)

То есть любой путь, начинающийся с E и заканчивающийся S, можно построить, взяв существующий путь к E или S и добавив True. Эквивалентно, что каждый путь, который заканчивается в S, должен заканчиваться True.

Пятое уравнение аналогично бессмысленно и должно быть сформулировано как: 

pick S (map (++[False] xs) = map (++[False]) (pick S xs ++ pick M xs)

И седьмое уравнение следует переформулировать как: 

pick N (map (++ [True]) xs) = pick N xs ++ map (++[True]) (pick N xs ++ pick M xs)
...