1

我马上说这是一个任务，我不是在寻找答案 - 只是一些方向，因为我已经研究了很长一段时间了。给定以下尾递归求和函数：

sumTR [ ] acc = acc  
sumTR (x:xs) acc = sumTR xs (x + acc)

我们必须通过归纳证明： 

sumTR xs (sumTR ys acc) = sumTR (ys ++ xs) acc

在证明了基本情况（在 xs 上感应并将 ys 视为常数）后，我得出： 

sumTR x:xs(sumTR ys acc) = ... = sumTR xs (x + sumTR ys acc)  
sumTR (ys ++ x:xs) acc = ... = sumTR xs (sumTR ys (x + acc))

我们的讲师经历了一个更简单的例子（sum1 xs = sum2 xs，sum1 是简单的递归），当他达到你不能让它们变得更相似的地步时，他证明了一个“更强的属性”，通过注意到类似sum2 xs acc = acc + xs 的总和。然后他设置了一个涉及“for all acc”的归纳假设，然后将 acc 设置为 0。

我遇到的主要问题是 acc 已经在 LHS 和 RHS 上，所以我觉得我已经接近了，但我并没有真正证明更强大的属性（这个问题没有具体要求，但我认为我们应该使用它）。此外，我不确定在将元素取出（或将它们插入）函数时，我可以在多大程度上使用加法的关联性。

任何帮助表示赞赏！

4

1 回答 1

4

做归纳要容易得多ys，因为那时对于空ys，我们有

sumTR xs (sumTR [] acc) =  -- by first case of (inner) sumTR
sumTR xs acc =             -- by definition of (++)
sumTR ([] ++ xs) acc       -- Q.E.D.

对于y:ys，我们有

sumTR xs (sumTR (y:ys) acc) =    -- by second case of (inner) sumTR
sumTR xs (sumTR ys (y + acc)) =  -- by induction
sumTR (ys ++ xs) (y + acc) =     -- by second case of sumTR, "in reverse"
sumTR (y:(ys ++ xs)) acc =       -- by definition of (++)
sumTR ((y:ys) ++ xs) acc         -- Q.E.D.

Going withys对我们有帮助，因为(++)它是由左手参数的递归定义的，ys在这种情况下就是这样。

于 2016-08-27T11:01:44.397 回答