平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

プログラミング言語、状態と型
Jacques Garrigue
1996 年 8 月

この講義ノートの構成は次の通り。まず、第 1 章ではチューリング機械を定義し、いくつかの例をみる。第 2 章で型なしラムダ計算の定義と性質をみ、第 3 章で前者と後者の同値性を証明する。
さらに第 4 章でラムダ計算に型体系を導入する。

1

チューリング機械

チューリング機械とは、計算機の全ての機能を備える最も単純なモデルである。英国の数学者
A. M. Turing が 1936 年に計算過程の定式化のために定義した。記号が書かれているテープ、それを読むヘッドと制御部の状態という三つ組からできている。テープの長さは無限だが、記号のア
ルファベットと制御部の状態数は有限である、さらにテープの上に書かれている記号の数も各時点では有限である。

...

B B a1 a2 . . . ai ai+1 . . . an B B . . .
A⇒, q
直感的なチューリング機械の動作は三段階になっている。

1. ヘッドの下のテープの値 ai を読む。
2. その値と制御部の状態 q に応じて、新しい値 a0i を同じ場所に書き込み、新しい状態 q 0 に移る。
3. 同様に次の移動方向が決り、書き終わった後、左または右の位置 (i − 1 または i + 1) にヘッドを移す。
このとても単純な機械では、実はコンピュータができる全ての計算が実行できる。
チューリング機械の使う記号、取れる状態、とその状態遷移を正確に定義する。
定義 1 チューリング機械は次の 5 つ組 M = (K, Σ, δ, q0 , H) によって定義される。

K: 空でない有限集合。K の要素を状態という。
Σ: 空でない有限集合 (アルファベット)。Σ の元を記号という。Σ は空白記号 B を含む。
q0 : K の要素で、初期状態という。
H: K の部分集合で、その要素を停止状態という。
δ: (K \ H) × Σ → Σ × { 左, 右 } × K なる関数で、遷移関数という。

1

平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

それでは機械が定義されたが、動的な状態はまだ把握されていない。そのために時点の概念が導入される。
定義 2 あるチューリング機械 M の時点はテープ、位置、状態の 3 つ組で定義される。

t = (T, i, q)
T : Z → K なる関数で、T (n) 6= B であるような n は高々有限個しかない。
i: Z の整数。
q: K の状態。
定義 3 チューリング機械 M が一動作で時点 t から t0 に移ることを t `M t0 と書く。

δ(q, T (i)) = (a, d, q 0 ) ⇒ (T, i, q) `M (T 0 , i0 , q 0 )• T 0 (i) = a, k 6= i ならば T 0 (k) = T (k)• d = 右 ならば i0 = i + 1, d = 左 ならば i0 = i − 1`M の反射推移閉包を `∗M と書く。さらに、q 0 は停止状態ならば、(T, 0, q0 ) `∗M (T 0 , n, q 0 ) を
T .M (T 0 , n, q 0 ) と書き、M を T で実行した結果が (T 0 , n, q 0 ) だという。
例題 1 括弧の対応をチェックする機械。

Σ = {B, E, L, R}
B は空記号、E は消した跡、L は左括弧、R は右括弧
K = {R, L, C, T, F }R は右探索、L は左探索、C は最終チェック、T, F は真と偽
q0 = RH = {T, F }
B
E
L
R
q\a
R
(a, 左, C) (a, 右, R) (a, 右, R) (E, 左, L)δ =L(a, 右, F ) (a, 左, L) (E, 右, R) (a, 右, F )C(a, 右, T ) (a, 左, C) (a, 右, F ) (a, 右, F )例題 2 任意の自然数の加算 a + b = c∑∑
テープの初期状態 (それ以外は B). a = k0 ai · 2i , b = l0 bi · 2ja0 a1 . . . ak M I0 b0 . . . bl
テープの最終状態 (それ以外は B). c =∑mi
0 ci · 2

M c0 c1 . . . cm

2

平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

Σ = {B, 0, 1, M, I0 , I1 }K = {L, R, A0 , A1 , A00 , A01 , A000 , A002 , W0 , W1 , F, T }q0 = R
q\a
B
0
1
M
I0
I1
L
(a, 右, R)(a, 左, L)(a, 左, L)(a, 左, L)R(B, 右, A0 )(B, 右, A1 )(a, 右, F )Ai(i, 左, L)(a, 右, Ai )(a, 右, Ai )(a, 右, Ai ) (a, 右, A0i ) (a, 右, A00i )δ =A0i(I0 , 左, Wi )(I0 , 左, Wi ) (Ii , 左, W1−i )00
Ai (Ii , 左, W1−i ) (Ii , 左, W1−i ) (I1 , 左, Wi )Wi(i, 左, L)(i, 左, L)
0F(a, 左, T )(a, 右, F )(a, 右, F )(a, 右, A0 ) (a, 右, A000 )

2

ラムダ計算

ドイツの論理学者 Schonfinkel が 1920 年代に作ったλ計算は元々論理の証明論のための道具だった。しかし、情報科学との関係がだんだん深くなり、1950 年代からリスプから始まる関数型言語の重要な基礎となった。ラムダ計算自体が機械だとはいえないが、それを用いて様々な計算機械がすぐ導かれる。

2.1(抽象) 項書換系

元々はそうではなかったが、λ計算は項書換系によって定義される。計算を項の一部の書き換えとして見る、ということだ。例えば、数式の書換系を次のように定義できる。
項 (term)

E ::= R | (E + E) | (E − E) | (E × E) | (E/E)

書換規則

x, y は R の実数ならば、(x + y)(x − y)(x × y)
(x/y)

→
→
→
→

x+y
x−y
x×y
x/y

((x + y) は数式だが、 x + y は実数である)
上の規則を簡約規則ともいう。
簡約の例(15 + (1/3)) × (5 − 2) → (15 + 0.3333) × (5 − 2) → (15.3333) × 3 → 46

3

平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

2.2

λ計算の構文 (syntax)

定義 4 λ項 (λ-term) は次の三つの構文からできている。

M

::= x
変数 (variable)| λx.M
抽象 (abstraction)| (M M ) 適用 (application)x は文脈 (環境) で定義されている値 (別のλ項) を指す。
λx.M は項 M の中に使われている変数 x を束縛する。関数として見れば f = λx.M という定義は、普段の f (x) = M 。ただし、λx.M と書くとき、名前をつける必要がないという便利さがある。
(M1 M2 ) は関数の適用である。普段の M1 (M2 ) にあたるが、M1 は名前 (変数) だけでなく、どのλ項でもよい。
上の文法を普段の数式と混ぜると、
f (x) = x + 1 のとき f (2)が 1 回で書ける。

((λx.x + 1) 2)
自由変数と代入 λx.M では、M の中の全ての x の出現は「束縛されている」という。ある項 Mの中で、x が使われながら、束縛されていないのであれば、x は M の自由変数である。M の自由変数の集合 F V (M ) は再起的に次の三条で定義される。

F V (x)= {x}F V (λx.M ) = F V (M ) \ {x}F V (M N ) = F V (M ) ∪ F V (N )代入はそういう自由変数の値を定義する。([N/x]M ) は項 M の中に出現するすべての自由な x
を N と置き換える。
([N/x]x)= N([N/x]y)= y([N/x]λx.M )= λx.M([N/x]λy.M )= λy.([N/x]M )0([N/x](M M )) = (([N/x]M ) ([N/x]M 0 ))4 条目では、y は N の自由変数であってはならない。そのためには、次のα変換が許される。z は
M の自由変数でなければ、
λy.M ↔ λz.([z/y]M )こういう束縛変数の改称は常に許される。

2.3

簡約規則

定義 5 λ項、α変換と次のβ簡約で構成される項書き換え系はλ計算という。

((λx.M ) N ) → ([N/x]M )4

平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

例題 3 簡約の例(λf.λg.λx.f x (g x)) (λx.λy.x) (λx.λy.x)→ λx.((λx.λy.x) x ((λx.λy.x) x))→ λx.((λy.x) (λy.x))→ λx.x(λx.(x x)) (λx.(x x))→ (λx.(x x)) (λx.(x x))→ ...
定理 1 λ計算は合流性を持つ。M → . . . → N と M → . . . → P という二つの簡約があれば、N → . . . → T , P → . . . → T となるような T が存在する。

2.4

λ計算は万能である

全てのプログラムはλ計算で書ける。
整数

チャーチによるエンコーディングがある (Church numeral)。

cn = λf.λx.(f . . . (f x) . . .)f を n 回適用する
c+ = λm.λn.λf.λx.(m f (n f x)) 加算
ブール環

次のエンコーディングを使う。

t = λx.λy.x

f = λx.λy.y

not = λb.λx.λy.(b y x)数の区別も可能で、例えば次の項が引き数に数をもらい、真偽値を返す。

if0 = λn.(n (λx.f) t)
不動点演算子 再起的な関数を定義するのに、不動点演算子 Y が必要になる。その基本的な属性
は、(Y M ) が (M (Y M )) に簡約できることである。

Y = (λf.λx.(x (f f x))) (λf.λx.(x (f f x)))
それによって、引き算なども定義できる。

c− = (Y (λf.λx.λy.(if0 y x (f (p x) (p y)))))s= λn.λf.λx.(f (n f x))
p = λn.(n (λz.(if0 z f (s z))) f)

2.5

評価戦略

ラムダ計算は機械ではない。なぜかといえば、簡約という計算機構があっても、それをどの順番で行うか、あるいはいつ計算が終わるか、が定まっていない。標準形と戦略はちょうどそれを決める役割をはたしている。

5平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

標準形 簡約できる個所を全く残さない (既約) 標準形以外にも、先頭の部分だけが簡約できない
弱冠頭標準形も定義できる。例えば (x ((λy.y) z)) や λx.((λy.y) z) は既約標準形でない (y がまだ簡約できる) が弱冠頭標準形である。形式化すると、λx.M または (x M1 . . . Mn ) のどちらかの形をしたものが弱冠頭標準形である。
最左戦略 最も左にある簡約できる個所を先に簡約する。名前呼び出し (call-by-name) に当る。関数の引数を評価せずに、そのまま代入する。(λx.x) ((λy.y) z) → ((λy.y) z)。ある戦略で M →∗ N (N標準形) のとき、最左戦略でも M →∗ N 。
最右最内戦略 最も右にある簡約できる個所の中で、最も中にあるものを選ぶ。値呼び出し (callby-value) に当る。関数の引数を標準形に落してから代入する。(λx.x) ((λy.y) z) → ((λx.x) z)。
ある戦略で M →∗ . . .(無限に続く簡約) のとき、最右最内戦略でも無限な簡約になる。
機械 標準形 (停止状態) と戦略 (遷移関数) の組み合わせを選ぶと、任意のλ項を決定的な機械としてみることができる。

3

チューリング機械とラムダ計算の同値性

3.1

チューリング機械をλ項に対とリスト構造 二つの値を一つの項で表現する時、対という形にする。(a1 , a2 ) = λf.(f a1 a2 )。
適当な関数を使うと、各要素が抽出できる。例えば (a1 , a2 )(λx.λy.x) = a1 。便宜のために f st =λp.(p (λx.λy.x)) と snd = λp.(p (λx.λy.y)) を定義する。同様に n 組が作れる。(a1 , . . . an ) =λf.(f a1 . . . an ).
規則性のある無限なデータ構造を無限リストとして表現できる。[a1 , a2 , . . .] は (a1 , [a2 , a3 , . . .])= λf.(f a1 [a2 , a3 , . . .n ]) になる。このままでは無限なλ項になり、計算に使えないが、規則性があれば Y を使って有限なλ項が作れる。
状態と記号 M = (K, Σ, q0 , H, δ), |K| = k, |Σ| = l とする。各状態と記号に番号をふっておき、K = {q0 , . . . , qk−1 }, Σ = {σ0 = B, . . . , σl−1 }。次の翻訳を定義する。

qi = λx0 . . . xk−1 .xi
σi = λx0 . . . xl−1 .xi
時点

時点 (T, n, q) を

(q, T (n), [T (n − 1), T (n − 2), . . .], [T (n + 1), T (n + 2), . . .])の 4 つ組で表す。無限リストを使うことになるが、B でしか構成されていない末端の部分を Y を使って表現する。[B, . . .] = Y (λy.(B, y)) →∗ (B, Y (λy.(B, y))) →∗ . . .
遷移関数

ある時点から次の時点への遷移関数を関数の l 組の k 組で表す。

∆ = λt.t((δ(q0 , σ0 ), δ(q0 , σ1 ), . . . , δ(q0 , σl−1 )), . . . , (δ(qk−1 , σ0 ), . . .))6

平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

00

 λtl .λtr .f (q , f st tl , snd tl , (σ , tr ))when δ(q, σ) = (σ 0 , 左, q 0 )δ(q, σ) =λtl .λtr .f (q 0 , f st tr , (σ 0 , tl ), snd tr ) when δ(q, σ) = (σ 0 , 右, q 0 )
λtl .λtr .(q, σ, tl , tr )when q ∈ H
この中の f を恒等関数 λx.x と定めると、抽象的に見る ∆ の型は (K, Σ, Σ list, Σ list) →(K, Σ, Σ list, Σ list) であり、時点から時点への遷移関数に対応している。
実行∆ は 1 回分の動作しか行わないので、その不動点を取ればよい。そのために f を抽象化する。
λf.∆ : ((K, Σ, Σ list, Σ list) → (K, Σ, Σ list, Σ list)) →((K, Σ, Σ list, Σ list) → (K, Σ, Σ list, Σ list))(Y (λf.∆)) : (K, Σ, Σ list, Σ list) → (K, Σ, Σ list, Σ list)

それを初期状態に適用すると、T . (T 0 , n, q 0 ) が算出される。しかし無限リストを使っているので、既約標準形まで計算すると止らない。弱冠頭標準形では正しい結果が得られる。

(Y (λf.∆)) (q0 , T (0), [T (−1), . . .], [T (1), . . .]) →∗(q 0 , T 0 (n), [T 0 (n − 1), . . .], [T 0 (n + 1), . . .])3.2

λ項を実行できるチューリング機械

この節の目的はλ項をテープに書き、実行することである。
テープを実行するチューリング機械を考える前に、λ項を実行しやすい形でテープに書き込まなければならない。特に変数名とα変換は省きたい。そのために De Bruijn 添数を導入する。
定義 6 De Bruijn 添数

変数名を使わないラムダ計算を定義する。

M ::= n | λM | (M M )添数はこの変数が何番目の抽象 (中から数えて) で束縛されたかを表す。例えば λx.λy.x = λλ2,
λx.(x x) = λ(1 1)。代入を新しく定義する。

⇑n k
⇑n k
⇑n λM

= k+1
k≥n
= k
k<n
= λ(⇑n+1 M )β 簡約

λM N → [N/1]M[N/n]n[N/n]k[N/n]k[N/n]λM[N/n](M M 0 )

=
=
=
=
=

N
k−1
k>n
k
k<n
λ([⇑n N/n + 1]M )([N/n]M [N/n]M 0 )例題 4 対から 1 つ目の値を出す。

f st λ(1 a b) = λ(1 λλ2) λ(1 a b) → λ(1 a b) λλ2 → λλ2 a b → λa b → a
テープの形式5 つの記号 {0, 1, E, λ, @} を使い、テープへの変換 M を定義する。
n = (n の 2 進法記述) E
λM = λ M(M M 0 ) = @ M M 07平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

チューリング機械 Λ 上のテープを実行する機械 Λ はここで定義しないが、加算等の簡単な動作でできるので、そういうチューリング機械の存在は明かであろう。ここで弱冠頭標準形を最左戦
略で計算する。

3.3

万能チューリング機械

任意のチューリング機械をλ項で表現できる、任意のλ項はある特定のチューリング機械が実行するテープに変換できる。そういう二つの定理に面白い系がある。
系 1 任意のチューリング機械を模擬できる万能チューリング機械が存在する。その機械は模擬する機械の定義をテープで与えられ、それを実行する。
証明 模擬したいチューリング機械をλ項に変換し、それを Λ に与えればよい。

型付きλ計算4上の関数は数学的関数と違い、定義域と値域を定めていない。例えば、c+ は整数以外の物に適用しても意味がないが、そのような項は正しくないと判断できない。

4.1型 (type) と項型付きλ計算では、そのような領域を型で表す。単純な計算系では全ての値は一つだけの型に属する。型には二種類があり、基底型と関数・構造型に分けられる。

b ::= int | bool | . . .
t ::= b | t → t | t × t
項の中にも、型情報を入れ、定数も追加する。

M ::= x | ct | λx:t.M | (M M ) | (M, M )簡約規則には、βに加えて定数に関するδ規則も導入される。

(λx:τ.M ) N(fstτ ×θ→τ (M, N ))(sndτ ×θ→θ (M, N ))(addint→int→int mint nint )
...

4.2

→
→
→
→

[N/x]MM
N(m + n)int

型推論

ある項の正しさ (well-formedness) を型判定式で表す。

Γ`M :τ
M は項であり、τ は型である。そして Γ は型宣言列と呼ばれる変数名と型の集合 (x1 : τ1 , . . . ,xn : τn )。

8

平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

定義 7 次の型推論規則で型判定式が証明された項を正しいとする。
変数 Γ ` x : τ (x : τ はΓに含まれる)
定数 Γ ` cτ : τ

例題 5

抽象

Γ, x : θ ` M : τΓ ` λx:θ.M : τ適用Γ`M :θ→τ Γ`N :θΓ ` (M N ) : τ

直積Γ`M :τ Γ`N :θΓ ` (M, N ) : τ × θ

証明

x : int ` sint→int : int → int x : int ` x : int
x : int ` (sint→int x) : int` 1int : int` λx:int.(sint→int x) : int → int` ((λx:int.(sint→int x)) 1int ) : int

4.3

属性

次の定理は fst, snd 以外のδ規則を含まない計算系に関するものである。
定理 2 (主部簡約) Γ ` M : τ と M → N が成り立てば、Γ ` N : τ が成り立つ。
定理 3 (強正規化) Γ ` M : τ ならば、無限な簡約列 (M → M1 → M2 → . . .) は存在しない。

4.4

状態の導入

値呼び出し戦略 各関数がどの順番で評価されるかが分かるので、状態をどこでも変えられるよ
うにしてもいい。動的に状態の大きさを増やしてもいい。

newref τ →ref(τ ) M
deref ref(τ )→τ r
setref ref(τ )→τ →unit r M
例

→ r
→ M
→ ()

空いている位置 r に値 M を書き込む
位置 r から値 M を読む
位置 r に値 M を書き込む

f (n) を呼ぶと、r の中身に n が足され、新しい値が返される。
r : ref(int) = newref 0f : int → int = λx.((λy.((λz.y) (setref r y))) (add (deref r) x))

特定の評価戦略を仮定しない場合 状態を引数としてとり、結果と一緒に返す。もともと f : θ → τなる関数があり、その関数の中で状態を変える必要があれば、実際には f : θ → σ → (τ × σ) という型になる (σ は状態全体の型)。このままでは使いにくいので、λ計算を拡張する。
まず σ → (τ × σ) = ST (τ ) と略する。そして、この ST (τ ) を扱う関数を定義する。ここではσ = σ1 × . . . × σn9

平成8年度(第18回)数学入門公開講座テキスト(京都大学数理解析研究所，平成8年8月5日～8月9日開催)

getiST (σi ) (s1 , . . . , sn )setiσi →ST (unit) M (s1 , . . . , sn )thenST (θ)→(θ→ST (τ ))→ST (τ ) M N s
returnτ →ST (τ ) M s

→
→
→
→

(si , (s1 , . . . , sn ))((), (s1 , . . . , si−1 , x, si+1 , . . . , sn ))(λp.(N (fst p) (snd p))) (M s)(M, s)

この方法は圏論のモナドによるものである。
例

同上s : int × bool × int = (0, t, 0)
f : int → ST (int) = λx.(then get3 (λy.then (set3 (add x y)) (λz.get3)))

参考文献[1] 有川節夫. オートマトンと計算可能性, 情報処理シリーズ, 第 9 巻. 培風館, 1986.
[2] Eugenio Moggi. Notions of computation and monads. Information and Computation, Vol. 93,
pp. 55–92, 1991.
[3] 横内寛文. プログラム意味論, 情報数学講座, 第 7 巻. 共立出版, 1994.

10