2007/12/13

Coding Week

本來跟 scm 老師說如果這兩週進度異常順利,才會有時間想想 relational derivation in Agda,結果不但進度異常不順利,還在課堂間偷寫了一點點 Agda XD。現在要在兩三天內把 AI task 1 和 DCL lab 5 生出來,非常緊了 XD。

Agda 的話其實只是證了一兩個簡單的定理,畢竟是課間弄出來的 XD。像 relational fold 可以精煉(refine):

rel-fold-refine : {A B : Set} ->
  (R₁ R₂ : B ← (A × B)) (S₁ S₂ : ℙ B) ->
    R₁ ⊒ R₂ -> S₁ ⊇ S₂ -> fold R₁ S₁ ⊒ fold R₂ S₂

然後夠精煉的 relational fold 就可以轉成 functional fold:

rel-fold-to-foldr : {A B : Set} -> (f : A -> B -> B) (e : B) ->
                      fold (fun (uncurry f)) (sing e) ⊒ fun (foldr f e)

其中 foldrData.List 裡面的版本,所以 f 外面要套上 uncurrysing 則是把一個元素轉成 singleton set。我覺得要從 ordered? ○ perm 導出 insertion sort 還是非常難 ─ perm 在上次 quick sort 大冒險的時候就已經證明是相當難搞的東西了 XD。

Relational composition 的 associativity 也讓我想了一陣,以致於圖論的第二節都聽不太懂 XD。本來想說是不是可以設法讓兩邊轉成某種 normal form(如 prenex normal form)然後推過去,最後把過程藏在 chain reasoning 下面變成自動的,可是弄一弄發現我不會給 type XD。

最後在 Agda Wiki 上面看到關於 universe polymorphism 的討論,感覺上和 '←'、'○' 的多版問題有關,不過不知道是不是真的有關 XD。

--
緊張刺激 XD。

Labels: ,

<< 回到主頁