证明展开的融合法则

Question

我正在阅读 Jeremy Gibbons 关于 origami programming 的文章，但我被困在练习 3.7 上，该练习要求 reader 证明 融合定律 列表展开：

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 可以产生无限列表。在正式的类型系统中，您很少能证明两个无限结构是 "equal" —— 正式的相等性太强而无法证明大多数结果。相反，我们证明 bisimilarity，这在非正式情况下也可能是相等的。

双相似性在理论上很棘手，我不会深入研究（部分原因是我不完全理解其基础），但在实践中使用它并不难。基本上，要证明两个列表是双相似的，您可以证明它们要么都是 Nil，要么都是 Cons，并且它们的头相同，尾巴是双相似的， 而您在证明尾部的双相似性时可能会使用余归假设（但在其他地方不会）。

所以对你来说，我们通过协归来证明对于所有b（因为我们需要对不同的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 为真则

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 构造函数下使用余归假设 。如果允许我们在其他任何地方使用它，那么我们就可以证明任意两个列表是双相似的。

Answer 2

经过一些谷歌搜索后，我发现了一篇由同一位 Jeremy Gibbons（和 Graham Hutton）撰写的论文 proof methods for corecursive programs；这篇文章包括一个关于双模拟和共同归纳的部分，@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')

证明展开的融合法则

Proving the fusion law for unfold

haskell

recursion

proof

induction

recursion-schemes