证明流

平等我有一个数据类型证明流

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)))

其中约是近似函数。如何证明没有明确的合谋证明的平等？

来源

2011-03-03 danportin

为什么你要证明这一点，而不使用coinduction？正如归纳法是有限列表/树的数据的自然证明方法一样，coinduction是codata的自然证明方法，如流或“无限深，无限分支的树”。 – 2011-03-03 11:56:16

特别是，因为证明在“程序语法”级别运行。双相似性的证明不是。 – danportin 2011-03-03 12:03:10

这看起来很适合cstheory stackexchange站点，尤其是如果你用稍微更一般/正式的术语来说明的话。 – sclv 2011-03-03 18:15:15

以下是我认为可行并且仍然处于程序化语法和等式推理层面的草图。

基本的直觉是，关于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-07 16:43:20 sclv

为什么哟需要coinduction？只是导入。

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

也可以写成（你需要证明的左边和右边的平等）

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

，让您在休息时间一个学期。这给你你的感应。

来源

2011-03-10 18:40:42 jbolden1517

我认为你错过了这一点。你实际上得到了'N f（repeat $ pure f）<*> N a（repeat $ pure a）= N（fa）（zipWith（<*>）（repeat $ pure f）（repeat $ pure a））''直接导致丹波尔丁想要首先证明的平等...... – sclv 2011-03-10 20:28:38

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

（只是检查：所有的玫瑰树是无限宽和无限深我猜，法律将不以其他方式持有？）

来源

2011-05-18 16:11:44

回答

相关问题