「型別理論與形式證明筆記」修訂間的差異
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 25： | 行 25： | ||
箭頭<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">\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">(xx)</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)。 | |||
[[category:資訊]] | [[category:資訊]] | ||
於 2024年7月8日 (一) 22:05 的修訂
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：解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle {\mathbb{V}} = \left\{ \alpha,\beta,\gamma,\ldots \right\}} 用希臘字母表示。
解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \mathbb{T}} ：所有簡單型別，定義如下：
- 型別變數：解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \alpha \in {\mathbb{V}} \Rightarrow \alpha \in {\mathbb{T}}} ，表達基本型別，比如list, nat等
- 箭頭型別：解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \alpha,\tau \in {\mathbb{T}} \Rightarrow (\alpha \rightarrow \tau) \in {\mathbb{T}}}
箭頭解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \rightarrow} 是右結合的，和函數的apply代入不同。比較解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \alpha \rightarrow \beta \rightarrow \gamma = \left( \alpha \rightarrow (\beta \rightarrow \gamma) \right)} 和解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x_{1}x_{2}x_{3} = \left( \left( x_{1}x_{2} \right)x_{3} \right)} 。
註：在本書中，解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \mathbb{N}} 和 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \mathbb{L}} 指數學世界的自然數和列表，而nat和list指電腦程式世界的同樣的型別。
「term 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M} 有類型（type、型別）解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \sigma} 」寫成解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M:\sigma}
type有唯一性。比如：若解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\sigma} 且解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\tau} ，則解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \sigma \equiv \tau}
簡單型別lambda演算的出現的推演規則：
- application（代入）：若 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M:\sigma \rightarrow \tau} 且 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle N:\sigma} ，則 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle MN:\tau}
- abstration（抽象）：若 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\sigma} 且 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M:\tau} ，則 解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \lambda x.M:\sigma \rightarrow \tau}
解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle (xx)} 在這種情況下，因為不可能既是解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\alpha \rightarrow \beta} 且解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle x:\alpha} 這種型別存在，所以這種式子不會被構造到。
若解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle \exists\sigma\text{ such that }M:\sigma} ，則解析失敗 (MathML 使用 SVG 或 PNG 備用 (建議用於現代瀏覽器與輔助工具)：從伺服器 "https://wikimedia.org/api/rest_v1/" 收到無效的回應 ("Math extension cannot connect to Restbase.")。): {\textstyle M} 是可賦予型別的(typable)。