2008/02/16

Adventure in Oxford

我懶得寫了耶,反正看到很多東西,Oxford 的環境很不錯 XD。scm 老師的朋友寫了一張參觀路線給我,還借我他的職員證,所以我可以憑證進入各個學院(不然要繳錢或根本進不去)。中間 scm 老師的學妹帶我進她的學院吃中餐(就是 Harry Potter 電影裡的餐廳!)以及參觀。總之看了幾個學院、參觀兩個博物館、和 Oxford 一些其他的地標。Postcards 我剛剛弄好了,明天丟進郵筒裡。

回來突然想到 Jeremy 昨天講的話,試著改用 universal property(的一個方向)證明 fold fusion,果然一句話就解決了,因為 induction 現在藏在 universal property 的證明裡面。

foldr-univr : {A B : Set} -> (h : [ A ] -> B) -> forall f e ->
  (h [] ≡ e) -> (forall x xs -> h (x ∷ xs) ≡ f x (h xs)) ->
  (forall x -> h x ≡ foldr f e x)
foldr-univr h f e base-cond step-cond []       = base-cond
foldr-univr h f e base-cond step-cond (x ∷ xs) =
  ≡-trans (step-cond x xs)
          (≡-cong (f x) (foldr-univr h f e base-cond step-cond xs))

foldr-fusion : {A B C : Set} -> (h : B -> C) -> {f : A -> B -> B} ->
  {g : A -> C -> C} -> {e : B} -> (forall x y -> h (f x y) ≡ g x (h y)) ->
  forall x -> (h ∘ foldr f e) x ≡ foldr g (h e) x
foldr-fusion {_} {_} {_} h {f} {g} {e} fuse-cond =
  foldr-univr (h ∘ foldr f e) g (h e) ≡-refl
              (\x xs -> fuse-cond x (foldr f e xs))

--
快離開 Oxford 嘍。

Labels: ,

Blogger yen32/16/2008 11:16 pm 說:

喔喔喔,有明信片了~

 

<< 回到主頁