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)

其中 foldr 是 Data.List 裡面的版本，所以 f 外面要套上 uncurry。sing 則是把一個元素轉成 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。