haskell - 证明展开的融合定律

Question

我正在阅读 Jeremy Gibbons 的文章 origami programming我被困在练习 3.7 上，它要求读者证明列表展开的融合定律:

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

if

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

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

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

双相似性在理论上很棘手，我不会深入研究(部分原因是我不完全理解其基础)，但在实践中使用它并不太难。基本上，要证明两个列表是相似的，您需要证明它们都是 Nil ，或者它们都是 Cons具有相同的头部和尾部是双相似的，并且在证明尾部的双相似性时您可以使用共归纳假设(但不是在其他地方)。

所以对你来说，我们通过联合归纳证明对于所有 b (因为我们需要对不同的 b s 使用共归纳假设):

(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那么是真的

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 }

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