日記 (2020 年 7 月 9 日)

7 月 8 日では、 λμ-計算を導入してその直観的意味について解説した。今日は、 λμ-計算に型付け規則を定め、 Curry–Howard 対応のもとで古典論理に対応することを見ていこうと思う。

定義 4.1.

計算体系 λμ を考える。可算集合 󱀀 を固定し、この元を基本型 (basic type) と呼ぶ。さらに、基本型をメタ変項 α で表すことにし、その上で、 A::=α∣⊥∣A⇀A とする。このとき、これによって定まるものを型 (type) という。

λμ-計算には変項と名前があるので、型割り当てのときに使われる文脈もそれぞれに対応して 2 種類考える必要がある。

定義 4.2.

計算体系 λμ において、変項と型の 0 個以上の組から成る列であって現れる変項が相異なるものを変項文脈 (variable context) という。同様に、名前と型の 0 個以上の組から成る列であって現れる名前が相異なるものを名前文脈 (name context) という。変項文脈は、変項と型をこの順でコロンで区切ったものを並べることで x1:A1,⋯,xn:An と表す。名前文脈についても同様である。

変項文脈 Γ に対して、そこに変項と型の組 x:A を追加して得られるものを Γ,x:A と書くが、このとき暗黙的に Γ に現れる変項と x は異なるものとする。また、変項文脈 Γ,Γ󰎘 に対して、 Γ に現れる変項と型の組が全て Γ󰎘 にも現れることを Γ⊆Γ󰎘 で表す。特に、 Γ を並び替えて Γ󰎘 が得られるときは Γ⊆Γ󰎘 が成り立つ。名前文脈についても同様の記号を用いる。

λμ-計算の型割り当ては、変項文脈 Γ と名前文脈 Δ と項 M と型 A の 4 つ組になり、 Γ⊢M:A∣Δ と表される。通常のラムダ計算における型割り当てに対し、最後に名前文脈が追加されている点に注目してほしい。この関係は以下のように定義される。

定義 4.3.

型システム λμ の型割り当て規則を、 Γ,x:A⊢x:A∣ΔAxiom Γ⊢M:A∣Δ Γ󰎘⊢M:A∣Δ󰎘Weak (Γ⊆Γ󰎘,Δ⊆Δ󰎘) Γ,x:A⊢M:B∣Δ Γ⊢λx.M:A⇀B∣Δ⇀I Γ⊢M:A⇀B∣Δ Γ⊢N:A∣Δ Γ⊢MN:B∣Δ⇀E Γ⊢M:⊥∣a:A,Δ Γ⊢μa.M:A∣Δ⊥E Γ⊢M:A∣Δ Γ⊢{a}M:⊥∣a:A,Δ⊥I で定める。

特殊な型である ⊥ は、常に例外を投げるなどで値を返さない関数の返り値の型と見なすと分かりやすい。 TypeScript では never 型 (void 型ではない) に対応するものである。実際、 {a}M という名前付き項は、これが置かれた環境ではなく a に束縛された環境で M を評価するという意味があるので、 {a}M のすぐ外側には何も値を返さない。そのため、 {a}M は ⊥ 型になっているのである。

以上のように、 ⊥ は値をもたない型を表しているので、論理学的には矛盾 (証明が存在しない論理式) に対応する。論理学では、 A の否定が成立とは A を仮定すると矛盾することとして定義するので、これを踏まえて A⇀⊥ のことを ¬A で表すことにする。

ここで、型割り当ての具体例をいくつか見てみよう。まず、 7 月 8 日で例に挙げた cont≡λm.μa.m(λx.μb.{a}x) を考える。これは、 m:¬¬A⊢m:¬¬A∣ m:¬¬A⊢m:¬¬A∣a:A x:A⊢x:A∣ x:A⊢{a}x:⊥∣a:A x:A⊢{a}x:⊥∣b:⊥,a:A x:A⊢μb.{a}x:⊥∣a:A ⊢λx.μb.{a}x:¬A∣a:A m:¬¬A⊢λx.μb.{a}x:¬A∣a:A m:¬¬A⊢m(λx.μb.{a}x):⊥∣a:A m:¬¬A⊢μa.m(λx.μb.{a}x):A∣ ⊢λm.μa.m(λx.μb.{a}x):¬¬A⇀A∣ と型付けできる。この cont の型である ¬¬A⇀A はいわゆる二重否定除去則で、これは直観主義論理では証明できず古典論理では証明できる命題の 1 つである。

次に、 call/cc≡λm.μa.{a}(m(λx.μb.{a}x)) という項を考えると、これは名前の通り Scheme の call/cc と同じ振る舞いをする項になる。詳細な証明図は省略するが、この項は ((A⇀B)⇀A)⇀A という型をもつことが示せる。これは Peirce の法則と呼ばれる形で、これも直観主義論理では証明できず古典論理では証明できる命題である。

以上のように、継続を扱う演算子には古典論理でしか証明できない形の型が付けられる。これはすなわち、古典論理と比べて直観主義論理に足りない演算とは、計算論的な視点から見れば継続の操作であったということである。このように、古典論理の計算論的意味付けをしたという点が、 Parigot などの成果である。

なお、 Parigot†2 はより強く以下のことを示した。

定理 4.4.

型システム λμ の型 A に対し、 λμ において型 A をもつ閉じた項が存在することは、古典論理において A がトートロジーであることと同値である。

証明.

λμ における型割り当て x1:B1,⋯,xm:Bm⊢M:A∣a1:C1,⋯,an:Cn が、古典論理における演繹 B1,⋯,Bm,¬C1,⋯,¬Cn⊢A に対応することを見れば良い。

追記 (2020 年 7 月 10 日)

最後の定理に簡単な解説を追加した。

参考文献

C.-H. L. Ong, C. A. Stewart (1997) 「A Curry-Howard foundation for functional computation with control」『Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages』 215–227
M. Parigot (1992) 「λμ-calculus: an algorithmic interpretation of classical natural deduction」『Lecture Notes in Artificial Intelligence』 624:190–201