看板 [ PLT ]
討論串[問題] What does ⊥-elimination do?
共 3 篇文章
內容預覽： 開啟 | 關閉 | 只限未讀
首頁
上一頁
1
下一頁
尾頁
#1
[問題] What does ⊥-elimination do?
推噓3(3推 0噓 3→)留言6則，0人參與, 最新作者suhorng ( )時間11年前 (2013/03/05 22:37), 編輯資訊
2
0
2
內容預覽:
想請問一下, NJ deduction system 中有這條規則. Γ |- ⊥. ---------- (⊥E). Γ |- A. 而對應過去的程式是. Γ |- e : ⊥. -------------------- (⊥E). Γ |- abort(e) : A. 其中 abort 是 Di
(還有1961個字)
#2
Re: [問題] What does ⊥-elimination do?
推噓0(0推 0噓 0→)留言0則，0人參與, 最新作者joshs (Josh Ko)時間11年前 (2013/03/06 02:11), 編輯資訊
0
0
1
內容預覽:
這東西在 Agda 才有完整意義。. 常見的用例是在 case analysis 時排除不可能的情況。. 如果是在 Haskell, 分析出（我們認為）不可能發生的情況時，. 我們會用 error "some complaint", 像. head :: [a] -> a. head [] = er
(還有1558個字)
#3
Re: [問題] What does ⊥-elimination do?
推噓4(4推 0噓 0→)留言4則，0人參與, 最新作者joshs (Josh Ko)時間11年前 (2013/03/06 04:49), 編輯資訊
0
0
0
內容預覽:
應該只有型式上的關聯 — 兩者都是某個 category 下的 initial object:. Empty type ⊥ 是 sets & (total) functions 這個 category 下的 initial object,. 因為從 ⊥ 到任意一個 set 都恰有一個 functio
(還有447個字)
首頁
上一頁
1
下一頁
尾頁