Haskell - 如何将最大值 (xs++ map (x+) xs) 转换为 max (最大 xs) (x + 最大 xs)

Question

“用 Haskell 进行函数式思考”中的练习之一是使用融合定律使程序更加高效。我在尝试复制答案时遇到了一些麻烦。

部分计算要求您将 maximum (xs++ map (x+) xs) 转换为 max (maximum xs) (x + Maximum xs)等式推理。

maximum 被定义为 foldr1 max 并且由于我不知道围绕foldr1的许多规则，我什至被困在转换 的第一部分foldr1 max (xs++ map (x+) xs) 到 max (foldr1 max xs) (foldr1 max (map (x+) xs)) 所以这是我想要的第一件事来理解。

一旦我们克服了这一点，下一部分就显得更难了，即将 foldr1 max (map (x+) xs) 转换为 x + Foldr1 max xs。直觉上这是有道理的；如果您要查找所有添加了“x”的一组数字的最大值，那么这与查找添加“x”之前的所有数字的最大值并将“x”添加到结果中是相同的。

我发现在第二阶段唯一对我有帮助的是 this stack overflow answer答案基本上是给你的(如果你假设 p = q)，没有像你通常在等式推理中看到的那样易于理解的单独步骤。

那么请有人告诉我进行转换的步骤吗？

Answer 1

这可以通过归纳法看出。

假设，xs == [] 。两个表达式都是 true，因为两者都会产生 error .

假设，xs == [y]

maximum([y]++map(x+)[y]) == -- by definition of map
                         == maximum([y]++[x+y])
                            -- by definition of ++
                         == maximum([y,x+y])
                            -- by definition of maximum
                         == foldr1 max [y,x+y]
                            -- by definition of foldr1
                         == max y (foldr1 max [x+y])
                            -- by definition of foldr1
                         == max y (x+y)
                            -- by definition of foldr1 and maximum [y]
                         == max (maximum [y]) (x+maximum [y])

接下来，我们需要 maximum 的交换性证明:maximum (xs++(y:ys)) == max y (maximum (xs++ys)) - 如果您跳过此证明并直接转到 maximum (y:ys ++ map(x+)(y:ys)) 的证明，您会注意到这是必要的- 一步需要移动(x+y)从列表中间开始 ys++(x+y):map(x+)ys .

假设，xs==[] :

maximum ([]++(y:ys)) == maximum (y:ys)
                     -- by definition of foldr1 and maximum
                     == max y (maximum ys)
                     == max y (maximum ([]++ys))

假设，xs==x:xx :

maximum(x:xx++(y:ys)) == maximum (x:(xx++(y:ys)))
                     -- by definition of foldr1 and maximum
                      == max x (maximum (xx++(y:ys)))
                     -- by induction
                      == max x (max y (maximum (xx++ys)))
 -- by commutativity of max, max a (max b c) == max b (max a c)
                      == max y (max x (maximum (xx++ys)))
                     -- by definition of foldr1 and maximum
                      == max y (maximum (x:(xx++ys)))
                     -- by definition of ++
                      == max y (maximum ((x:xx) ++ ys))

好吧，现在回到证明原来的说法。现在，假设xs == y:ys

 maximum (y:ys ++ map(x+)(y:ys)) ==
 -- by definition of map
                         == maximum(y:ys ++ (x+y):map(x+)ys)
 -- by definition of foldr1 and maximum
                         == max y (maximum(ys ++ (x+y):map(x+)ys)
 -- by commutativity of maximum
                         == max y (max (x+y) (maximum (ys++map(x+)ys)))
 -- by induction, (maximum (ys++map(x+)ys)) == max (maximum ys) (x+maximum ys))
                         == max y (max (x+y) 
                                       (max (maximum ys) (x+maximum ys)))
 -- by commutativity of max (ie max a (max b c) == max b (max a c))
                         == max y (max (maximum ys) 
                                       (max (x+y) (x+maximum ys)))
 -- by associativity of max (is max a (max b c) == max (max a b) c)
                         == max (max y (maximum ys))
                                       (max (x+y) (x+maximum ys)))
                         -- by definition of max, max (x+y) (x+z) == x+(max y z)
                         == max (max y (maximum ys))
                                       (x + max y (maximum ys)))
                         -- by definition of foldr1 and maximum
                         == max (maximum (y:ys)) (x + maximum (y:ys))

<小时/>

既然您还询问了归纳法以及如何看待某个事物可以通过归纳法来证明，这里还有更多内容。

您可以看到一些步骤是“根据定义”的 - 通过查看函数的编写方式我们知道它们是正确的。例如，maximum = foldr1 max和foldr1 f (x:xs) = f x $ foldr1 f xs对于非空 xs 。其他一些事物的定义不太清楚 - max y z max的定义未显示；然而，通过归纳可以证明max (x+y)(x+z) == x+max y z 。这里从 max 0 y == y 的定义开始，那么怎么算max为了更大x 。 (然后您还需要以类似的方式涵盖负 x 和 y 的情况。)

例如，自然数为零以及自然数的任何后继。你看，这里我们没有定义任何比较，什么都没有。因此，加法、减法、最大值等属性源自函数的定义:

data Nat = Z | S Nat -- zero and any successor of a natural number
(+) :: Nat -> Nat -> Nat -- addition is...
Z + x = x -- adding zero is neutral
(S x) + y = S (x + y) -- recursive definition of (1+x)+y = 1+(x+y)
-- here unwittingly we introduced associativity of addition:
-- (x+y)+z=x+(y+z)
-- so, let's see the simplest case:
-- x == Z
-- (Z+y)+z == -- by definition, Z+y=y -- see the first line of (+)
--         == y+z
--         == Z+(y+z) -- by definition, Z+(y+z)=(y+z)
--
-- ok, now try x == S m
-- (S m + y) + z == -- by definition, (S m)+y=S(m+y) -- see the second line of(+)
--               == S (m+y) + z
--               == S ((m+y)+z) -- see the second line of (+)
--                                 - S (m+y) + z = S ((m+y)+z)
--               == S (m+(y+z)) -- by induction, the simpler
--                                 case of (m+y)+z=m+(y+z)
--                                 is known to be true
--               == (S m)+(y+z) -- by definition, see second line of (+)
-- proven

然后，因为我们还没有对 Nats 进行比较，所以必须定义 max以特定的方式。

max :: Nat -> Nat -> Nat
max Z y = y -- we know Z is not the max
max x Z = x -- and the other way around, too
-- this inadvertently introduced commutativity of max already

max (S x) (S y) = S (max x y) -- this inadvertently introduces the law
-- that max (x+y) (x+z) == x + (max y z)

假设，我们想证明后者。假设x == Z

max (Z+y) (Z+z) == -- by definition of (+)
                == max y z
                == Z + (max y z) -- by definition of (+)

好的，现在假设 x == S m

max ((S m) + y) ((S m)+z) == -- by definition of (+)
                == max (S(m+y)) (S(m+z))
                -- by definition of max
                == S (max (m+y) (m+z))
                -- by induction
                == S (m+(max y z))
                -- by definition of (+)
                == (S m)+(max y z)

所以，你看，了解定义很重要，证明最简单的情况很重要，在稍微复杂的情况下使用简单情况的证明也很重要。