看板
[ PLT ]
討論串[心得] Y Combinator 與 Mutual Recursion
共 6 篇文章
內容預覽:
應該說, 因為我們假設操作的 logic system 包含 ex false quodlibet. 那麼對任何 type, 從 \bot 出發都寫得出 proof term. 不是很確定兩個 \bot 是不是一樣的東西. 確實, 兩者的來源是不同的.. 不過存在任何 context C[] 把兩個
(還有328個字)
內容預覽:
_|_ (\bot) 是任意 type 的 proof term 是甚麼意思呢？. _|_ 應該是對應 logic 上的 false 或稱 absurdity,. 雖然 \bot 也用在 denotational semantics 上, 作為. information order 上"沒有資訊"的
(還有250個字)
內容預覽:
解釋得很棒！真是感謝.... 這個講法不錯（筆記）。. 補充一下，這裡操作上的意思是我們能寫出不會中斷的程式。. 用 untyped lambda calculus 我們能寫出可以一直 reduce 下去，. 不會終止的 term (例如 Y, 和很多其他的). 它的表達能力和 Turing. ma
(還有838個字)
內容預覽:
老實說你的問題真是戳在痛處.. 讀了那麼久 type system 還沒好好想過這個問題. 下面來試著回答看看. 首先先確定一個概念: function 也是 data, 只不過一般的 data type 是 Int. function 的 type 會是 Int -> Int. 因此 value-
(還有3223個字)
內容預覽:
這邊有個疑問. 在Function 裡面定義recursive function 會有問題～. 所以用Y combinator 可以搞定～. 那為什麼. data 層次的recursive 定義不會遇到類似的問題?. 這與haskell的什麼語言特性有關嗎？. 是否有些語言可以支援這樣的宣告，有些卻
(還有257個字)