→ recorriendo :的書有滿完整的說明 可以看到type理論可以很複雜 04/18 15:05
→ recorriendo :recursive type有套告理論 polymorphic type又有一套 04/18 15:05
→ recorriendo :理論 04/18 15:06
→ t0444564 :這串文或許可以加入精華區了XD 04/19 02:13
※ 引述《yueayase (scrya)》之銘言：
: 看了以上的討論, 我不知道type theory和邏輯符號語言之間的差別
type就是把變數分類 像程式語言裡把變數分成int, boolean一樣
標準的數理邏輯裡變數沒有分類
不過也有分類變數的理論 一般通稱做many-sorted logic
沒有type的理論只需要一個universe
有type的理論則每一個基本type都要有一個universe
然後因為還要定義product type, function type等等
所以大部分都還需引入category theory來處理
現在數學基礎的典範是集合論 是一個沒有type的理論
因此只有一個set theoretic universe
而自然數, 實數, ordinal number... 都可以定義成這個universe內的object
當然不認同這個數學基礎的大有人在...
: 因為我也曾經看過像logic set and recursion(http://ppt.cc/PatL)之類的書
: 裡面主要就是在說邏輯符號系統的language structure是怎樣
: 怎樣去interpret這些language意思
: 像之前提到的 A Mathematical Introduction to Logic也是在說這些東西
: 就不是很清楚type theory和這類書籍所說的有什麼差別
: 附帶一提,
: 這些東西又好像和computer science 的 formal language(eg: context-free grammar)
有關係 像語言學裡名詞 動詞 句子等都是一個type
不過搞context-free grammar的人比較喜歡叫他們part-of-speech
categorial grammar (一種更接近數理邏輯的文法) 則多稱之為type
: 或是 computation theory(eg: Turing machine <=> λ-calculus, decidability...)
這裡的確有些有趣的定理
例如 untyped lambda calculus 和 Turing machine 等價
(能計算所有computable function)
Typed lambda calculus 不能計算所有 computable function
但加入 fixed point operator 或允許 recursive type
就跟Turing machine等價了~
有興趣的話找本 programming language theory 的書都會有寫
: 有一些關聯
: 的確, 聽說作Artificial Intelligence的人, 早期好像也在研究logic...
嘖嘖 後來有所謂AI winter 所以現在AI已經不搞邏輯了...
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 128.12.24.136
※ 編輯: recorriendo 來自: 128.12.24.136 (04/18 14:40)
※ 編輯: recorriendo 來自: 128.12.24.136 (04/18 14:46)