證明流

平等我有一個數據類型證明流

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

回答

相關問題