-
簡單類型λ演算
鎖定
簡單類型 lambda 演算是連接詞只有→(函數類型)的有類型 lambda 演算。這使它成為規範的、在很多方面是最簡單的有類型 lambda 演算的例子。
- 中文名
- 簡單類型λ演算
- 外文名
- Simple Type lambda calculus
- 學 科
- 數學
簡單類型λ演算概念
簡單類型lambda演算是連接詞只有→(函數類型)的有類型lambda演算。這使它成為規範的、在很多方面是最簡單的有類型lambda演算的例子。簡單類型也被用來稱呼對簡單類型 lambda 演算的擴展比如積、陪積或自然數(系統 T)甚至完全的遞歸(如PCF)。相反的,介入了多態類型(如系統F)或依賴類型(如邏輯框架)的系統不被當作是簡單類型。簡單類型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入來嘗試避免無類型 lambda 演算的悖論性使用
[1]
。
簡單類型λ演算類型
簡單類型lambda演算的類型構造自基本類型(或類型變量)α,β,γ,…,給定類型σ,τ我們能構造σ→τ。邱奇只使用了兩個基本類型,o是命題的類型,ι是個體的類型。這種演算經常只有一個基本類型,通常考慮為o。
→是右結合的:我們讀σ→τ→ρ為σ→(τ→ρ)。對每個類型σ我們指派一個數字o(σ),它是σ的階。對於基本類型,我們設置o(α)=0,而對於函數類型我們遞歸的定義o(σ→τ)=max(o(σ)+1,o(τ))。
簡單類型λ演算項
要定義有給定類型的lambda項的集合,我們介入定類型上下文Γ,Δ,…,它們是形如x:σ的類型假定的序列,這裏的x是變量。我們介入判斷Γ⊢t:σ,它意味着t在上下文Γ中是類型σ的項,它們由下列定類型規則給出
[2]
:
換句話説,
1.如果 x 有類型 σ ,我們知道 x 有類型 σ。
2.在特定上下文中,如果 x 有類型 σ ,而我們有某個不是 x 的 y,則 y 有類型 τ 的事實,和上述上下文一起,允許我們推出 x 有類型 σ 。更加清楚的,向上下文增加一個新值不改變現存的值(假定新值不同於以前的值之一)。
3.在特定上下文中,如果 x 有類型 σ,而 t 有類型 τ ,則我們在同一個上下文中,可以構造lambda 抽象 λ x : σ . t ,它有類型 σ → τ 。
4.在特定上下文中,如果 t 有類型 σ → τ ,而 u 有類型 σ,則我們可以構造表達式 t u,它有類型 τ。這捕獲了函數應用的概念。