用递归公式替换证明

Question

以下问题和部分解决方案来自 Richard Bird 的 Thinking Functionly with Haskell (pp 132-133, 139)

给定

foldl f e (x:xs) = foldl f (f e x) xs
foldl f e [] = e

证明

foldl (@) e xs = foldr (<>) e xs

对于所有有限列表 xs，前提是

1. (x <> y) @ z = x <> (y @ z)

2. e @ x = x <> e

感应盒（左侧）：

foldl (@) e (x:xs)

= {def 折叠}

foldl (@) (e @ x) xs

= {附带条件 2}

foldl (@) (x <> e) xs

---

这显然不是证明的最后一步，但它是我问题的根源：因为

e

是由

foldl

递归扩展的，看起来它的定义取决于递归的阶段，因此不清楚对我来说

e @ x = x <> e

始终是有效的替代。上面的

foldl (@) (e @ x) xs

中，

e

的参数

foldl

采用

e @ x

的值，所以我认为不能应用条件2——要进行替换，它需要是

(e @ x) @ x

Answer 1

我认为你只是忘记了基本情况和归纳假设：

Base case:
foldl (@) e [] = e                 [definition of foldl]
               = foldr (<>) e []   [definition of foldr]

Induction assumption: foldl (@) e xs = foldr (<>) e xs

Induction step:
foldl (@) e (x:xs) = foldl (@) (e @ x) xs   [definition of foldl]
                   = foldl (@) (x <> e) xs  [given e @ x = x <> e]
                   = foldr (<>) (x <> e) xs [assumption]
                   = foldr (<>) e (x:xs)    [definition of foldr]