证明流的平等答案

【问题标题】：Proving equality of streams证明流的平等
【发布时间】：2011-07-07 23:31:35
【问题描述】：

我有一个数据类型

data N a = N a [N a]

玫瑰树和应用实例

instance Applicative N where
 pure a = N a (repeat (pure a))
 (N f xs) <*> (N a ys) = N (f a) (zipWith (<*>) xs ys)

并且需要证明它的应用定律。然而，pure 创建了无限深、无限分支的树。因此，例如，在证明同态定律时

pure f <*> pure a = pure (f a)

我认为证明相等

zipWith (<*>) (repeat (pure f)) (repeat (pure a)) = repeat (pure (f a))

通过近似（或采用）引理会起作用。然而，我的尝试在归纳步骤中导致了“恶性循环”。特别是减少

approx (n + 1) (zipWith (<*>) (repeat (pure f)) (repeat (pure a))

给予

(pure f <*> pure a) : approx n (repeat (pure (f a)))

其中 approx 是近似函数。如何在没有明确的归纳证明的情况下证明相等性？

【问题讨论】：

为什么要在不使用共归纳法的情况下证明它？正如归纳是有限列表/树等数据的自然证明方法一样，联合归纳是余数据（如流或“无限深、无限分支的树”）的自然证明方法。
特别是，因为证明是在“程序语法”级别运行的。双相似性证明没有。
这看起来像是 cstheory stackexchange 网站的一个很好的候选者，特别是如果你用稍微更一般/正式的术语来说明它。

标签： list haskell infinite applicative

【解决方案1】：

以下是我认为可行且仍停留在程序语法和等式推理级别的一些东西的草图。

基本的直觉是，推理repeat x 比推理一般的流（更糟糕的是，列表）要容易得多。

uncons (repeat x) = (x, repeat x)

zipWithAp xss yss = 
    let (x,xs) = uncons xss
        (y,ys) = uncons yss
    in (x <*> y) : zipWithAp xs ys

-- provide arguments to zipWithAp
zipWithAp (repeat x) (repeat y) = 
    let (x',xs) = uncons (repeat x)
        (y',ys) = uncons (repeat y)
    in (x' <*> y') : zipWithAp xs ys

-- substitute definition of uncons...
zipWithAp (repeat x) (repeat y) = 
    let (x,repeat x) = uncons (repeat x)
        (y,repeat y) = uncons (repeat y)
    in (x <*> y) : zipWithAp (repeat x) (repeat y)

-- remove now extraneous let clause
zipWithAp (repeat x) (repeat y) = (x <*> y) : zipWithAp (repeat x) (repeat y)

-- unfold identity by one step
zipWithAp (repeat x) (repeat y) = (x <*> y) : (x <*> y) : zipWithAp (repeat x) (repeat y)

-- (co-)inductive step
zipWithAp (repeat x) (repeat y) = repeat (x <*> y)

【讨论】：

【解决方案2】：

为什么需要共同感应？只是感应。

pure f <*> pure a = pure (f a)

也可以写成（需要证明左右相等）

N f [(pure f)] <*> N a [(pure a)] = N (f a) [(pure (f a))]

这允许您一次关闭一个学期。这给了你你的感应。

【讨论】：

我认为你没有抓住重点。你实际上得到了N f (repeat $ pure f) <*> N a (repeat $ pure a) = N (f a) (zipWith (<*>) (repeat $ pure f) (repeat $ pure a))，这直接导致了 danportin 首先想要证明的平等......

【解决方案3】：

我会使用展开的通用属性（因为重复和适当的非咖喱 zipWith 都是展开）。有一个相关的讨论on my blog。但您可能也喜欢 Ralf Hinze 关于独特固定点的论文ICFP2008（以及随后的 JFP 论文）。

（只是检查一下：你所有的玫瑰树都是无限宽和无限深的？我猜法律不会成立。）

【讨论】：