5

我正在阅读 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？相关问题：有哪些很好的资源可以解释和激发各种归纳技术，例如结构归纳？

4

2 回答 2

3

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

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

双相似性在理论上很棘手，我不会深入探讨（部分原因是我不完全理解基础），但在实践中使用它并不太难。基本上，要证明两个列表是双相似的，您可以证明它们都是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 }

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

于 2017-08-13T23:52:02.050 回答
2

经过一番谷歌搜索后，我发现了同一位 Jeremy Gibbons（和 Graham Hutton）的论文，其中介绍了 corecursive 程序的证明方法；这篇文章包括一个关于互模拟和共归纳的部分，这是@luqui 在接受的答案中使用的证明技术。第 6 节使用展开的普遍性质证明了聚变定律。为了完整起见，我复制了下面的证明。

的普遍性质unfoldL：

h = unfoldL p f g
<=>
∀ b . h b = if p b then Nil else Cons (f b) (h (g b))

聚变定律的证明：

unfoldL p f g . h = unfoldL p' f' g'
<=> { universal property }
∀ b . (unfoldL p f g . h) b = if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
<=> { composition }
∀ b . unfoldL p f g (h b) = if p' b then Nil else Cons (f' b) (unfoldL p f g (h (g' b)))
<=> { unfoldL }
∀ b . if p (h b) then Nil else Cons (p (h b)) (unfoldL p f g (g (h b))) = if p' b then Nil else Cons (f' b) (unfoldL p f g (h (g' b)))
<=> { composition }
∀ b . if (p . h) b then Nil else Cons (p . h) b (unfoldL p f g ((g . h) b)) = if p' b then Nil else Cons (f' b) (unfoldL p f g ((h . g') b))
<=  { assumptions }
(p . h = p') ^ (f . h = f') ^ (g . h = h . g')
于 2017-08-14T11:38:49.017 回答