2009/02/12

AC!

XOO 寫信來討論,我才赫然發現證明 weak bisimilarity 的 transitivity 時為了方便而寫的

λΣ₁₁-dist : {A : Set} {P : A → Set1} {Q : (z : A) → P z → Set1} →
             (∀ z → Σ₁₁ (P z) (Q z)) → Σ₁₁ (∀ z → P z) (λ p → ∀ z → Q z (p z))
λΣ₁₁-dist f = (λ x → proj₁₁₁ (f x)) , (λ x → proj₁₁₂ (f x))
竟然就是 ITT 的 Axiom of Choice!突然從實用情境當中跳出來,嚇死我了 XD。

--
所以我們現在轉向研究 type theory 了嗎?

Labels:

Blogger yen32/14/2009 12:24 pm 說:

我的beamer可以用中文了,哇哈哈哈,這是炫耀文。

你上線後再跟你說~哇哈哈哈

 
Blogger XOO2/14/2009 2:10 pm 說:

> 所以我們現在轉向研究 type theory 了嗎?

應該不是?...

但知道什麼作得到, 什麼作不到應該滿重要的 @"@

 

<< 回到主頁