证明融合法的展开

Question

我正在阅读Jeremy Gibbons关于折纸编程的文章,我坚持练习3.7,要求读者证明列表的融合法展开:

unfoldL p f g . h = unfoldL p' f' g'

如果

p . h = p'
f . h = f'
g . h = h . g'

unfoldL列表展开的功能定义如下:

unfoldL :: (b -> Bool) -> (b -> a) -> (b -> b) -> b -> List a
unfoldL p f g b = if p b then Nil else Cons (f b) (unfoldL p f g (g b))

这是我目前尝试的证据:

(unfoldL p f g . h) b
=   { composition }
unfoldL p f g (h b)
=   { unfoldL }
if p (h b) then Nil else Cons (f (h b)) (unfoldL p f g (g (h b)))
=   { composition }
if (p . h) b then Nil else Cons ((f . h) b) (unfoldL p f g ((g . h) b))
=   { assumptions }
if p' b then Nil else Cons (f' b) (unfoldL p f g ((h . g') b))
=   { composition }
if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
=   { ??? }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
=   { unFoldL }
unFoldL p' f' g'

我不确定如何证明标记的步骤???.我应该在函数应用程序上使用某种归纳法b？相关问题:什么是解释和激励各种归纳技术的好资源,例如结构归纳？

Answer 1

我还没有读过吉本斯的文章，他可能依赖其他技术，但这是我所知道的。

您正在寻找某种归纳法，这是一个很好的直觉，因为您需要的东西与您试图证明的东西非常相似。但这里实际上需要共归纳。这是因为unfoldL可以产生无限列表。在形式类型系统中，很少能证明两个无限结构是“相等的”——形式相等性太强，无法证明大多数结果。相反，我们证明了双相似性，在非正式情况下也可能是相等的。

从理论上讲，双相似性很棘手，我不会深入讨论它（部分原因是我不完全理解其基础），但在实践中使用它并不太难。基本上，要证明两个列表是双相似的，您可以证明它们要么都是Nil，或者它们都具有Cons相同的头部并且它们的尾部是双相似的，并且在证明尾部的双相似性时可以使用共归纳假设（但不能使用共归纳假设）别处）。

因此，对于您来说，我们通过共归纳法证明了对于所有人b（因为我们需要对不同的 s 使用共归纳假设b）：

(unfoldL p f g . h) b ~~ unfoldL p' f' g' b

到目前为止我们已经

(unfoldL p f g . h) b
= { your reasoning }
if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))

结合案例分析p' b，如果p' b为True则

if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
= { p' b is True }
Nil
~~ { reflexivity }
Nil
= { p' b is True }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
= { unfoldL }
unfoldL p' f' g'

; 如果p' b为假则

if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
= { p' b is False }
Cons (f' b) ((unfoldL p f g . h) (g' b))
*** ~~ { bisimilarity Cons rule, coinductive hypothesis } ***
Cons (f' b) (unfoldL p' f' g' (g' b))
= { p' b is False }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
= { unfoldL }

标记的那一行***是关键的一行。首先，请注意它是 a~~而不是=。此外，我们只能在构造函数下Cons使用共归纳假设。如果我们被允许在其他地方使用它，那么我们就可以证明任何两个列表都是相似的。