3

“用 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”添加到结果中相同。

在第二阶段，我发现唯一对我有帮助的是这个堆栈溢出答案 ，答案基本上是给你的（如果你假设 p = q），没有像你通常用等式推理看到的那样容易理解的步骤。

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

4

2 回答 2

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)

引理的证明遵循归纳法。首先，让我们记住我们的定义：

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

然后，对于 A：

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

以此类推，自己试试吧。

于 2014-12-02T23:37:39.970 回答
2

这可以通过归纳看出。

假设，xs == []。两个表达式都是正确的，因为两者都 yield 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)

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

于 2014-12-03T00:55:07.210 回答