2

我试图通过结构归纳来证明以下陈述：

foldr f st (xs++yx) = f (foldr f st xs) (foldr f st ys)        (foldr.3)

但是我什至不确定如何定义 foldr，所以我被困住了，因为没有向我提供定义。我现在相信 foldr 可以定义为

foldr f st [] = st                                             (foldr.1)
foldr f st x:xs = f x (foldr f st xs)                          (foldr.2)

现在我想开始处理将空列表传递给 foldr 的基本情况。我有这个，但我认为它不正确。

foldr f st ([]++[]) = f (foldr f st []) (foldr f st [])
LHS:
    foldr f st ([]++[]) = foldr f st []                        by (++)
    foldr f st [] = st                                         by (foldr.1)
RHS:
    f (foldr f st []) (foldr f st []) = f st st                by (foldr.1)
    = st                                                       by definition of identity, st = 0

LHS = RHS, therefore base case holds

现在这就是我的归纳步骤：

Assume that:
  foldr f st (xs ++ ys) = f (foldr f st xs) (foldr f st ys)        (ind. hyp)

Show that:
  foldr f st (x:xs ++ ys) = f (foldr f st x:xs) (foldr f st ys)    (inductive step)

LHS:
    foldr f st (x:xs ++ ys) = f x (foldr f st xs) (foldr f st ys)  (by foldr.2)
RHS:
    f (foldr f st x:xs) (foldr f st ys) = 
  = f f x (foldr f st xs) (foldr f st ys)                          (by foldr.2)
  = f x (foldr f st xs) (foldr f st ys)

LHS = RHS, therefore inductive step holds. End of proof.

我不确定这个证明是否有效。我需要一些帮助来确定它是否正确，如果不正确 - 它的哪一部分不是。

4

1 回答 1

2

首先：您可以通过 API 文档找到许多基本 Haskell 函数的定义，该文档可在 Hackage 上找到。的文档base在这里。foldr被导出Prelude，其中有一个指向其源代码的链接：

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr k z = go
          where
            go []     = z
            go (y:ys) = y `k` go ys

出于效率原因，它是这样定义的；查找“工人包装”。相当于

foldr f st [] = st
foldr f st (y:ys) = f y (foldr f st ys)

第二：在您想要的证明中， 的类型f必须是a -> a -> a，它的一般性低于a -> b -> b。

让我们研究一下基本情况 ( xs = ys = [])。

foldr f st ([]++[]) = f (foldr f st []) (foldr f st [])
-- Definition of ++
foldr f st []       = f (foldr f st []) (foldr f st [])
-- Equation 1 of foldr
st                  = f st              st

这个等式一般不成立。要继续证明，您必须假设st是 的身份f。

我相信，在非基本情况下，您还必须假设这f是关联的。这两个假设结合起来表明了这一点f并st形成了一个幺半群。你想证明什么foldMap吗？

于 2014-11-17T03:52:58.360 回答