集中講義ハンドアウトおよびレポート課題
（ 2015 年 12 月 15 日 – 12 月 18 日、東北大学）
京都大学数理解析研究所 照井一成 terui@kurims.kyoto-u.ac.jp
最終更新：2015年12月23日
更新履歴
• 「優」確定に必要な⋆の数を8つから7つに変更。
1 型なしラムダ計算
1.1 定義
ラムダ項. 変数の可算集合Varが与えられているとする。ラムダ項を次の文法で定義する。
M, N ::= x |(λx.M) |(M N).
ただしx∈Var. (λx.M)をラムダ抽象といい、(M N)を適用という。ラムダ項全体の集合 をTermと書く。
かっこは適宜省略する。また、
λx1· · ·xn.M ≡ (λx1.· · ·(λxn−1.(λxn.M))· · ·) M N1· · ·Nn ≡ (· · ·((M N1)N2)· · ·Nn)
とする。
ラムダ項λ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項関係→β⊆Term2を次のように定義する。
(λ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).
関係→βを含む最小の前順序（反射的推移的関係）を→∗βとかく。また、関係→βを含 む最小の同値関係を=βとかく。それ以上β簡約できないラムダ項（つまり(→β)−1極小 元）を正規形という。とくに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, M1◦M2:=λz.M1(M2z), M1◦ · · · ◦Mn:=λz.M1(M2· · ·(Mnz)· · ·) ただしzはM1, . . . , Mnの中には現れない新しい変数とする。次が成り立つ。
idM →β M (M1◦M2)N →β M1(M2N) (M1◦M2)◦M3 →β M1◦M2◦M3 M1◦(M2◦M3) →β M1◦M2◦M3 ブール値・ブール関数.
true := λxy.x false := λxy.y
neg := λbxy.byx conj := λb1b2xy.b1(b2xy)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, M2i:=λz.zM1M2, proj1M :=Mtrue, proj2M :=Mfalse.
ただしz6∈fv(M1)∪fv(M2). このようにすれば
proj1hM1, M2i →∗β M1, proj2hM1, M2i →∗β M2 となる。また、
ifN thenM1 elseM2 := N M1M2
と定義すれば、
if true thenM1 elseM2 →∗β M1, if false thenM1 elseM2 →∗β M2 が成り立つ。
チャーチ数項と繰り返し.
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.proj2(iter(λhm, hi.hsucm, f mhi)h0, gin) ここでλhm, hi.M(m, h)と書いたのはλx.M(proj1x,proj2x)の省略である。
命題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 →β N1, M →β N2 =⇒ N1 ↓N2.
✒ ✑
実際には以下の強い性質が成り立つが、ここでは証明しない。
定理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 ::=xM1· · ·Mn |λx.M ただしn≥0.
✒ ✑
2 単純型つきラムダ計算 λ
2.1 定義
単純型. 基本型の集合PrmTypeが与えられているものとする。型を以下で定義する。
σ, τ ::= o|(σ →τ).
ただしo∈PrmType. 型全体の集合をType(λ)と書く。
σ →(τ →ρ)をσ →τ →ρと略記する。
単純型つきラムダ項. 次の関数により各変数には型が割り当てられているものとする。
type:Var−→Type(λ) ただし各型σについてVarσ :=type−1(σ)は可算無限。
「ラムダ項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項関係(→β)−1はTerm(λ)上で整礎である。つまり無限β簡約列 M0 →β M1 →β M2 →β · · ·
はTerm(λ)の中に存在しない。
✒ ✑
一般に、M ∈Termを起点とする無限β簡約列が存在しないとき、Mは強正規化可能で あるという。他方で、Mから正規形へと至る有限のβ簡約列が存在するとき、Mは弱正 規化可能であるという。
系2.7(弱正規化可能性, Turing(?))
✓ ✏
どんな型つきラムダ項も正規形を持つ。
✒ ✑
弱正規化可能性がΠ02文なのに対し、強正規化可能性はΠ11文であることに注意。
補題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◦πσ−1. このとき、任意の閉ラムダ項M :σはπσ-不変である：
πσ([[M]]) = [[M]].
これを一般化して次の定義を得る。
論理的関係. R⊆X2が与えられたとき、Ro:=Rとし、
(f, g)∈Rσ→τ ⇐⇒ ∀(a, b)∈Rσ.(f(a), g(b))∈Rτ. と定める。
補題2.12(基本補題)
✓ ✏
R⊆X2とする。任意のラムダ項M[xσ11, . . . , xσnn] :τ と付値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⊆X2について(a, a)∈Rσ.
✒ ✑
未解決問題. 上の定理は任意の型σに拡張できるか？
2.7 強正規化定理の証明
SN集合. 集合SN⊆Termを次のように定める。
M1∈SN · · · Mn∈SN n≥0 xM1· · ·Mn∈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の型は単純型である1。ただし基本型は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
⊢ ∃find→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−1(⊤)6=∅ =⇒ [[εσ]](f)∈f−1(⊤)
となるように[[=σ]] : [[σ]]2 −→[[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−1(σ)とする。
多相ラムダ計算では、変数、ラムダ抽象、適用に加え、型抽象Λα.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 := λbB.Λα.λxαyα.bαyx :B→B
suc := λmN.Λα.λfα→α. f ◦(mαf) :N→N
exp := λnNmN.Λα.m(α →α)(nα) :N→N→N iter := λfN→NgNmN.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β→γ.λlL(β).Λα.λfγ→α→α. lα(λxβ.f(F x)) : ∀βγ.(β →γ)→L(β)→L(γ).
論理結合子の定義
⊤ := ∀α. α→α
⊥ := ∀α. α
σ∧τ := ∀α.(σ →τ →α)→α.
σ∨τ := ∀α.(σ →α)→(τ →α)→α
∃β.σ[β] := ∀α.(∀β.σ[β]→α)→α.
ただしαはσ, τ に自由変数として含まれない新しい型変数とする。
3.3 多相ラムダ計算の性質 定理3.4
✓ ✏
部分関数f :N⇀Nについて、次の二つは同値である。
1. f のグラフはΣ01集合であり、全域性が二階算術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ならばYX ∈ 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ならばある有限部分関数f0 ⊆f in f が存在してG(f0, 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(f0, m) = n,f0 ⊆f in fを 満たす最小のf0が（ただ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 := (N2, ⌢⌣PF) (m1, n1)⌢PF (m2, n2) ⇔ m1 6=m2
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/2nを表す。
クリーク空間. (Clq(X),⊆)を半順序集合として見る。
完備性 Clq(X)の有向集合D⊆Clq(X) は常に上極限を持つ（つまりS↑D∈Clq(X)）。
代数性 どんなa ∈ Clq(X)も有限要素からなる有向集合の上極限として表せる（つまり
a=S↑
{a0 ∈FClq(X) :a0 ⊆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(a0)∋y, a0 ⊆f in aを 満たす最小のa0が存在する。
✒ ✑
そのような(a0, y)をFの最小対という。
tr(F) :={(a0, y)∈FClq(X)× |Y|: (a0, y)はF の最小対} と定め、F の跡（あるいは骨組み）と呼ぶ。
整合空間の直積. X1 = (|X1|, ⌢⌣1), X2 = (|X2|, ⌢⌣2)が整合空間のとき、X1×X2 :=
({1} × |X1| ∪ {2} × |X2|, ⌢⌣12),
(i, x)⌢⌣12(j, y) ⇐⇒ x ⌢⌣i y (i=j)
⇐⇒ 常に成り立つ (i6=j) とし、また⊤:= (∅,∅)と定める。すると
X1× ⊤ ∼=X1, Clq(X1×X2)∼=Clq(X1)×Clq(X2) が成り立つ。
関数整合空間. X, Y が整合空間のとき、X ⇒Y := (FClq(X)× |Y|, ⌢⌣0), (a, y)⌢0(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|, ⌢⌣0),
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,X0 ⊆f in Xを満たす最小のX0が存在する。
そのような(X0, x)をΦの最小対といい、Φの最小対全体の集合をTR(Φ)と書く。
安定族. Φを安定写像とするとき、次の性質を満たすクリークの族a={a(X)}X∈CohU, a(X)∈Clq(Φ(X))をΦに関する安定族という。
• X ⊆Y ならa(X)⊆a(Y).
• a(X)∋xならX0 ⊆f in X, (X0, x)∈TR(Φ)を満たすX0が存在するが、そのX0が a(X0)∋x,X0 ⊆f inXを満たす最小の整合空間となっている。
そのような(X0, x)をaの最小対といい、aの最小対全体の集合をTr(a)と書く。Φに関す る安定族全体の集合をQst
X∈CohUClq(Φ(X))と書く。
多相整合空間. Φを安定写像とするとき、∀X.Φ(X) := (TR(Φ), ⌢⌣0), (X, x)⌢0(Y, y) ⇐⇒ X∪Y ∈CohU ならば 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)の要素をT1, T2, . . . で表す。またType(λ2)∪{∗}の要素はδ1, δ2, . . . で表す。
SN集合. SN(∗) :=Type(λ2)とする。またσ∈Type(λ2)について型σを持つラムダ項の
集合SN(σ)を次のように定義する。
T1∈SN(δ1) . . . 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) T1 ∈SN(σ1) . . . 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(α)1（V(α)の第一要素）で置き換えた結果をσV と書く。また、集合[[σ]]V を次のよう に定める。
[[α]]V := V(α)2 [[σ→τ]]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(α)1で置き換えた結果をMv,V と書く。
補題3.28(基本補題)
✓ ✏
M[xσ11, . . . , xσnn] :τを型つきラムダ項とする。このとき任意の型付値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⊆X2が与えられたとき、Rσを2.6節の通りに定め る。すると[[true]],[[false]]∈[[B]]はそれぞれ
[[true]](x)(y) =x, [[false]](x)(y) =y (x, y∈X) を満たす関数になる。
5⋆⋆.
(a) ([[true]],[[false]])6∈RBとなるようなR⊆X2を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 ⊆X2について(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項関係→⊆X2が与えられているものとする。a, b∈Xについてa=bまたは
a=a0→a1→a2 → · · · →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=a0 →a1 →a2 → · · ·
なる無限列は存在しないものとする（強正規化性）。このとき、任意の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.
