"珍珠编程"中的等式 - 有人可以解释一下吗？

Question

我的朋友们觉得我被卡住了.有人可以解释我从"功能算法设计珍珠"第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-方程式,但总的来说这仍然是难以捉摸的.

Answer 1

好的,我需要可视化您的状态图:

并为其提供类型签名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是空列表.

请注意,这假设为[]∈ xs.

此外,如果ys = replicate n False,pick E [ys] = [ys]那么这意味着∀ n,ys∉ 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)