我没能读懂《RWH》;我命令没有人放弃Haskell:函数式编程的技巧。现在我对第 146 页上的这些功能证明很好奇。具体来说,我试图证明 8.5.1sum (reverse xs) = sum xs
。我可以做一些归纳证明,但后来我陷入困境。
HYP:
sum ( reverse xs ) = sum xs
BASE:
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) 那么reverse 1+2+3 = 3+2+1
,
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
and Double
违反这些假设的地方。
Lemma: sum (xs ++ ys) == sum xs + sum ys
给定关联性(+)
Proof:
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
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)