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 == []。兩種表述都是真實的，因爲兩者都產生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))證明 - 一個步驟需要從列表ys++(x+y):map(x+)ys的中間移動(x+y)。

假設，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 zmax的定義未顯示;然而，它可以通過感應表明，max (x+y)(x+z) == x+max y z。這裏以max 0 y == y的定義開始，然後如何編制max更大的x。 （然後，您還需要以類似的方式覆蓋負數x和y的情況。）

例如，自然數爲零且爲自然數的後繼數。你看，在這裏我們沒有任何比較定義，什麼都沒有。因此，的屬性加成，減，Max等軟件，自定義的功能幹：

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 

然後，因爲我們沒有NAT的對比的是，在一個特定的定義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) 

所以，你看，它使用的證據是重要的是知道的定義，重要的是證明了簡單的情況下，重要在稍微複雜的情況下更簡單的情況。

Answer 2

草圖：

maximum (xs ++ map (x+) xs) 
foldr1 max (xs ++ map (x+) xs) 
foldr max (foldr1 max xs) (map (x+) xs) 
foldr max (maximum xs) (map (x+) xs) 
max (maximum xs) (foldr1 max (map (x+) xs)) 
max (maximum xs) (x + foldr1 max xs) 
max (maximum xs) (x + maximum xs) 

使用（有可能是較弱的假設，我挑什麼工作）

0. xs, ys are nonempty 
1. f is commutative and associative 
A. foldr1 f (xs ++ ys) == foldr f (foldr1 f xs) ys 
B. foldr f s xs = f s (foldr1 f xs) 
C. foldr1 f (map g xs) = g (foldr1 f xs) 
    if f (g x) (g y) == g (f x y) 

的的證明通過感應lemmata跟隨。 首先，讓我們記住我們的定義：

foldr k z [] = z 
foldr k z (x:xs) = k x (foldr k z xs) 

foldr1 k [z] = z 
foldr1 k (x:xs) = k x (foldr1 k xs) 

map k [] = [] 
map k (x:xs) = k x : map k xs 

然後，答：

To show: foldr1 f (xs ++ ys) == foldr f (foldr1 f xs) ys 
Induction on xs. 
Base case: xs = [x] 
    foldr1 f ([x] ++ ys) == f x (foldr1 f ys) 
    Induction on ys: ys = [y] 
     == f x (foldr f [y]) = f x y = f y x 
     == foldr f x [y] = foldr f (foldr1 f [x]) [y] 
    Step. ys = (y:yy) 
     == f x (foldr1 f (y:yy)) 
     == f x (f y (foldr1 f yy)) -> associativity and commutativity 
     == f y (f x (foldr1 f yy)) -> induction assumption 
     == f y (foldr f x yy) 
     == foldr f (foldr1 f [x]) (y:yy) 
Step: xs = (x:xx) 
    foldr1 f (x:xx ++ ys) = f x (foldr1 f (xx ++ yy)) 
     == f x (fold f (foldr1 f xx) yy) 
     == fold f (foldr1 f xx) (x:yy) 
    Induction on ys. 
    Base case ys = [y] 
     == f x (f y (foldr1 f xx)) == f y (f x (foldr1 f (x:xx)) 
     == fold f (foldr1 f xs) [y] 
    Step. ys = (y:yy) 
     == f x (f y (fold f (foldr1 f xx) yy) -> associativity, commutativity 
     == f y (f x (fold f (foldr1 f xx) yy) -> induction assumption 
     == f y (fold f (foldr1 f (x:xx) yy) 
     == fold f (foldr1 f xs) ys 

等等，自己嘗試一下。