我正在阅读 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
上的函数应用程序使用某种归纳法。 ?相关问题:有哪些好的资源可以解释和激发各种归纳技术,例如结构归纳?
最佳答案
我没有读过 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
下方使用合归纳假设。构造函数。如果允许我们在其他任何地方使用它,那么我们可以证明任何两个列表是相似的。
关于haskell - 证明展开的融合定律,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/45665417/