檢視 型別理論與形式證明筆記 的原始碼
←
型別理論與形式證明筆記
跳至導覽
跳至搜尋
由於下列原因,您沒有權限進行編輯此頁面的動作:
您請求的操作只有這個群組的使用者能使用:
使用者
您可以檢視並複製此頁面的原始碼。
{{Nav|程式語言、邏輯學}} {{isbn|9781107036505}} 原標題:''Type Theory and Formal Proof: An Introduction'' 作者:Rob Nederpelt, Herman Geuvers '''編輯格式注意''' # 章節內文太多的時候,拆成新頁面。 # typst 撰寫 + pandoc 產生貼上於個人維基的內容。 =第1章:無型別lambda運算(untyped lambda calculus)= = 第2章:簡單型別lambda運算(simple typed lambda calculus) = == 2.2 simple type 簡單型別 == 型別變數 type variable:<math display="inline">{\mathbb{V}} = \left\{ \alpha,\beta,\gamma,\ldots \right\}</math>用希臘字母表示。 <math display="inline">\mathbb{T}</math>:所有簡單型別,定義如下: # 型別變數:<math display="inline">\alpha \in {\mathbb{V}} \Rightarrow \alpha \in {\mathbb{T}}</math>,表達基本型別,比如list, nat等 # 箭頭型別:<math display="inline">\alpha,\tau \in {\mathbb{T}} \Rightarrow (\alpha \rightarrow \tau) \in {\mathbb{T}}</math> 箭頭<math display="inline">\rightarrow</math>是右結合的,和函數的apply代入不同。比較<math display="inline">\alpha \rightarrow \beta \rightarrow \gamma = \left( \alpha \rightarrow (\beta \rightarrow \gamma) \right)</math>和<math display="inline">x_{1}x_{2}x_{3} = \left( \left( x_{1}x_{2} \right)x_{3} \right)</math>。 註:在本書中,<math display="inline">\mathbb{N}</math> 和 <math display="inline">\mathbb{L}</math> 指數學世界的自然數和列表,而nat和list指電腦程式世界的同樣的型別。 「term <math display="inline">M</math>有類型(type、型別)<math display="inline">\sigma</math>」寫成<math display="inline">M:\sigma</math> type有唯一性。比如:若<math display="inline">x:\sigma</math>且<math display="inline">x:\tau</math>,則<math display="inline">\sigma \equiv \tau</math> 簡單型別lambda演算的出現的推演規則: # application(代入):若 <math display="inline">M:\sigma \rightarrow \tau</math> 且 <math display="inline">N:\sigma</math>,則 <math display="inline">MN:\tau</math> # abstration(抽象):若 <math display="inline">x:\sigma</math> 且 <math display="inline">M:\tau</math>,則 <math display="inline">\lambda x.M:\sigma \rightarrow \tau</math> <math display="inline">(x\ x)</math>在這種情況下,因為不可能既是<math display="inline">x:\alpha \rightarrow \beta</math>且<math display="inline">x:\alpha</math>這種型別存在,所以這種式子不會被構造到。 若<math display="inline">\exists\sigma\text{ such that }M:\sigma</math>,則<math display="inline">M</math>是可賦予型別的(typable)。 == 2.3 Church-typing (explicit typing) 和 Curry-typing (implicit typing) == # typing à la Church(explicit typing,外顯型別):先給定型別予變數,再推出其他表達式的型別。 # typing à la Curry(implicit typing,隱藏型別):先給定一個表達式,再推論其內變數可能的型別。 explicit typing的案例: 設<math display="inline">M \equiv \left( \left( \lambda x.\lambda y.x \right)(u\ v) \right)</math>,如果<math display="inline">v:\alpha \rightarrow \alpha</math>,<math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta</math>,<math display="inline">x:\beta</math>,<math display="inline">y:\gamma</math>,則<math display="inline">M:\gamma \rightarrow \beta</math> implicit typing的案例(需要用推理和類似合一 (unification) 的方法): <math display="inline">M \equiv \left( \left( \lambda x.\lambda y.x \right)(u\ v) \right)</math>,可以推論: <math display="inline">v:\alpha</math> <math display="inline">u:\alpha \rightarrow \beta</math> <math display="inline">\lambda x.\lambda y.x:\gamma \rightarrow \delta</math> <math display="inline">x:\gamma</math> <math display="inline">\lambda y.x:\delta = \varepsilon \rightarrow \zeta</math> <math display="inline">y:\varepsilon</math> <math display="inline">x:\gamma = \zeta</math> <math display="inline">\lambda y.x:\delta = \varepsilon \rightarrow \gamma</math> <math display="inline">\lambda x.\lambda y.x:\gamma \rightarrow \varepsilon \rightarrow \gamma</math> <math display="inline">(u\ v):\beta = \gamma</math> <math display="inline">u:\alpha \rightarrow \gamma</math> <math display="inline">M:\varepsilon \rightarrow \gamma</math> 但是implicit typing的型別變數,只是一種示例,可以把β用「ω→ω」這種形式取代。 本書常用explicit typing。 我們用上面的explicit typing的範例, <math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha)</math> 可以推論到 <math display="inline">\left( \left( \lambda x.\lambda y.x \right)(u\ v) \right):\beta \rightarrow \gamma</math>, 則可以寫成: 在上下文<math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha)</math>下,<math display="inline">\left( \left( \lambda x: \beta.\lambda y: \gamma.x \right)(u\ v) \right):\gamma \rightarrow \beta</math> 用形式語言的方式寫出來如下: <math display="inline">u:(\alpha \rightarrow \alpha) \rightarrow \beta,v:(\alpha \rightarrow \alpha) \vdash \left( \left( \lambda x: \beta.\lambda y: \gamma.x \right)(u\ v) \right):\gamma \rightarrow \beta</math> === 2.4 Church lambda→演算的推演規則 (derivation rules) === 先賦予型別的lambda term,其名為<math display="inline">\Lambda_{\left\{ {\mathbb{T}} \right\}}</math>,定義如下: <math display="inline">\Lambda_{\mathbb{T}} = V\left| \left( \Lambda_{\mathbb{T}}\ \Lambda_{\mathbb{T}} \right) \right|\left( \lambda V:{\mathbb{T}}.\Lambda_{\mathbb{T}} \right)</math>,其中<math display="inline">V</math>表變數的集合。 '''定義''' # statement形如<math display="inline">M:\sigma</math>,其中<math display="inline">M \in \Lambda_{\mathbb{T}}</math>且<math display="inline">\sigma \in {\mathbb{T}}</math>(<math display="inline">\sigma</math>是型別)。<math display="inline">M</math>稱為主體(subject),<math display="inline">\sigma</math>稱為類型(type)。 # declaration(宣告)是有變數當主體的statement # context(上下文)是一系列不同主體(不同變數)的宣告列表(註:context可為空) # judgement(判斷)形如<math display="inline">\Gamma \vdash M:\sigma</math>,其中左邊的<math display="inline">\Gamma</math>是上下文,右邊的<math display="inline">M:\sigma</math>是statement [[category:資訊]]
此頁面使用了以下模板:
模板:ISBN
(
檢視原始碼
)
模板:Isbn
(
檢視原始碼
)
模板:Nav
(
檢視原始碼
)
返回到「
型別理論與形式證明筆記
」。
導覽選單
個人工具
登入
命名空間
頁面
討論
變體
視圖
閱讀
檢視原始碼
檢視歷史
更多
搜尋
導覽
首頁
愛爾蘭語辭典
近期變更
隨機頁面
有關 MediaWiki 的說明
相關網站
總首頁
Blog
舊 blog
現用 blog 備份
工具
連結至此的頁面
相關變更
特殊頁面
頁面資訊