標籤：

Lambda演算求值策略類型系統

你好，類型（六）：Simply typed lambda calculus

05-23

你好，類型（六）：Simply typed lambda calculus

來自專欄業餘程序員的個人修養

簡單類型化 $lambda$ 演算（simply typed lambda calculus） $lambda^ o$ ，是無類型 $lambda$ 演算的類型化版本，

它是眾多類型化 $lambda$ 演算中最簡單的一個。

它只包含一個類型構造器（type constructor） $o$ ，

即，接受兩個類型 $T_1,T_2$ 作為參數，返回一個函數類型 $T_1 o T_2$ 。

下文中，我們首先從最基礎的概念說起，詳細的區分項（term）和值（value）的概念，

然後介紹簡單類型化 $lambda$ 演算系統的求值規則和類型規則。

1. 項和值

1.1 項

項（term）是一個語法概念，一個合法的項，指的是一段符合語法的字元串。

例如，在 $lambda_eta$ 系統中，項的定義如下，

$t::=x|lambda x.t|t~t$

它表明，一個合法的 $lambda_eta$ 項，要麼是一個變數 $x$ ，

要麼是一個 $lambda$ 抽象（abstraction） $lambda x.t$ ，要麼是一個 $lambda$ 應用（application） $t~t$ 。

1.2 值

值（value）是一個和語義相關的概念，有三種常用的方法為項指定語義。

（1）操作語義，通過定義一個簡單的抽象機器，來說明一個程序語言的行為。

（2）指稱語義，一個項的語義是一個數學對象。

（3）公理語義，不是首先定義程序的行為，而是用項所滿足的規則限定它的語義。

下面我們採用操作語義的方法，來定義求值的概念。

首先，我們人為指定項的一個子集，將其中的元素稱為值。

假如項的定義如下， $t::=true|false|if~t~then~t~else~t$ ，

我們可以定義值， $v::=true|false$ 。

值可能是項被求值的最終結果，但也不全是，因為對某些項的求值過程可能不會終止。

1.3 求值規則

求值規則，是定義在項上的推導規則，例如，

（1） $if~true~then~t_1~else~t_2 o t_1$ ，

（2） $if~false~then~t_1~else~t_2 o t_2$ ，

（3） $frac{t_1 o t_1}{if~t_1~then~t_2~else~t_3 o if~t_1~then~t_2~else~t_3}$

其中， $x o y$ 表示，項 $x$ 可以一步求值為項 $y$ 。

1.4 範式

一個不含自由變數的項，稱為封閉項，封閉項也稱為組合子。

例如，恆等函數 $id=lambda x.x$ 就是一個封閉項。

如果沒有求值規則可用於項 $t$ ，就稱該項是一個範式。

範式可能是一個值，也可能不是，但每一個值都應該是範式。

如果一個封閉項是一個範式，但不是一個值，就稱該項受阻。

不是值的範式，在運行時間錯誤分析中起著極其重要的作用。

2. 類型

2.1 類型上下文

一個類型上下文（也稱類型環境） $Gamma$ ，是一個變數和類型之間綁定關係的集合。

空上下文，可以記為 $varnothing$ ，但是我們經常省略它。

用逗號可以在 $Gamma$ 右邊加入一個新的綁定，例如， $Gamma,x:T$ 。

$vdash t:T$ ，表示項 $t$ 在空的類型上下文中，有類型 $T$ 。

2.1 類型規則

$lambda^ o$ 是一個新的系統，比起 $lambda_eta$ 而言，增加了一些基於類型的推導規則。

其中， $lambda^ o$ 中 $lambda$ 項的語法如下：

（1） $t::=x|lambda x:T.t|t~t$

（2） $T::=T o T$

（3） $Gamma::=varnothing|Gamma,x:T$

推導規則：

（1） $frac{x:TinGamma}{Gammavdash x:T}$

（2） $frac{Gamma,x:T_1vdash t:T_2}{Gammavdashlambda x:T_1.t:T_1 o T_2}$

（3） $frac{Gammavdash t_1:T_1 o T_2~~~~Gammavdash t_2:T_1}{Gammavdash t_1~t_2:T_2}$

根據以上的推導規則，我們可以證明， $vdash(lambda x:Bool.x)~true:Bool$

2.3 求值規則

$lambda^ o$ 系統中，值的定義如下：

（1） $v::=lambda x:T.t$

求值規則，定義如下：

（1） $frac{t_1 o t_1}{t_1~t_2 o t_1~t_2}$

（2） $frac{t_2 o t_2}{t_1~t_2 o t_1~t_2}$

（3） $(lambda x:T.t)~v o [xmapsto v]t$

其中（2），相當於 $eta$ 變換，

$[xmapsto v]t$ ，表示將 $t$ 中所有自由出現的 $x$ 換為 $v$ 。

2.4 Curry-style and Church-style

對於 $lambda^ o$ 系統來說，通常有兩種不同風格的解釋方式，

如果我們首先定義項，然後定義項的求值規則——語義，

最後再定義一個類型系統，用以排除掉我們不需要的項，

這種語義先於類型的定義方式，稱為Curry-style。

另一方面，如果我們定義項，然後再給出良類型的定義，

最後再給出這些良類型項的語義，就稱為Church-style，類型先於語義，

在Church-style的系統中，我們不關心不良類型項的語義。

歷史上，隱式類型的 $lambda$ 演算系統，通常是Curry-style的，

而顯式類型的 $lambda$ 演算系統，通常是Church-style的。

3. 關於單位類型

簡單類型化 $lambda$ 演算，直接用起來可能並不好用，

人們會再為它擴充一些類型，例如，添加一些基本類型 $Bool$ ， $Nat$ 或者 $String$ ，

定義單位類型，列表類型，元組類型，和類型，等等。

下面我們選擇單位類型進行介紹。

滿足單位類型的項只有一個，為此我們新增一個項的定義，

$t::=...|unit$

再新增一個類型的定義，

$T::=Unit$

以及一個推導規則，

$Gammavdash unit:Unit$

$Unit$ 的作用類似於C和Java中的 $void$ 類型，主要用於表示副作用，

在這樣的語言中，我們往往並不關心表達式的結果，而只關心它的副作用，

因此，用 $Unit$ 來表示結果的類型，是一個合適的選擇。

這裡提到單位類型，是為以後Top類型和Bot類型做鋪墊。

參考

Wikipedia: Simply typed lambda calculus

類型和程序設計語言

下一篇：你好，類型（七）：Recursive type

推薦閱讀：

※語言背後的代數學（十）：Curry-Howard-Lambek correspondance
※柯里化的前生今世（十）：類型和類型系統
※Hacklang的類型系統規格

TAG:Lambda演算 | 類型系統 | 求值策略 |