A2 簡單類型λ演算

簡單類型 λ 演算

簡單類型 λ 演算（λ→）是僅使用「→」（函式類型）作為連接詞的一種有類型 λ 演算。它是一個簡單且規範的有類型 λ 演算範例，並且在多方面是最簡單的形式。簡單類型也可以用來指稱對簡單類型 λ 演算的擴充，例如積、陪積、自然數系統（系統 T）或完全遞歸（如 PCF）等。相比之下，包含多型類型（如系統 F）或依值型別（如邏輯框架）的系統則不屬於簡單類型範疇。簡單類型 λ 演算最初由阿隆佐·邱奇於1940年提出，目的是為了避免無類型 λ 演算中的悖論性問題。

類型

簡單類型 λ 演算的類型由基本類型（或類型變數）如 α、β、γ 等構成。在這些類型的基礎上，若已知兩個類型 σ 和 τ，我們可以構造新的類型 σ → τ。邱奇的系統最初只使用了兩個基本類型：o 代表命題類型，ι 代表個體類型。這些類型中，o 最常被視為唯一的基本類型。

在簡單類型中，「→」是右結合的：例如，σ → τ → ρ 會被解析為 σ → (τ → ρ)。每個類型 σ 會被賦予一個階數 o(σ)，其定義為：

• 基本類型的階數為 0（o(α) = 0）。
• 函式類型的階數為其參數類型和返回類型階數的最大值加一，即 o(σ → τ) = max(o(σ) + 1, o(τ))。

項

為了定義具有指定類型的 λ 項，我們引入了類型上下文，如 Γ、Δ 等，這些上下文包含形式為 x : σ 的類型假定，其中 x 是變數。根據這些上下文，我們可以推導出某個 λ 項 t 的類型為 σ，記作 Γ ⊢ t : σ。以下是簡單類型 λ 演算中的一些基本規則：

1. 變數規則：

   • 若 x : σ 屬於上下文 Γ，則可以推導出 x : σ。

2. 變數替代規則：

   • 如果 x : σ 是上下文 Γ 中的條目，且 x ≠ y，則在新的上下文 Γ, y : τ 中，我們仍然可以推導出 x : σ。

3. 抽象規則：

   • 如果在上下文 Γ 中，已知 x : σ 且 t : τ，則可以推導出 λx:σ.t : σ → τ。

4. 應用規則：

   • 如果在上下文 Γ 中，已知 t : σ → τ 和 u : σ，則可以推導出 t u : τ。

這些規則定義了如何在 λ 演算中處理變數、抽象函式和函式應用。以下是一些閉合項的範例：

• λx:α.x : α → α
• λx:α.λy:β.x : α → β → α
• λx:α → β → γ.λy:α → β.λz:α.xz(yz) : (α → β → γ) → (α → β) → α → γ

這些閉合項展示了 λ 演算中如何使用抽象和應用來構建函式，並且它們在組合子邏輯中扮演著重要角色。

βη-等價

簡單類型 λ 演算中的項可通過 βη-等價來辨識。β-等價表示當 λ 項應用於一個參數時，會按照右邊的項進行替換。而 η-等價則指如果 x 在 t 中不自由出現，則 λx:σ.t x 與 t 是等價的。

簡單類型 λ 演算在 Curry-Howard 同構中與直覺邏輯（極小邏輯）密切相關。在這個同構中，閉合項的類型對應於極小邏輯中的重言式。

重要成果

1967年，Tait 證明了 β-歸約是強規格化的，這意味著 βη-等價是可判定的。Statman 在1977年證明規格化問題不是基本遞迴的，而 Berger 和 Schwichtenberg 在1991年則證明了純語意規格化的結果。此外，βη-等價的合一問題已被證明是不可判定的。

這些理論成果推動了 λ 演算在數學邏輯和計算機科學中的應用，並且為後來的語言設計和理論計算領域提供了基礎。