2,617
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
無編輯摘要
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 130： | 行 130： | ||
注意上面的符號，逗號,表示連結上下文。上下文<math>\Gamma</math>可以為空。 | 注意上面的符號，逗號,表示連結上下文。上下文<math>\Gamma</math>可以為空。 | ||
推論可以由上到下讀，或是下到上讀推到目標。 | |||
推論不只是建構judgement，更是一種justify的方式。 | |||
1.變數沒有前提，只有conclusion，可以用在推演開頭，意思是在上下文內的變數可以從這個上下文推演出來。 | 1.變數沒有前提，只有conclusion，可以用在推演開頭，意思是在上下文內的變數可以從這個上下文推演出來。 | ||
| 行 147： | 行 151： | ||
} | } | ||
</math> | </math> | ||
;比較數學和邏輯學： | |||
1. 數學： | |||
<math> (func-appl)\cfrac{f : A \rightarrow B and ~c \in A}{f(c)\in B}</math> | |||
<math> (func-abst)\cfrac{\forall x \in A, f(x)~\in~B}{f:~A\rightarrow B}</math> | |||
2. 邏輯學： | |||
*(⇒-elim 消去)<math display="inline">\cfrac{A \Rightarrow B\quad A}{B}</math> | |||
*(⇒-intro 引入)（參考附錄的表記法） | |||
<pre> | |||
*Assume : A* | |||
| ... | |||
| B | |||
------ | |||
A⇒B | |||
</pre> | |||
旗標flag（本筆記用雙星號**夾起來的地方表示變數定義或assumption假設） | |||
旗杆（本筆記用串聯的豎線|標記）表示定義假設的範圍(scope)。 | |||
若∃上下文Γ, ∃型別ρ s.t.(such that) Γ⊢M:ρ（且M是pre-typed），則M是legal。 | |||
=附註：本筆記使用的邏輯推演排版法= | =附註：本筆記使用的邏輯推演排版法= | ||