「型別理論與形式證明筆記」修訂間的差異

跳至導覽 跳至搜尋

型別理論與形式證明筆記 (檢視原始碼)

於 2024年7月30日 (二) 00:41 的修訂

增加 2,483 位元組 、 2024年7月30日 (二) 00:41
無編輯摘要
行 180： 行 180：


若∃上下文Γ, ∃型別ρ s.t.(such that) Γ⊢M:ρ（且M是pre-typed），則M是legal。
若∃上下文Γ, ∃型別ρ s.t.(such that) Γ⊢M:ρ（且M是pre-typed），則M是legal。
== 2.5 不同的推演格式 ==
型別推論如natural deduction是樹狀。
但是推演過程會發散，使讀者無法專注其中。
linear format 比較可以省略，如下：
<pre>
(1) y:α→β, z:α⊢y:α→β
(2) y:α→β, z:α⊢z:α
(3) y:α→β, z:α⊢y z:β
(4) y:α→β⊢λ z :α. (y z):α→β
(5) y:α→β⊢λ y:α→β. λ z :α.(y z):(α→β)→(α→β)
</pre>
排序有時不一定照順序也可。
judgement之間的相依性，是一個嚴格偏序(strict partial order)關係：
* 非自反性 irreflexive：J ⇏ J
* 非對稱性 asymmetric：(J1 ⇒ J2) ⇏ (J2⇒ J1)
* 遞移性 transitive：(J1 ⇒ J2) ∧ (J2 ⇒ J3) ⇒ (J1 ⇒ J3)
可是還會出現一堆重複的上下文。所以就用 flag format 的標記法（類似Fitcher式），見[[#附註：本筆記使用的邏輯推演排版法|附註]]
==2.6 型別論要解決的問題==
# well-typedness (viz Ch 2.7) aka typability
#* ? ⊢term:? #找到一個上下文和type，使term legal。
#** 型別指派是變體：context ⊢term:?，推得term型別，aka inhabitation（term construction)
#* 型別檢查：「context ⊢term:type」是否能推導出？
#* 尋找term：context ⊢?:type，找到符合type的term。
這些問題在lambda→係可決定的，有演算法可以產出，但更後面的系統的term finding，是無固定演算法且非決定型別。
==2.7 well-typedness 於lambda→==
找上下文和term的type，範例：
M = λ y:α→β. λ z :α.(y z):？，求型別和上下文。
因為這裡沒有自由變數，所以可以假設上下文是∅。
所以我們可以找上下文。
因為有引入y 和z，所以：
<pre>
*y : α → β*
| ??
| λ z :α.(y z):??
λ y:α→β. λ z :α.(y z):？
</pre>
接續
<pre>
*y : α → β*
| *z : α*
| | ??
| | (y z):??
| | λ z :α.(y z):??
λ y:α→β. λ z :α.(y z):？
</pre>
接續
<pre>
*y : α → β*
| *z : α*
| | (y z):β
| | λ z :α.(y z):??
λ y:α→β. λ z :α.(y z):？
</pre>
接續
<pre>
*y : α → β*
| *z : α*
| | (y z):β
| | λ z :α.(y z):α→β
λ y:α→β. λ z :α.(y z):(α→β)→(α→β)
</pre>
所以可以得知型別。
但是若是z是β，則無法得知其型別，換言之，是illegal的。這種well-typedness推論有不同的推論方法。


=附註：本筆記使用的邏輯推演排版法=
=附註：本筆記使用的邏輯推演排版法=
行 224： 行 305：


</pre>
</pre>
書中把變數引入(var)省略，所以變成：
<pre>
*y : α → β*
| *z : α*
| | y z: β
| λz.(y z): α → β
λy.λz.(y z): (α → β) → α → β
</pre>
[[category:資訊]]
[[category:資訊]]
[[分類:邏輯學]]
取自「https://kianting.info/wiki/w/特殊:手機版差異/2777」

導覽選單