2007/11/04

A Final Remark on scanr

scanr-pf 的 return type 其實可以復用 Logic.Identity module 裡面的 "_≡_" 和 scm 老師定義的 "_⋮_":

scanr-pf' : {A B : Set} -> (f : A -> B -> B) -> (e : B) -> (xs : List A) ->
              List B ⋮ _≡_ ((map (foldr f e) ○ tails) xs)
scanr-pf' f e xs = sub ((foldr (sc f) (e :: [])) xs)
  ( chain> (map (foldr f e) ○ tails) xs
       === foldr (sc f) (e :: []) xs
             by foldr-fusion {_}{_}{_}
                  {til}{[] :: []}{map (foldr f e)}{sc f} fuse-cond xs
  ) where
    fuse-cond : {A B : Set}{f : A -> B -> B}{e : B} ->
                  (x : A)(yss : List (List A)) ->
                  map (foldr f e) (til x yss) ≡ (sc f) x (map (foldr f e) yss)
    fuse-cond x (ys :: yss) = refl

如此就不需要另外造一個 Indeed type,看起來也比較清楚。引進 _⋮_ 的 elimination rule,就可以導出較快的 scanr 版本:

subElim : {A : Set}{P : A -> Set} -> A ⋮ P -> A
subElim (sub x _) = x

scanr' : {A B : Set} -> (A -> B -> B) -> B -> List A -> List B
scanr' f e xs = subElim (scanr-pf' f e xs)

再這樣下去,Agda 就要變成我在 functional programming 上的母語了 XD。

--
我的名字悄悄出現在 scm 老師的網頁上了耶!XD

Labels: ,

Anonymous scm11/04/2007 7:04 am 說:

哇!很棒唷! :)

我昨天看了你這幾篇,晚上我也是想用 _≡_ 和_⋮_ 做做看。不過我覺得 Indeed 也是蠻好的概念。這週中間如果我有空的話,我試著把 mss 的證明寫出來好了。

週五你跟我們談談這個吧?

一個問題是:除了使用 _⋮_ 或 indeed 之外,我們也總是可以直接寫一個 scanr', 定義跟本來 Haskell 裡面的一樣,然後另外寫一個 type 就是

(scanr' f e) ≡ ((map (foldr f e) ○ tails) xs)

的證明。這像是傳統的方式:先寫程式,另外寫證明。

那麼我們用 _⋮_ 把 scanr' 和他的證明綁一起,和傳統方法比較之下有什麼好處呢?

我是希望有些好處啦。這週有空的話我會想想。

 
Blogger Josh Ko11/04/2007 10:15 am 說:

> 週五你跟我們談談這個吧?

OK. XD

> 那麼我們用 _⋮_ 把 scanr' 和他的證明綁一起,和傳統方法比較之下有什麼好處呢?

剛剛睡前隨便想想,好像是得到「沒有特別好處」的結論,不過睡醒後就把細節忘記了 XD。

 

<< 回到主頁