18

我有一个数据类型

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

4

3 回答 3

4

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

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

于 2011-05-18T16:11:44.890 回答
3

以下是我认为有效并保持在程序语法和等式推理级别的一些东西的草图。

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)
于 2011-03-07T16:43:20.153 回答
1

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

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

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

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

这使您可以一次停止一个学期。这给了你你的感应。

于 2011-03-10T18:40:42.080 回答