1 型なしラムダ計算

集中講義ハンドアウトおよびレポート課題 

（ 2015 _年 12 _月 15 _日 – 12 _月 18 _{日、東北大学）}

京都大学数理解析研究所 照井一成 [email protected]

最終更新：2015年12月23日

更新履歴

• ^{「優」確定に必要な}⋆の数を8つから7つに変更。

1 型なしラムダ計算

1.1 定義

ラムダ項. 変数の可算集合Varが与えられているとする。ラムダ項を次の文法で定義する。

M, N ::= x |(λx.M) |(M N).

ただしx∈Var. (λx.M)をラムダ抽象といい、(M N)を適用という。ラムダ項全体の集合 をTermと書く。

かっこは適宜省略する。また、

λx₁· · ·x_n.M ≡ (λx₁.· · ·(λx_n−1.(λx_n.M))· · ·) M N₁· · ·N_n ≡ (· · ·((M N₁)N₂)· · ·N_n)

とする。

ラムダ項λx.Mにおいて、λxはMの中に現れるxを束縛する。どのようなλxにも束 縛されない変数を自由変数という。Mに含まれる自由変数の集合をfv(M)と書く。自由 変数を含まないラムダ項を閉項という。

項の代入. ラムダ項M の中に現れる自由変数xに注目するときには、M[x]のように書 く。そしてM[x]^{の中に現れる自由変数}x^{の出現全てに}Nを代入して得られるラムダ項を M[N]またはM[N/x]と書く。

α規約. 束縛変数の名前は、束縛関係を変えない限り自由に付け替えてよい。それゆえ λx.M[x]とλy.M[y]は同じラムダ項を表す。

変数規約. ラムダ項をラムダ項に代入するときには、新たな束縛関係が生じないよう、

束縛変数の名前を付け替えてから代入する。ゆえにM[y] ≡ (λx.xy)のときM[(xz)]は

(λx.x(xz))ではない。そうではなく、束縛変数xをwと名前変えし、M[y]≡(λw.wy)と

した上で、M[(xz)]≡(λw.w(xz))とする。

β簡約 2項関係→β⊆Term²を次のように定義する。

(λx.M[x])N →β M[N]

M →β N λx.M →β λx.N M →β N

KM →β KN

M →β N M K→β N K

(λx.M[x])N ^{の形のラムダ項を}β^{基という。}

例.

(λx.x(xy))(λz.wz) →β (λz.wz)((λz.wz)y) →β (λz.wz)(wy) →β w(wy).

関係→βを含む最小の前順序（反射的推移的関係）を→^∗_β^{とかく。また、関係}→βを含 む最小の同値関係を=_βとかく。それ以上β簡約できないラムダ項（つまり(→β)⁻¹極小 元）を正規形という。とくにM →^∗_β N でNがそれ以上β簡約できないとき、N のこと をMの正規形という。与えられたラムダ項の正規形を求めることを正規化という。

上の例により、(λx.x(xy))(λz.wz) →^∗_β w(wy)^{であり、また}w((λz.wz)y) =β (λz.wz)(wy) である。w(wy)は正規形である。

1.2 ラムダ項を用いた関数表現

恒等関数・関数合成.

id:=λz.z, M₁◦M₂:=λz.M₁(M₂z), M₁◦ · · · ◦Mn:=λz.M₁(M₂· · ·(Mnz)· · ·) ただしz^はM1, . . . , Mnの中には現れない新しい変数とする。次が成り立つ。

idM →β M (M₁◦M₂)N →β M₁(M₂N) (M₁◦M₂)◦M₃ →β M₁◦M₂◦M₃ M₁◦(M₂◦M₃) →β M₁◦M₂◦M₃ ブール値・ブール関数.

true := λxy.x false := λxy.y

neg := λbxy.byx conj := λb₁b₂xy.b₁(b₂xy)y 次のことに注意する。

neg≡λb.λx.λy.(by)x, true≡λx^′.λy^′.x^′ すると

neg true→β λx.λy.((λx^′.λy^′.x^′)y)x→β λx.λy.(λy^′.y)x→β λx.λy.y≡false.

同様にしてneg false→β∗ trueも言える。

順序対・条件文.

hM1, M₂i:=λz.zM₁M₂, proj₁M :=Mtrue, proj₂M :=Mfalse.

ただしz6∈fv(M1)∪fv(M2). ^{このようにすれば}

proj₁hM1, M₂i →^∗_β M₁, proj₂hM1, M₂i →^∗_β M₂ となる。また、

ifN thenM1 elseM2 := N M1M2

と定義すれば、

if true thenM₁ elseM₂ →^∗_β M₁, if false thenM₁ elseM₂ →^∗_β M₂ が成り立つ。

チャーチ数項と繰り返し.

0 := λf.id 1 := λf z.f z n := λf. f◦ · · · ◦f

| {z }

n

(n >1) iter := λf gm. mf g

次が成り立つ。

iterM N n →^∗_β nM N →β (M◦ · · · ◦M

| {z }

n

)N →β M(M· · ·(M

| {z }

n

N)· · ·).

後続関数・足し算・掛け算・べき乗

suc := λmf. f ◦(mf) add := λnmf.(nf)◦(mf) mult := λnm. n◦m exp := λnm. mn.

例えば足し算について見てみると

add 3 2→^∗_β λf.(3f)◦(2f)→^∗_β λf.(f◦f ◦f)◦(f ◦f)→^∗_β λf.f◦f◦f◦f ◦f ≡5.

原始再帰法

rec:=λf gn.proj₂(iter(λhm, hi.hsucm, f mhi)h0, gin) ここでλhm, hi.M(m, h)と書いたのはλx.M(proj₁x,proj₂x)の省略である。

命題1.1

✓ ✏

M, N をラムダ項とするとき、次のことが成り立つ。

recM N0 =β N,

recM Nn+1 =_β Mn(recM Nn).

ラッセルのパラドックスから不動点定理へ. ラムダ抽象λx.M[x]は集合{x:M[x]}^の一 般化であり、適用M N は所属関係N ∈M の一般化だと思うことができる。つまりラム ダ計算は素朴集合論の一般化である。そこでラッセルのパラドックス

R∈R, R:={x:neg(x∈x)}

をラムダ項で表してnegを任意のラムダ項Mに置き換えると fixM := (λx.M(xx))(λx.M(xx)).

となる。このとき

fixM →β M(fixM) fix(λF.M[F]) →^∗_β M[fix(λF.M[F])]

が成り立つ。fixを不動点演算子という。

最小化. ラムダ項Pが与えられたとき、

µP := fix(λF x.if P xthenxelseF(sucx)) と置くと、

µP n →^∗_β ifPn then n elseµP(n+1).

1.3 型なしラムダ計算の性質 定理1.2(チューリング完全性)

✓ ✏

部分関数f :N⇀Nについて、次の二つは同値である。

1. f は部分再帰的関数である。

2. ラムダ項Fが存在して

f(m) =n ⇐⇒ F m→^∗_β n が任意のm, n∈Nについて成り立つ。

✒ ✑

M, N が共通のラムダ項Kに簡約できるとき（つまりM →^∗_β K, N →^∗_β K）、M ↓N と書く。

補題1.3(局所合流性)

✓ ✏

M →β N₁, M →β N₂ =⇒ N₁ ↓N₂.

✒ ✑

実際には以下の強い性質が成り立つが、ここでは証明しない。

定理1.4(合流性, Church and Rosser)

✓ ✏

M →^∗_β N1, M →^∗_β N2 =⇒ N1 ↓N2.

✒ ✑

系1.5

✓ ✏

1. 各ラムダ項は高々1つしか正規形を持たない。

2. M =_β N ⇐⇒ M ↓N. 3. N が正規形のとき、

M =β N ⇐⇒ M →^∗_β N.

✒ ✑

系1.6

✓ ✏

1. 2項M, N が与えられたとき、M =_β N かどうかは決定不能である。

2. ∅ 6=X (Termとする。もしX^が=β について閉じているなら、X^{は再帰的集} 合ではない。

✒ ✑

定理1.7

✓ ✏

正規化可能なMが与えられたとする。このとき、常にもっとも左側にあるβ基を選 んでβ簡約を続ければ、必ず正規形に到達することができる。

✒ ✑

補題1.8

✓ ✏

正規形のラムダ項は次の文法により生成される。

M ::=xM₁· · ·Mn |λx.M ただしn≥0.

✒ ✑

2 単純型つきラムダ計算 λ

2.1 定義

単純型. 基本型の集合PrmTypeが与えられているものとする。型を以下で定義する。

σ, τ ::= o|(σ →τ).

ただしo∈PrmType. 型全体の集合をType(λ)と書く。

σ →(τ →ρ)をσ →τ →ρと略記する。

単純型つきラムダ項. 次の関数により各変数には型が割り当てられているものとする。

type:Var−→Type(λ) ただし各型σ^についてVar_σ :=type⁻¹(σ)^{は可算無限。}

「ラムダ項Mが型σを持つ」ことをM :σまたはM^σと書き、以下のように定義する。

x∈Var_σ

x:σ (var) M :τ x∈Var_σ

λx.M :σ→τ (abs) M :σ→τ N :σ M N :τ (app) また、

Term_σ :={M ∈Term | M :σ}, Term(λ) := [

σ∈Type(λ)

Term_σ

と定める。Term(λ)(Termである。以下では、型つきのラムダ項M ∈Term(λ)のみを考 える。

命題2.1

✓ ✏

型σを持つ閉項M :σがある ⇐⇒ ^論理式σは直観主義命題論理で証明可能.

✒ ✑

それゆえ型つきラムダ項M :σは論理式σの証明と同一視できる。

定理2.2(主部簡約定理)

✓ ✏

M[x^τ] :σ, N :τ =⇒ M[N] :σ M :σ, M →^∗_β N =⇒ N :σ.

✒ ✑

階数

rank(o) := 0

rank(σ→τ) := max{rank(σ) + 1,rank(τ)}

rank(M) := max{rank(type(N)) :N はM の部分項}.

とくにM :σが正規形の閉項のときには、rank(M) =rank(σ)である。

2.2 型つきラムダ項を用いた関数表現

基本型o∈PrmTypeを1つ固定する。

Bσ := σ→σ →σ B := Bo

Nσ := (σ →σ)→(σ→σ) N := No

命題2.3

✓ ✏

Mを正規形の閉項とする。

1. M :Bならば、M ≡true 又は false.

2. M :Nならば、あるn∈NについてM ≡n （またはλf^(σ→σ).f）。

✒ ✑

以下の項の階数は2である。

neg : B→B conj : B→B→B

また以下の項の階数は3である。

∀: (B→B)→B ただし∀ ≡λF.conj(Ftrue)(Ffalse).

一方でrec,fix6∈Term(λ)である。

2.3 単純型つきラムダ計算の性質

各自然数rについて次の決定問題を考える。

• Bool(r): 階数rの閉項M, N :Bが与えられたとき、M =β N かどうか？

定理2.4(T. 2012)

✓ ✏

1. r = 2n+ 2のとき、Bool(r)はn-EXPTIME完全である。

2. r = 2n+ 3^のとき、Bool(r)^はn-EXPSPACE^{完全である。}

とくにBool(2)はP完全であり、Bool(3)はPSPACE完全である。

✒ ✑

系2.5(Statman)

✓ ✏

同じ型の項M, N ^{が与えられたとき}M =β Nかどうかを決定する問題は、決定可能 であるが初等的ではない。

✒ ✑

定理2.6(強正規化可能性)

✓ ✏

2項関係(→β)⁻¹はTerm(λ)上で整礎である。つまり無限β簡約列 M₀ →β M₁ →β M₂ →β · · ·

はTerm(λ)^{の中に存在しない。}

✒ ✑

一般に、M ∈Termを起点とする無限β簡約列が存在しないとき、M^{は強正規化可能で} あるという。他方で、Mから正規形へと至る有限のβ簡約列が存在するとき、Mは弱正 規化可能であるという。

系2.7(弱正規化可能性, Turing(?))

✓ ✏

どんな型つきラムダ項も正規形を持つ。

✒ ✑

弱正規化可能性がΠ⁰₂文なのに対し、強正規化可能性はΠ¹₁文であることに注意。

補題2.8(Newmanの補題)

✓ ✏

クラスX上の（集合状の）整礎関係Rが局所合流性を満たすならば、R^{は合流性を}

✒満たす。 ✑

このことと補題1.3から、少なくとも型付きラムダ項については合流性（定理1.4）が 成り立つことがわかる。

系2.9(等式理論の無矛盾性)

✓ ✏

true,false:B^についてtrue=β falseは成り立たない。

✒ ✑

2.4 外延性について η^簡約.

λx.M x →η M (x6∈fv(M)).

→βと→ηを含む最小の合同関係（ラムダ抽象、適用について閉じた同値関係）を=_βη と書く。これは以下のように定義できる。

(λx.M[x])N =_βη M[N]

x6∈fv(M) λx.M x=_βη M

M =_βη M

M =βη N N =_βηM

M =βη N N =βη K M =_βη K M =_βη N

λx.M =βη λx.N

M =_βη N K=_βη L M K =βη N L 命題2.10

✓ ✏

=βηは外延性を満たす。つまりM, N :σ →τのとき、

M K=βηN K ^{（すべての}K:σ^{について）} =⇒ M =βη N.

✒ ✑

2.5 単純型つきラムダ計算の標準モデル

簡単のため、基本型はただ1^つo^{しかないものとする。}

型の解釈 何らかの集合X^{を固定する。}

[[o]] :=X, [[σ →τ]] := [[τ]]^[[σ]].

ラムダ項の解釈 関数v^{は、各変数}x∈Var_σにv(x) ∈[[σ]]を割与えるものとする（これ を付値という）。このとき、各M :σ^に対して[[M]]v ∈[[σ]]^{を次のように定める。}

[[x]]_v := v(x)

[[λx^σ.M]]_v := {(a,[[M]]_v[x7→a]) :a∈[[σ]]}

[[M N]]v := [[M]]v([[N]]v).

M ^{が閉項のとき、}[[M]] := [[M]]vとする（v^{は任意）。}

定理2.11(Friedman, Plotkin)

✓ ✏

M, N が同じ型を持つ閉項のとき、

M =_βη N =⇒ [[M]] = [[N]].

さらにXが無限集合のときには逆も成り立つ。

✒ ✑

2.6 論理的関係

π を集合X 上の置換とすると、π は任意の[[σ]] 上の置換π_σ へと自然に拡張できる：

f ∈[[σ→τ]]^に対して

πσ→τ(f) :=πτ◦f◦π_σ⁻¹. このとき、任意の閉ラムダ項M :σ^はπσ-^{不変である：}

π_σ([[M]]) = [[M]].

これを一般化して次の定義を得る。

論理的関係. R⊆X²が与えられたとき、Ro:=Rとし、

(f, g)∈Rσ→τ ⇐⇒ ∀(a, b)∈R_σ.(f(a), g(b))∈R_τ. と定める。

補題2.12(基本補題)

✓ ✏

R⊆X²とする。任意のラムダ項M[x^σ₁¹, . . . , x^σ_nⁿ] :τ と付値v, wについて (v(xi), w(xi))∈Rσi (1≤i≤n) =⇒ ([[M]]v,[[M]]w)∈Rτ. とくにM^{が閉項のときは}([[M]],[[M]])∈Rτ.

✒ ✑

定理2.13(Plotkin 1970)

✓ ✏

Xは無限集合であるとし、rank(σ) ≤2とする。このとき、任意のa∈[[σ]]について 次の2つは同値である。

1. ある閉項M :σについてa= [[M]]

2. ^すべてのR⊆X^{2について}(a, a)∈Rσ.

✒ ✑

未解決問題. 上の定理は任意の型σに拡張できるか？

2.7 強正規化定理の証明

SN集合. 集合SN⊆Termを次のように定める。

M₁∈SN · · · Mn∈SN n≥0 xM₁· · ·M_n∈SN

M ∈SN λx.M ∈SN

M[N]K~ ∈SN N ∈SN (λx.M[x])N ~K ∈SN 補題2.14

✓ ✏

M ∈SNならMは強正規化可能である。

✒ ✑

補題2.15

✓ ✏

M, N を型つきラムダ項とする。

1. M[x^σ], N^σ ∈SNならM[N]∈SN.

2. M^σ→τ, N^σ ∈SNならM N ∈SN.

✒ ✑

補題2.16

✓ ✏

Mが型つきラムダ項ならM ∈SN.

✒ ✑

補題2.14, 2.16から定理2.6が従う。

2.8 HOL Lightの基礎

ここでは証明支援系HOL Lightの背後にある論理HOLをやや簡略化して説明する。

大雑把にいってHOLはチャーチの単純型理論に選択公理と無限公理を加えたものに相当 する。

構文論. HOLの型は単純型である¹。ただし基本型はind,boolの2つのみとする。HOL の項は単純型つきラムダ項である。ただしラムダ項の中で定数

=σ:σ→σ →bool, εσ : (σ →bool)→σ (σ∈Type(λ)) を用いてよいものとする。

bool型のラムダ項を表すのにϕ, ψ等の記号を用いる。=σ M NをM =N と書く。さ らにσ =boolのときにはM ⇔Nとも書く。

Γ∪ {ϕ}^がbool型のラムダ項の有限集合のとき、

Γ⊢ϕ を推件という。

推論規則. HOLの推論規則は以下の通り。最後の3つ以外はラムダ計算のメタ関係=_β を対象化することにより得られることに注意。

⊢M =M REFL Γ⊢M =N Γ⊢N =K

Γ∪∆⊢M =K TRANS Γ⊢M =N ∆⊢K =L

Γ∪∆⊢M K=N L MK COMB Γ⊢M =N

Γ⊢(λx.M) = (λx.N) ABS

⊢(λx.M[x])N =M[N] BETA

ϕ⊢ϕ ASSUME Γ⊢ϕ⇔ψ ∆⊢ϕ

Γ∪∆⊢ψ EQ MP Γ⊢ϕ ∆⊢ψ

(Γ\{ψ})∪(∆\{ϕ})⊢ϕ⇔ψ DEDUCT ANTISYM ただしABS^{規則において}Γ^はxを自由変数として含まないものとする。

論理記号は省略表現として導入する。

⊤ := id=id :bool

∧ := λpq.hp, qi=h⊤,⊤i :bool→bool→bool

⇒ := λpq.p∧q⇔p :bool→bool→bool

∀σ := λP.P =λx.⊤ : (σ →bool)→bool

∃σ := λP.∀q.(∀x.P[x]⇒q)⇒q : (σ →bool)→bool

∨ := λpq.∀r.(p⇒r)⇒(q⇒r)⇒r :bool→bool→bool

⊥ := ∀p.p :bool

¬ := λp.p⇒ ⊥ :bool→bool

∀σ(λx^σ.ϕ[x])のことを∀x.ϕ[x]^と書く。∃^{についても同様。}

その他にHOL Lightの論理は3つの公理を含む。

⊢(λx.M x) =M ETA AX

⊢M x⇒M(εM) SELECT AX

⊢ ∃f^ind→ind.ONE ONEf ∧ ¬ONTOf INFINITY AX ただしM はxを自由変数として含まないものとする。また

ONE ONEf := ∀x1.∀x2.f x1 =f x2 ⇒x1 =x2

ONTOf := ∀y.∃x. y=f x.

以上の推論規則により、通常の高階古典論理の定理に加え、選択公理と無限公理が導出 できる。

HOL^{の標準モデル} [[ind]] :=ω, [[bool]] := {⊤,⊥}とすれば、前と同様にして全ての型 を解釈できる。また、

a=b ⇐⇒ [[=_σ]](a, b) =⊤ f⁻¹(⊤)6=∅ =⇒ [[ε_σ]](f)∈f⁻¹(⊤)

となるように[[=σ]] : [[σ]]² −→[[bool]], [[εσ]] : [[σ →bool]]−→[[σ]] を定める。

以上によりHOLの全ての項を解釈できる。最後に Γ|=ϕ を、すべての付値vについて

[[ψ]]v =⊤ (ψ∈Γ) =⇒ [[ϕ]]v

が成り立つことと定義する。

定理2.17(健全性)

✓ ✏

Γ⊢ϕ =⇒ Γ|=ϕ.

✒ ✑

ゆえにHOLは無矛盾である。しかも（選択公理を仮定すれば）V_ω+ωの中でモデルを 構成できる。

3 多相ラムダ計算 λ2

3.1 定義

多相型. ^{型変数の集合}TypeVarが与えられているものとする。λ2の型を以下で定義する。

σ, τ ::= α |(σ→τ) |(∀α.σ).

ただしα ∈ TypeVar. 型全体の集合をType(λ2)と書く。単純型の場合と異なり、型のレ

ベルでも束縛表現が出てくることに注意。型σに含まれる自由型変数の集合をftv(σ)と 書く。

λ2のラムダ項. 以前と同様、変数には型が割り当てられているものとする。

type2 :Var −→Type(λ2).

Var_σ :=type2⁻¹(σ)^とする。

多相ラムダ計算では、変数、ラムダ抽象、適用に加え、型抽象Λα.M、型適用M σの2 つが新たに組み込まれている。λ2のラムダ項は次の規則により得られる。

x∈Var_σ

x:σ (var) M :τ x∈Var_σ

λx.M :σ→τ (abs) M :σ →τ N :σ M N :τ (app) M :σ

Λα.M :∀α.σ (Abs) M :∀α.σ[α]

M τ :σ[τ] (App)

ただし(Abs)規則を適用するときには、

α6∈ {ftv(type(x)) :x∈fv(M)}

が満たされていなければならない（固有変数条件）。ここでfv(M)^はM^{に含まれる自由} 変数の集合。

型つきラムダ項全体の集合をTerm(λ2)と書く。

命題3.1

✓ ✏

型σを持つ閉項M :σがある ⇐⇒ ^論理式σは直観主義二階命題論理で証明可能.

✒ ✑

系3.2

✓ ✏

型σが与えられたとき、閉項M :σがあるかどうかは決定不能である。

✒ ✑

β簡約. 簡約規則として、新たに

(Λα.M[α])τ →β M[τ]

が加わる。厳密にいえば、これはMに含まれる束縛変数x^σ[α]を一斉に別の変数y^σ[τ]で

（型なしラムダ項としての）構造が変わることはない。また固有変数条件により、自由変 数の置き換えが生じることはない。

2項関係→βの正確な定義は次の通り。

(λx.M[x])N →β M[N] (Λα.M[α])τ →β M[τ]

M →β N λx.M →β λx.N M →β N

KM →β KN

M →β N M K→β N K

M →β N M τ →β N τ

主部簡約定理（定理2.2）も以前と同様に成り立つ。つまりラムダ項の型はβ簡約して も変わらない。ただしβ基内部の型は動的に変わっていくため、多少の注意が必要である。

定理3.3(主部簡約定理)

✓ ✏

M[x^τ] :σ, N :τ =⇒ M[N] :σ M[α] :σ[α] =⇒ M[τ] :σ[τ] M :σ, M →^∗_β N =⇒ N :σ.

✒ ✑

3.2 多相型ラムダ項を用いた関数表現

基本的なデータ型と関数. 多相型を用いて、改めてデータ型を定義し直す。

B := ∀α. α→α→α

true := Λα.λx^α.λy^α.x :B false := Λα.λx^α.λy^α.y :B

N := ∀α.(α →α)→(α→α) n := Λα.λf^α→α. f ◦ · · · ◦f

| {z }

n

:N

ただし0:= Λα.λf^α→α.λz^α.z,1:= Λα.λf^α→α.λz^α.f z.

こうすれば、前出の関数型ラムダ項も再定義できる。たとえば neg := λb^B.Λα.λx^αy^α.bαyx :B→B

suc := λm^N.Λα.λf^α→α. f ◦(mαf) :N→N

exp := λn^Nm^N.Λα.m(α →α)(nα) :N→N→N  iter := λf^N→Ng^Nm^N.mNf g : (N→N)→N→N recも同様にλ2のラムダ項に直すことができて、その型は

rec: (N→N→N)→N→N.

となる。それでもfixやµ^{は型を持たない。}

リスト型と多相関数. 型σのリスト型は次のように定義できる。

L(σ) := ∀α.(σ →α→α)→α→α.

たとえばa, b, c:σとすると、リスト[a; b; c]は

Λα.λf^σ→α→α.f a◦f b◦f c:L(σ)

と表せる。関数型プログラミング言語でよく用いられるmap関数は、関数F とリストl が与えられたらlの各要素にF を適用する関数である。

map(F,[a; b; c]) = [F(a); F(b); F(c)].

これはリストの型に依存しない多相関数の代表例である。このような関数がλ2^の中でう まく表現できる。

map := Λβ.Λγ.λF^β→γ.λl^L(β).Λα.λf^γ→α→α. lα(λx^β.f(F x)) : ∀βγ.(β →γ)→L(β)→L(γ).

論理結合子の定義

⊤ := ∀α. α→α

⊥ := ∀α. α

σ∧τ := ∀α.(σ →τ →α)→α.

σ∨τ := ∀α.(σ →α)→(τ →α)→α

∃β.σ[β] := ∀α.(∀β.σ[β]→α)→α.

ただしαはσ, τ に自由変数として含まれない新しい型変数とする。

3.3 多相ラムダ計算の性質 定理3.4

✓ ✏

部分関数f :N⇀Nについて、次の二つは同値である。

1. f のグラフはΣ⁰₁集合であり、全域性が二階算術PA2で証明できる。

2. 多相型ラムダ項F :N→Nが存在して

f(m) =n ⇐⇒ F m→^∗_β n が任意のm, n∈Nについて成り立つ。

✒ ✑

上の定理の⇐方向には次の定理が関わっている。具体的には、閉項M :N→σが与え られたとき、「すべての自然数nについてM nは強正規化可能である」ことをPA2が証 明できることから帰結する。

定理3.5(強正規化可能性)

✓ ✏

任意の型σについて、型σを持つ閉項M :σは強正規化可能である。

✒ ✑

λ2は局所合流性を満たす。それゆえ再びNewmanの補題（補題2.8）が使える。

定理3.6

✓ ✏

→βはTerm(λ2)上で合流性を満たす。

✒ ✑

それゆえ系1.5の諸性質が成り立つ。

系3.7

✓ ✏

1. 各ラムダ項はちょうど1つ正規形を持つ。

2. ^同じ型の2^項M, N^{が与えられたとき、}M =β N かどうかは決定可能である。

✒ ✑

3.4 標準モデルの多相版？

次のような集合族U^{を考える。}

1. X ∈ U^ならばX 6=∅.

2. X, Y ∈ U^ならばY^X ∈ U.

3. 任意の関数F :U −→ U ^についてQ

X∈UF(X)∈ U.

このようなU ^{があれば、}2.5節の解釈を多相型に自然に拡張することができる。

型付値V :TypeVar−→ U^{が与えられたとき}[[σ]]V ∈ U^{を以下で定める。}

[[α]]V := V(α) [[σ →τ]]_V := [[τ]]^[[σ]]_V ^V

[[∀α.σ]] := Q

X∈U[[σ]]_V[α7→X]

このように型の解釈を定めれば、ラムダ項の解釈も自然にできて M :σ =⇒ [[M]]∈[[σ]]

M =βη N =⇒ [[M]] = [[N]]

となるようにできる（M, Nは同じ型）。ただし型抽象に関するη規則は次の通り。

Λα.M α →η M (α6∈ftv(M)).

定理3.8

✓ ✏

U が上の性質を満たすならば、U の全ての要素は一点集合である。

✒ ✑

3.5 領域理論の考え方

部分関数f :N⇀Nとそのグラフ{(m, n)∈N×N:f(m) =n}を同一視する。

PF:={f :f はNからNへの部分関数}.

とし、全域関数F :PF−→PF^{について考える。}

Fˆ(f, n) :=F(f)(n)

と定義すれば、Fは部分関数Fˆ :PF×N⇀Nと同一視できる。

有向集合族. 集合族X ⊆PFを考える。任意の2元f, g∈ X に対してf ∪g⊆hを満た すh∈ X ^{があるとき、}X は有向であるという。有向集合族の和S

X^{を有向和といい}S↑

X と書く。

有限呼び出し性. G:PF×N⇀ Nが第一引数について単調であり（つまりG(f, m) =n かつf ⊆gならばG(g, m) =n）、なおかつ次の性質を持つとき、Gは有限呼び出し性を 持つという。

• 任意のf ∈ PF, m∈Nについて、G(f, m) =nならばある有限部分関数f₀ ⊆f in f が存在してG(f₀, m) =n.

連続性. F :PF−→PFが任意の有向和を保存するとき、つまり次が成り立つときF^は 連続であるという。

F(S↑

X) =S↑

f∈X F(f).

命題3.9

✓ ✏

F :PF−→PF^{が連続であることと、}Fˆ:PF×N⇀Nが有限呼び出し性を持つこと は一致する。

✒ ✑

確定呼び出し性. G:PF×N⇀Nが第一引数について単調であり、なおかつ次の性質を 持つときGは確定呼び出し性を持つという。

• ^任意のf ∈PF, m∈Nについて、G(f, m) = nならばG(f₀, m) = n,f₀ ⊆f in fを 満たす最小のf₀が（ただ1つ）存在する。

安定性. 連続写像F :PF−→PFが次の性質を満たすとき、安定であるという。任意の f, g ∈PFについて

f ∪g∈PF =⇒ F(f∩g) =F(f)∩F(g).

命題3.10

✓ ✏

F :PF−→PFが安定であることと、Fˆが確定呼び出し性を持つことは一致する。

単一呼び出し性. G:PF×N⇀Nが第一引数について単調であり、なおかつ次の性質を持 つとき、Gは単一呼び出し性を持つという。任意のf ∈PF, m∈Nについて、G(f, m) =n ならばG({(k, l)}, m) =nとなる要素(k, l)∈fがただ一つ存在する。

線形性. F :PF−→PFが任意の互いに素な集合族の和を保存するとき、Fは線形であ るという。

F(P

X) =P

f∈X F(f).

命題3.11

✓ ✏

F :PF−→PFが線形写像であることと、Fˆが単一呼び出し性を持つことは一致する。

✒ ✑

3.6 整合空間意味論

整合空間. 集合|X|^と|X|^{上の反射的関係} ⌢⌣Xの対X = (|X|, ⌢⌣X)を整合空間という。

|X|の要素をトークンといい、⌢⌣^{Xを整合関係という。}

x ⌢X y ⇐⇒ x ⌢⌣^X y∧x6=y

とすれば非反射的関係が得られる。逆に非反射的関係 ⌢X が与えられれば ⌢⌣^{X を復元} することもできる。互いに整合なトークンの集合a ⊆ |X|^{をクリークという（}∀x, y ∈ a. x ⌢⌣^X y）。Xのクリーク全体の集合をClq(X)、有限クリーク全体の集合をFClq(X)と 書く。

例.

N := (N,=)

PF := (N², ⌢⌣^PF) (m₁, n₁)⌢PF (m₂, n₂) ⇔ m₁ 6=m₂

R := (D, ⌢⌣^R) x ⌢^R y ⇔ den(x)6=den(y)∧ |x−y| ≤2^−den(x)+ 2^−den(y). ただしD:=Z×N,den(m, n) :=n. (m, n)∈D^は有理数m/2ⁿを表す。

クリーク空間. (Clq(X),⊆)を半順序集合として見る。

完備性 Clq(X)の有向集合D⊆Clq(X) は常に上極限を持つ（つまりS↑D∈Clq(X)）。

代数性 どんなa ∈ Clq(X)も有限要素からなる有向集合の上極限として表せる（つまり

a=S↑

{a0 ∈FClq(X) :a₀ ⊆f in a}^）。

有界完備性 任意の二元a, b∈Clq(X)^{について、}a⊆c,b⊆c^なるc∈Clq(X)^{が存在する} ときにはa∪b∈Clq(X)である。

以上の3性質を持つので、(Clq(X),⊆)はスコット領域である。またdI領域にもなって いる。

各a∈FClq(X)について

hai:={b∈Clq(X) :a⊆b}

とし、{hai:a∈FClq(X)}^{を開基として}Clq(X)に位相を入れる（スコット位相）。

補題3.12

✓ ✏

U ⊆Clq(X)^は開集合 ⇐⇒U は上方向に閉じており（a∈U,a⊆b^ならb∈U^）、有 向集合によって到達不能である（任意の有向集合D ⊆Clq(X)^{について、}S↑

D∈U ならd∈D∩U が存在する）。

✒ ✑

補題3.13

✓ ✏

X, Y を整合空間とする。F :Clq(X)−→ Clq(Y)は連続写像⇐⇒F は有向和を保存 する。

✒ ✑

安定写像. 整合空間XからY への安定写像F :X−→stY を次のように定義する。Fは Clq(X)からClq(Y)への連続写像であり、

a∪b∈Clq(X) =⇒ F(a∩b) =F(a)∩F(b) を満たす。XからY への安定写像全体の集合をCoh(X, Y)を書く。

補題3.14

✓ ✏

F :X −→Y ^{は安定写像} ⇐⇒ F^{は単調で、}F(a)∋y^ならばF(a₀)∋y, a₀ ⊆f in a^を 満たす最小のa₀が存在する。

✒ ✑

そのような(a₀, y)をFの最小対という。

tr(F) :={(a₀, y)∈FClq(X)× |Y|: (a₀, y)^はF ^の最小対} と定め、F の跡（あるいは骨組み）と呼ぶ。

整合空間の直積. X₁ = (|X1|, ⌢⌣¹), X₂ = (|X2|, ⌢⌣²)が整合空間のとき、X₁×X₂ :=

({1} × |X1| ∪ {2} × |X2|, ⌢⌣¹²),

(i, x)⌢⌣12(j, y) ⇐⇒ x ⌢⌣ⁱ y (i=j)

⇐⇒ 常に成り立つ (i6=j) とし、また⊤:= (∅,∅)^{と定める。すると}

X₁× ⊤ ∼=X₁, Clq(X₁×X₂)∼=Clq(X₁)×Clq(X₂) が成り立つ。

関数整合空間. X, Y が整合空間のとき、X ⇒Y := (FClq(X)× |Y|, ⌢⌣0), (a, y)⌢₀(b, z) ⇐⇒ a ⌢⌣^X b ならばy ⌢Y z

と定める。ただしa, b∈Clq(X)^についてa ⌢⌣^X b^はa∪b∈Clq(X)^{のことである。}|X|,|Y| が無限集合ならば濃度が保たれることに注意。

命題3.15

✓ ✏

任意の整合空間X, Y について

tr:Coh(X, Y)−→Clq(X⇒Y) は全単射である。

✒ ✑

定理3.16

✓ ✏

任意の整合空間X, Y, Z^について

Coh(Z,⊤) ∼= {∗}

Coh(Z, X×Y) ∼= Coh(Z, X)×Coh(Z, Y) Coh(Z, X ⇒Y) ∼= Coh(Z×X, Y)

が“自然に”成り立つ。すなわち整合空間と安定写像がなす圏Cohはカルテシアン閉 圏である。

✒ ✑

単純型の解釈. 単純型付きラムダ計算を考える。各基本型oに整合空間[[o]]を割り当て、

[[σ→τ]] := [[σ]]⇒[[τ]] とする。すると各閉ラムダ項M :σ^に対して[[M]]∈Clq([[σ]])^が自 然に定められる。

定理3.17

✓ ✏

同じ型を持つ任意の閉項M, N について

M =βη N =⇒ [[M]] = [[N]].

基本型oにうまく整合空間を割り当てれば、逆も成り立つ。

✒ ✑

ラムダ計算の逐次性. X, Y, Z を整合空間とし、関数F : Clq(X)×Clq(Y) −→ Clq(Z) が次の性質を満たすとする。空でないクリークa∈ Clq(X), b ∈ Clq(Y), c ∈Clq(Z)が存 在し、

F(a,∅) = c F(∅, b) = c F(∅,∅) = ∅

するとFは安定写像ではありえない。このことからラムダ項で表される関数（より一般的 に副作用のない関数型プログラム）の計算は（弱い意味で）逐次的であることがわかる。

整合空間意味論をはじめとする表示的意味論は、このように計算の性質を調べるのに有用 である。

3.7 線形論理の誕生

線形写像. X, Y を整合空間とする。関数F :Clq(X)−→Clq(Y)が F(P

D) =P

d∈DF(d)

を満たすとき、Fは線形写像であるといい、F :X−→linY と書く。ここで記法P

Dは、

D⊆Clq(X)の各要素が互いに交わらず、P

D=S

Dとなることを表す。XからY への 線形写像全体をLin(X, Y)と書く。

補題3.18

✓ ✏

F :X−→Y ^{は線形写像}⇐⇒ F(a)∋y^ならばF({x})∋y^を満たすx∈a^がただ1^つ 存在する。

✒ ✑

線形関数空間. 以下で2つの整合空間を定める。X⊗Y := (|X| × |Y|, ⌢⌣^X × ⌢⌣^Y), X−◦Y := (|X| × |Y|, ⌢⌣0),

(x, y)⌢0(w, z) ⇐⇒ x ⌢⌣^X w^ならば y ⌢Y z.

また1 := ({∗},{(∗,∗)})^とする。

定理3.19

✓ ✏

任意の整合空間X, Y, Z^について

1⊗X∼=X, X⊗(Y ⊗Z)∼= (X⊗Y)⊗Z, X⊗Y ∼=Y ⊗X および

Lin(Z, X−◦Y)∼=Lin(Z⊗X, Y)

が“自然に”成り立つ。すなわち整合空間と線形写像がなす圏Cohはモノイダル閉 圏である。

✒ ✑

安定写像の線形分解. !X := (FClq(X), ⌢⌣^X)とすると、

!X−◦Y = X ⇒Y である。また

!(X×Y)∼= !X⊗!Y, !⊤ ∼=1 が成り立つ。

さらにX^⊥:= (|X|, ⌢⌣⁰),

x ⌢0y ⇐⇒ ¬(x ⌢⌣^X y) とすると

X^⊥⊥=X, Lin(X, Y)∼=Lin(Y^⊥, X^⊥)

が成り立つ。かくして“二重否定律”を満たしながら直観主義論理を解釈できる奇妙な圏

実関数の表現. 整合空間Rを考える。任意の極大なクリークa∈Clq(R)はコーシー列を 表す。そこでρ(a) := limaと定めると、全射部分関数ρ:Clq(R)⇀Rが得られる。

関数f :R−→Rと安定写像F :R−→stRが、すべてのa∈dom(ρ)ついてf(ρ(a)) = ρ(f(a))を満たすとき、Fはf を実現するという。

定理3.20(Matsumoto and T. 2015)

✓ ✏

関数f :R−→R^について

1. f が連続関数であることとf を実現する安定写像が存在することは一致する。

2. f が一様連続関数であることとfを実現する線形写像があることは一致する。

✒ ✑

3.8 多相型の解釈

次の性質を満たす集合U 6=∅^{を考える。}

x, y∈ U =⇒ (x, y)∈ U a⊆f in U =⇒ a∈ U

以後|X| ⊆ U^{を満たす整合空間}X = (|X|, ⌢⌣^X)のみを考える。そのような整合空間全体 の集合をCohU と書く。明らかにX, Y ∈CohUならばX⇒Y ∈CohUである。

安定写像. 2つの整合空間X, Y について、|X| ⊆ |Y|かつ ⌢⌣^{X が} ⌢⌣^{Y の}|X|への制限 になっているとき、X⊆Y と書く。次の性質を満たす関数Φ :CohU −→stCohUを安定 写像という。

• X ⊆Y ^ならΦ(X)⊆Φ(Y).

• |Φ(X)| ∋xなら|Φ(X0)| ∋x,X₀ ⊆f in Xを満たす最小のX₀が存在する。

そのような(X₀, x)をΦの最小対といい、Φの最小対全体の集合をTR(Φ)と書く。

安定族. Φを安定写像とするとき、次の性質を満たすクリークの族a={a(X)}X∈CohU, a(X)∈Clq(Φ(X))をΦに関する安定族という。

• X ⊆Y ^ならa(X)⊆a(Y).

• a(X)∋xならX₀ ⊆f in X, (X₀, x)∈TR(Φ)を満たすX₀が存在するが、そのX₀が a(X₀)∋x,X₀ ⊆f inXを満たす最小の整合空間となっている。

そのような(X₀, x)をaの最小対といい、aの最小対全体の集合をTr(a)と書く。Φに関す る安定族全体の集合をQst

X∈CohUClq(Φ(X))と書く。

多相整合空間. Φを安定写像とするとき、∀X.Φ(X) := (TR(Φ), ⌢⌣0), (X, x)⌢₀(Y, y) ⇐⇒ X∪Y ∈Coh_U ならば x ⌢X∪Y y と定める。

命題3.21

✓ ✏

任意の安定写像Φ :CohU −→stCohUについて∀X.Φ(X) ∈CohU である。また Tr:Qst

X∈CohU Clq(Φ(X))−→Clq(∀X.Φ(X)) は全単射である。

✒ ✑

このようにすれば、各閉型σに整合空間[[σ]]∈CohUを割り当て、各閉ラムダ項Mに クリーク[[M]]∈Clq([[σ]])を割り当てることができる。さらにM, Nが同じ型のときには

M =_βη N =⇒ [[M]] = [[N]]

が成り立つ（逆は不明）。

3.9 強正規化定理の証明

Term(λ2)∪Type(λ2)の要素をT₁, T₂, . . . で表す。またType(λ2)∪{∗}^の要素はδ₁, δ₂, . . . で表す。

SN集合. SN(∗) :=Type(λ2)とする。またσ∈Type(λ2)について型σを持つラムダ項の

集合SN(σ)を次のように定義する。

T₁∈SN(δ₁) . . . Tn∈SN(δn) x ~T :σ

x ~T ∈SN(σ) (var)

M ∈SN(τ) x:σ

λx.M ∈SN(σ→τ) (abs) M[N^σ]T~ ∈SN(ρ) N ∈SN(σ) (λx^σ.M)N ~T ∈SN(ρ) (app) M ∈SN(σ)

Λα.M ∈SN(∀α.τ) (Abs) M[τ]T~ ∈SN(ρ)

(Λα.M[α])τ ~T ∈SN(ρ) (App) 補題3.22

✓ ✏

M ∈SN(σ)ならばMは強正規化可能である。

✒ ✑

補題3.23

✓ ✏

1. (λx^σ.M)x∈SN(τ)ならばλx.M ∈SN(σ→τ).

2. (Λα.M)α∈SN(τ)ならばΛα.M ∈SN(∀α.τ).

簡約可能性候補. 以前と同様に、すべての閉項M :σについてM ∈SN(σ) となること を示したいのだが、SN集合を直接扱うと循環論に陥る。そこでSNと似た性質を持ちな がら循環論を避けられる集合の族を考える。

次の性質を満たす(ρ, X)全部の集合をRC^{と書く（ここで}Xは型ρを持つラムダ項の 集合）。

M ∈X

M ∈SN(ρ) (sn) T₁ ∈SN(σ₁) . . . Tn∈SN(σn) x ~T :τ

x ~T ∈X (var^′) M[N^σ]T~ ∈X N ∈SN

(λx^σ.M)N ~T ∈X (app^′) M[τ]T~ ∈X

(Λα.M[α])τ ~T ∈X (App^′) 補題3.24

✓ ✏

1. (ρ,SN(ρ))∈ RC

2. ある(ρ, X)∈ RC^についてM ∈Xならば、M は強正規化可能である。

✒ ✑

補題3.25

✓ ✏

(σ, X),(τ, Y)∈ RC^ならば(σ→τ, X ⇒Y)∈ RC. ^ただし X⇒Y :={M^σ→τ :∀N ∈X, M N ∈Y}.

✒ ✑

X⇒Y ^{の構成は論理的関係の}1項版（論理的述語と呼ばれる）になっている。

補題3.26

✓ ✏

関数Φ : RC −→ RCは次の性質を満たすとする。ある型σ が存在して、すべての (τ, X)∈ RC^についてΦ(τ, X)は(σ[τ], Y)の形。このとき(∀α.σ,∀X.Φ(X))∈ RC^が 成り立つ。 ただし

∀X.Φ(X) :={M^∀α.σ :∀(τ, X)∈ RC. M τ ∈Φ(τ, X)}.

✒ ✑

型付値. 関数V :TypeVar−→ RCを型付値という。型σに対してσの中の自由変数αを V(α)₁（V(α)の第一要素）で置き換えた結果をσV と書く。また、集合[[σ]]V を次のよう に定める。

[[α]]V := V(α)₂ [[σ→τ]]_V := [[σ]]_V ⇒[[σ]]_V

[[∀α.σ]]V := ∀X.(fun(τ, X)∈ RC 7→ [[σ]]_{V[α7→(τ,X)]}) 補題3.25、補題3.26より(σ_V,[[σ]]_V)∈ RC^{が成り立つ。}

補題3.27

✓ ✏

[[σ[α]]]_{V[α7→[[τ]]V]}= [[σ[τ]]]_V.

✒ ✑

付値. 関数V :Var−→Term(λ2)を付値という。ただしx:σならばv(x) :σとなるよう にする。ラムダ項M が与えられたとき、自由変数xをv(N)で置き換え、自由型変数α をV(α)₁で置き換えた結果をM_v,V と書く。

補題3.28(基本補題)

✓ ✏

M[x^σ₁¹, . . . , x^σ_nⁿ] :τを型つきラムダ項とする。このとき任意の型付値V と付値vにつ いて

(xi)v,V ∈[[σi]]V (1≤i≤n) =⇒ Mv,V ∈[[τ]]

が成り立つ。とくにM が閉項ならばM ∈[[τ]].

✒ ✑

(τ,[[τ]])∈ RC^{に注意すれば、補題}3.24(2)と補題3.28から強正規化定理が従う。

4 ラムダ・キューブ

省略（もっと自分の言葉で書き直してから公開します）。

5 レポート課題

• ^締切：1^月15^日（金）

• 講義では説明不足な点も多々あったので、文献やweb上の解説記事を参考にするこ と。参照した文献・記事は明記すること。

• 人に相談しても構わないが、相談した場合その旨明記すること。また出来る限り自 分で考えて書くこと。

• 問題について不明な点がある場合には1月10日までにメールで問い合わせること。

• ハンドアウトおよびレポート問題は随時改訂される可能性がある。改訂前の版に基 づいてレポートを書いても全く問題ないが、提出前に最新版を確認することが望ま しい。

• 各問には、難しさに応じて⋆がついている。完答すれば⋆がその分得られる（不十 分な場合には減点）。

• 全部答えなくてもよい。目安としては⋆を7つ集めたら「優」確定と考えてほしい。

もっとも7つ未満でも「優」になる可能性は大いにある。

問1–2では型なしラムダ計算（第1章）について考える。

1^⋆. 相異なる2つの閉項M, N で

M →^∗_β N, N →^∗_β M となるものを求めよ。

2^⋆. 次の性質を満たす正規形の閉項predを求めよ。各自然数nについて pred n →^∗_β 0 (n= 0)

→^∗_β n−1 (n6= 0)

問3–6では単純型つきラムダ計算（第2章）について考える。ただし基本型はただ1^つo しかないものとし、また

N:= (o→o)→(o→o), B:=o→o→o とする。

3^⋆. 次の性質を満たす閉項zero?で型N→Bを持つものを１つ与えよ。各自然数nにつ いて

zero?n →^∗_β true (n= 0)

→^∗_β false (n6= 0)

4^⋆⋆⋆.Xが無限集合のとき、定理2.11の逆方向が成り立つことを示せ。ヒント：Term_σの

=βηによる同値類全体の集合をYσとする。2項関係Ro⊆X×Yoが与えられたら、論理 的関係と同様にしてR_σ ⊆[[σ]]×Y_σ （σは任意の型）へと拡張できて、基本補題が成り立 つ。

問5–6ではXは少なくとも2元を含むものとし、各型σに対して集合[[σ]]を2.5節の通 りに定める。またX上の2項関係R⊆X²が与えられたとき、Rσを2.6節の通りに定め る。すると[[true]],[[false]]∈[[B]]はそれぞれ

[[true]](x)(y) =x, [[false]](x)(y) =y (x, y∈X) を満たす関数になる。

5^⋆⋆.

(a) ([[true]],[[false]])6∈RBとなるようなR⊆X²を1つ与えよ。

(b) 次の性質を満たす関数univ ∈[[(o→B)→B]]を考える。f ∈[[o→B]]に対して univ(f) := [[true]] （すべてのx∈Xについてf(x) = [[true]]のとき）

:= [[false]] （それ以外のとき）

このとき、[[M]] =univとなるような閉項M :o→Bは存在しないことを示せ（基 本補題を使ってよい）。

6^⋆⋆. ^関数f ∈ [[B]]^が全ての2^項関係R ⊆X^{2について}(f, f) ∈ RBを満たすとき、f ^は [[true]]^か[[false]]のどちらかに限られることを示せ。

7^⋆⋆⋆. 古典一階述語論理について考える。ただし関数記号は含まず、関係記号としては等 号=のみを含むものとする。文ϕが古典一階述語論理で証明可能ならば、2.8節で挙げた 推論規則により⊢ϕが導出できることを示せ（注：排中律をどうするか？）。

第3章では、ブール値の型B、自然数の型N、型σのリスト型L(σ)を定義した。特に 自然数のリストの型は

L(N)≡ ∀α.(N→α→α)→(α→α)

8^⋆. 自然数のリストが与えられたとき各要素の総和を返す関数を、型L(N) → Nの閉項 で表せ。

9^⋆. 自然数でラベル付けされた有限二分木の型Tree(N)はどのように定義すればよいか？

4つ以上の節点を持つ二分木の例を1つ考え、それを型Tree(N)の閉項で表せ（3.2節で 説明したリスト型の場合を参考にせよ）。

10^⋆. 命題3.9, 命題3.10を厳密に証明せよ。

11^⋆. ^補題3.12, ^補題3.13^{を厳密に証明せよ。}

12^⋆. 補題2.8の可算版、すなわち次のことを厳密に証明せよ。Xを可算集合とし、X上 の2項関係→⊆X²が与えられているものとする。a, b∈Xについてa=bまたは

a=a₀→a₁→a₂ → · · · →an=b

となるa0,· · · , an∈X^{が存在するとき}a→^∗ b^{と書く。さらに}a→^∗ c^かつb→^∗c^を満た すc∈Xが存在するときa↓bと書く。

今、任意のa, b, c∈Xについて

a→b, a→c =⇒ b↓c

（局所合流性）が成り立つとする。また

a=a₀ →a₁ →a₂ → · · ·

なる無限列は存在しないものとする（強正規化性）。このとき、任意のa, b, c∈Xについて a→^∗b, a→^∗ c =⇒ b↓c

（合流性）が成り立つことを証明せよ。

13^⋆⋆. 本稿に数学的な間違いがあれば、指摘せよ（簡単なタイプミスを指摘してくれても 構わないが、⋆2つ分には相当しない）。

6 参考文献

• ^高橋正子. 計算論 計算可能性とラムダ計算. ^{近代科学社}, 1991.

• H. Barendregt. Lambda calculus with types. Handbook of Logic in Computer Science, vol 2, 1992.

• J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and Types, Cambridge University Press, 1989.

• J.-Y. Girard. Linear Logic: Its Syntax and Semantics. Advances in Linear Logic (edited by J.-Y. Girard, Y. Lafont and L. Regnier). Cambridge University Press, 1995.

• T. C. Hales. Developments in Formal Proofs. S´eminaire BOURBAKI, No. 1086, 2014.

• J. Harrison. HOL Light: An Overview. Theorem Proving in Higher Order Logics.

LNCS 5674, pp. 60–66, 2009.

• J. R. Hindley and J. P. Seldin. Lambda-Calculus and Combinators, Cambridge University Press, 2008.

• P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006.