list - 证明流的平等

Question

我有一个数据类型

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 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 是近似函数。如果没有明确的共归纳证明，我如何证明相等？

Answer 1

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

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