Avendia20

日記 (2018 年 2 月 28 日)

前回は自然演繹スタイルの直観主義線型論理を定義した。 ところで、 Curry–Howard 対応として知られているように、 何らかの論理体系があれば、 型と項がそれぞれ論理式と証明に対応するような計算模型があるはずである。 そこで今回は、 直観主義線型論理に対応する計算模型とその型付け規則を定義する。

項の定義にも様々なバリエーションがあり、 広く受け入れられている定義というのは特にないようである。 ここでは Bierman†2 の定義を用いる。 項の定義を個別に行うことはただ冗長なだけなのでここではせず、 型付け規則と同時に項も定義することにする。

以降、 M1,⋯,Mk のような列を簡単に 󰕷M と書く省略記法を採用する。

定義 2.1.

直観主義線型論理に関する項の型付け規則を以下によって定める。 x:A⊢x:AAxiom Γ1⊢M1:A1 ⋯ Γk⊢Mk:Ak Γ1,⋯,Γk⊢true󰕷M:11I Γ1⊢M1:A1 ⋯ Γk⊢Mk:Ak Δ⊢N:0 Γ1,⋯,Γk,Δ⊢false󰕷MforN:B ⊢⋆:⊤⊤I Γ⊢M:⊤ Δ⊢N:A Γ,Δ⊢let⋆↦MinN:A⊤E Γ⊢M:A Γ⊢N:B Γ⊢⟨M,N⟩:A×B×I Γ⊢M:A×B Γ⊢fstM:A×EL Γ⊢M:A×B Γ⊢sndM:B×ER Γ⊢M:A Γ⊢inlM:A+B+IL Γ⊢M:B Γ⊢inrM:A+B+IR Γ⊢M:A+B Δ,x:A⊢N:C Δ,y:B⊢P:C Γ,Δ⊢caseMofinlx↦N∣inry↦P:C+E Γ⊢M:A Δ⊢N:B Γ,Δ⊢M⊗N:A⊗B⊗I Γ⊢M:A⊗B Δ,x:A,y:B⊢N:C Γ,Δ⊢letx⊗y↦MinN:C⊗E Γ,x:A⊢M:B Γ⊢λx:A.B:A⊸B⊸I Γ⊢M:A⊸B Δ⊢N:A Γ,Δ⊢MN:B⊸E Γ1⊢M1:!A1 ⋯ Γk⊢Mk:!Ak !x1:A1,⋯,!xk:Ak⊢N:B Γ1,⋯,Γk⊢promote󰕷x↦󰕷MinN:!B!P Γ⊢M:!A Δ⊢N:B Γ,Δ⊢discardMinN:B!W Γ⊢M:!A Δ,x:!A,y:!A⊢N:B Γ,Δ⊢copyx,y↦MinN:B!C Γ⊢M:!A Γ⊢derelictM:A!D 以上によって定義される項を線型項 (linear term) という。

以下で定める省略記法もしばしば用いる。 discard󰕷MinN ≡ discardM1in(discardM2in(⋯(discardMkinN)⋯)) copy󰕷x,󰕷y↦󰕷MinN ≡ copyx1,y1↦M1in(copyx2,y2↦M2in(⋯(copyxk,yk↦MkinN)⋯))

さて、 項の簡約規則についても、 Bierman 自身が様々な種類のものを与えている。 ここでは、 その中で最も基本となる β-簡約のみを考える。 これは、 論理結合子を導入した後すぐに除去するという無駄な証明過程を取り除くことに対応している。

定義 2.2.

線型項の簡約規則を以下によって定める。 (λx:A.B)N ⇝β M[x:=N] let⋆↦⋆inM ⇝β M letx⊗y↦M⊗NinP ⇝β P[x:=M,y:=N] fst⟨M,N⟩ ⇝β M snd⟨M,N⟩ ⇝β N case(inlM)ofinlx↦N∣inry↦P ⇝β N[x:=M] case(inrM)ofinlx↦N∣inry↦P ⇝β P[y:=M] derelict(promote󰕷x↦󰕷MinN) ⇝β N[󰕷x:=󰕷M] discard(promote󰕷x↦󰕷MinN)inP ⇝β discard󰕷MinP copyy,z↦(promote󰕷x↦󰕷MinN)inP ⇝β copy󰕷u,󰕷v↦󰕷MinP[y:=Y,z:=Z] なお、 最後の式において、 Y ≡ promote󰕷x↦󰕷uinN Z ≡ promote󰕷x↦󰕷vinN とおいた。 以上によって定義される簡約を β-簡約 (reduction) という。

項の代入の定義はここでは省略する。 これは、 以下の定理が示すように、 代入によって型が変わらないよううまく定義されている。 線型論理に対応する項の定義は、 実は Abramsky†1 などが Bierman より前に行っていたが、 この型付け体系は代入による型の不変性が成立しないことが、 後に Wadler†3 によって証明された。 Bierman の定義では、 この問題が解消されている。

定理 2.3.

型割り当て Γ,x:A⊢M:B と Δ⊢N:A がともに導出可能であれば、 Γ,Δ⊢M[x:=N]:B も導出可能である。

また、 ここでは証明しないが、 β-簡約によって型が変わることもない。

定理 2.4.

型割り当て Γ⊢M:A が導出可能で、 さらに M⇝βN が成り立つならば、 Γ⊢N:A も導出可能である。

さて、 線型項と β-簡約の圏論的モデルを構成することが今後の目標だが、 圏論的モデルとは何なのかを以下に定義する。

モデルには対称モノイダル圏を用いるが、 モノイダル圏のテンソル積は常に ⊗ で表し、 これに対する単位元は ⊤ で表す。 代わりに終対象を 1 で表すことにする。

定義 2.5.

対称モノイダル圏 󰒚 を考える。 各論理式 A に対し、 対象 ⟦A⟧ が 1 つ定まっているとする。 さらに、 文脈 Γ≡x1:A1,⋯,xk:Ak に対し、 ⟦Γ⟧=⟦A1⟧⊗⋯⊗⟦Ak⟧ とおくと、 各型割り当て Γ⊢M:A に対し、 射 ⟦M⟧:⟦Γ⟧→⟦A⟧ が 1 つ定まっているとする。 このとき、 󰒚 を線型構造 (linear structure) という。

定義 2.6.

対称モノイダル圏 󰒚 を考える。 󰒚 が線型構造であって、 任意の β-簡約 M⇝βN に対して ⟦M⟧=⟦N⟧ が成り立っているとする。 このとき、 󰒚 を線型モデル (linear model) という。

参考文献

  1. S. Abramsky (1993) 「Computational interpretations of linear logic」 『Theoretical Computer Science』 111:3–57
  2. G. M. Bierman (1993) 「On intuitionistic linear logic』 Ph. D. thesis, The University of Cambridge
  3. P. Wadler (1992) 『There's no substitute for linear logic』 Workshop on Mathematical Foundations of Programming Language Semantics