21

我阅读 RWH 失败；没有人要退出，我订购了 Haskell: The Craft of Functional Programming。现在我对第 146 页上的这些功能证明感到好奇。具体来说，我正在尝试证明 8.5.1 sum (reverse xs) = sum xs。我可以做一些归纳证明，但后来我被卡住了..

炒作：

sum ( reverse xs ) = sum xs

根据：

sum ( reverse [] ) = sum []

Left  = sum ( [] ) (reverse.1)
      = 0          (sum.1)

Right = 0          (sum.1)

就职：

sum ( reverse (x:xs) ) = sum (x:xs) 

Left = sum ( reverse xs ++ [x] )    (reverse.2)

Right = sum (x:xs)   
      = x + sum xs                  (sum.2)

所以现在我只是想证明它Left sum ( reverse xs ++ [x] )等于Right x + sum xs，但这与我开始的地方并不太远sum ( reverse (x:xs) ) = sum (x:xs)。

我不太确定为什么需要证明这一点，使用reverse x:y:z = z:y:x(by defn) 的符号证明似乎完全合理，因为 + 是可交换的 (arth) then reverse 1+2+3 = 3+2+1，

4

4 回答 4

24 
sum (reverse [])     = sum []                     -- def reverse
sum (reverse (x:xs)) = sum (reverse xs ++ [x])    -- def reverse
                     = sum (reverse xs) + sum [x] -- sum lemma below
                     = sum (reverse xs) + x       -- def sum
                     = x + sum (reverse xs)       -- commutativity assumption!
                     = x + sum xs                 -- inductive hypothesis
                     = sum (x:xs)                 -- definition of sum

但是，有一些基本的关联性和交换性假设没有得到严格保证，这对于许多数字类型（例如违反这些假设的地方Float）将无法正常工作。Double

引理：sum (xs ++ ys) == sum xs + sum ys给定的关联性(+)

证明：

sum ([] ++ ys)     = sum ys           -- def (++)
                   = 0 + sum ys       -- identity of addition
                   = sum [] ++ sum ys -- def sum

sum ((x:xs) ++ ys) = sum (x : (xs ++ ys))  -- def (++)
                   = x + sum (xs ++ ys)    -- def sum 
                   = x + (sum xs + sum ys) -- inductive hypothesis
                   = (x + sum xs) + sum ys -- associativity assumption!
                   = sum (x:xs) + sum ys   -- def sum
于 2010-07-15T13:31:47.967 回答
6

基本上你需要证明

sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]

然后很容易导致

                        = x + sum (reverse xs)
                        = x + sum xs  -- by inductive hyp.

问题是表明sum分布在列表连接上。

于 2010-07-15T03:08:26.777 回答
4

使用和的定义将 (sum reverse xs ++[x]) 分解为 x + sum(reverse(xs))，并使用您的归纳假设知道 sum(reverse(xs)) = sum(xs)。但我同意，对于这样的问题，归纳是矫枉过正的。

于 2010-07-15T03:08:26.063 回答
3

这就是我认为你被卡住的地方。你需要证明一个引理说

sum (xs ++ ys) == sum xs + sum ys

为了证明这个定律，你必须假设加法是结合的，这仅适用于整数和有理数。

然后，您还需要假设加法是可交换的，这对于整数和有理数都是正确的，对于浮点数也是如此。

题外话：你证明的风格对我来说很奇怪。如果您使用Graham Hutton 书中的风格，我认为您将更轻松地编写此类证明。

于 2010-07-15T16:49:22.530 回答