Title Author(s) Citation Issue Date Type 線形論理とはどんな論理か 遠山, 茂朗 一橋研究, 29(1): 69-78 2004-04 Departmental Bulletin Paper Text Version publisher URL http://hdl.handle.net/10086/17892 Right Hitotsubashi University Repository 69 線形論理とはどんな論理か 遠 山 茂 期 1 はじめに 本稿では，J．一Y．GiIa正dの開発した線形論理（Lin蜘Logic）のモティヴェーションを考 察する．線形論理は，GiIa正dが高階型理論Fの意味論を考察しているときに，直観主義 論理のrλ⇒3」がr！λ→別と分析できることに気付いたことから始まった（ただし， r⇒」は直観主義論理のrならば」であり，r！」r→」はそれぞれ線形論理の様相オペレータ とrならば」である）、型理論は一般にプログラムを形式化するのに用いられる．他方，直 観主義論理のBHK解釈（Bmwe正一Heyti暗KolmogoIoプn古e正p−et盆tion）等，証明と計算 の関係を明らかにしようとする試みは20世紀初頭からなされてきた．型理論とこの試みと を結びつけるのがrカリー＝ハワード対応」という考え方である．線形論理もまた，この 考え方に基づいている． 本稿の構成は以下のようになる．まず2節では証明と計算の関係を見る．式計算でのカッ ト除去と（ある種のプログラムと考えられる〕ラムダ計算での計算（β一簡約）との関係を 見た上で，「カリー＝ハワード対応」を説明する．続く3節では，2節での議論を踏まえて 線形論理を概観する・線形論理はカット除去の複雑さを素直に定式化した体系であること が論じられる．最後の4節では証明の意味論を与える際に用いられる表示的意味論につい て若干考察し，線形論理がもたらす視点を指摘する． 2 証明と計算 この節では，Gent竈enの式計算（sequent caloulus）での証明におけるカット除去（㎝t eliminati㎝）と，ラムダ計算（λ一Ca1㎝1uS）での計算の実行（β一簡約）との関係を例を挙げ て解説する．この節で確認しておきたいことは，（式計算の証明における）カット除去と（ラ ムダ計算における）計算には密接な関係があるということである（以下では式計算や自然 演繹，ラムダ計算の初歩的な事柄については既知のものとする）． 2．1 カット除去と証明の正規化 古典論理や直観主義論理での妥当な推論を特徴づける形式体系としては，式計算’（LK， LJ）や自然演繹（NK，NJ），Hilbe正tの公理系などがある．この小節では式計算でのカッ ト除去と自然演緯での証明の正規化と赤対応していることを見る． 70 一橋研究 第29巻1号 まず式計算でのカット除去から見てゆこう．カットとは次のような親則である． rト△，λ ■4，θト目 （Cut） r，θ←△，日 この規則は「左辺から右辺を導いてよい」という意味を表す「←」の推移性を一般化したも のである．数学の教科書などを紐解くと，カット規則が頻繁に用いられているのがわかる． ある定理から補題を介して別の定理を証明する場合が典型例である．また，一般性を表す 命題∀蟷一州肥）から全称例化により具体的なηについての命題刈n）を導く推論でもカット 規則は用いられる． λ（抑）ト■4（n〕 ト∀皿．λ（皿〕∀π．刈π）←λ（伽） （・ut） トλ（冊） 他方，LKや阯に関しては以下の定理が成り立つ． カット除去定理 LK（LJ）で証明できる任意の式は，LK（LJ）でカットを用いずに証 明できる． この定理の証明は，カットされる式（カット規則の上式に現れるλ）に含まれる論理定 項の数を減らす具体的な書き換え手続きを与え，その書き換えは有限ステップで終わるこ とを示すことによって達成される．たとえば，先に挙げた全称例化の証明図にカット除去 の書き換え手続きを適用すると，∀』．刈皿）の現れない刈”）の証明図が得られるI π ←帥） 仰）トλ（簡） 1ψ／α1 ト∀肥坤〕∀刈皿）H（皿） ∼←λ（・〕 抑）ト抑〕 ∼ π［ψ （・・t） （・ut） トλ（n〕 ←刈η） ト川n〕 上図のπ［冊／o］はπの。igenv乱正i乱ble oを冊で書き換えた証明図である。まずカット式が ∀仏刈”）である証明図をカット式が刈皿）である証明図に書き換え。さらに刈冊）のカッ トを含まない証明図に書き換えている、 次に，カット除去の手続きの意味を自然演繹で考えてみることにする．．自然演緯もまた， 古典論理や直観主義論理の妥当な推論を定式化する形式体系であり，式計算と自然演緯に は以下のような関係がある． 定理 トλがLK（LJ）で証明できるのは，λがNK（NJ）で証明できる場合，かつそ の場合に限る． 式計算と自然演繹とは，その定式化の仕方が異なるだけで，同じもの（古典論理や直観 主義論理での論理的真理）を特徴づける体系であることがわかる．非常に大雑把に言って， 式計算での右の論理規則は自然演繹での導入則に対応し，式計算での左の論理規則は自然 演緩での除去貝。に対応する． 線形論理とはどんな論理か 7ユ 自然演繹の証明図で，ある論理定項をいったん導入し，そのあとでその論理定項を除去 するというステップが含まれる証明図を「迂回路のある証明図」と呼ぼう1たとえば，ま ず∀を導入して全称文∀”．刈”）を得てからこの∀を除去しλ（刊）を得る以下のような証 明図は迂回路のある証明図である． π 刈口〕 （∀導入〕 ∀躬一雄） （∀除去） 14（・〕 ここでαはπの前提に現れないものとする．こうした（導入して除去するという）迂回路 をとらない証明図は以下のようになろう． π［ψ1 川η〕 自然演縄での迂回路のない証明図をr正規的な証明図」といい，また，迂回路のある証明 図を正規的な証明図に書き換えることを丁証明の正規化」という．先に述べたように，自 然演縄での導入則は式計算での右の論理規則に，除去則は左の論理規則に，それぞれ対応 した．自然演繹での迂回路のある証明図は噂入レて除去する」というステップが含まれ る証明図であったが，これを式計算で考えれば右の論理規則と左の論理規則で導入された 論理式をカット親則によりr消す」ことに対応する．つまり．迂回路のある証明図はカッ トを含む証明図に対応すると考えられる．よって，自然演繹での証明の正規化は，式計算 でのカット除去に対応すると考えられるのであるユ． 2．2 カリー；ハワード対応 本小節では，自然演縄での証明図の正規化とラムダ書十算での計算の実行との類似性につ いて見る．この類似性はrカリー＝ハワード対応」と呼ばれ，証明をプログラムと見る考 え方である1カリー三ハワード対応の最もわかりやすい例は，NJ→（直観主義論理の自然 演縄の体系で，r→」のみを論理定項として持つ体系）と，ム→（型付きラムダ計算の体系 で，型構成子としてr→」のみを持つ体系）との対応であろう．そこでこれらの関係につ いて少し詳しく見てゆこう． 1ただしここでの対応は一対一ではない．式計算の証明図と自然演縄の証明図の対応関係が一対一ではないの である．たとえば，下図の左端および真ん中のカットなしの証明図はどちらも右端の自然演爆の証明図に対応す ると考えられる． ■4←λ 」BトB λ←λ 」目トB んB←λ＾B A8ト4＾B λ〈o月くD ．4＾0，Bトノー＾B λ、月くjDト■4＾8 4 眉 ■4＾0，月くD←λ＾」呂 ∠＾σ、8＾Dトλ＾月 』＾B 左端と真ん中では，（左＾〕の適用の順序が異なっており，式計算での証明図としては異なる．次の小節で見るカ リー＝ハワード対応の説明のためには自然演繧だけでよいが，後の構造規則に関する…義論は式計算の方が定式化 しやすいため，ここで合わせて論じたのである． 一橋研究 第29巻1号 72 まず，NJ→は以下の導入則と除去則を持つ． ［刈 8 ■4→8 λ λ→B（→I） B 〔→E〕 （→I）での［刈は前提をdischargeすることを表している（1つだけでなく，複数の場合や ○の場合も含む）． 他方，λ→では，ラムダ項Mと型σとからなるM．＝σによって，ラムダ項Mが型σ を持つことを表す．型はラムダ項の持つ何らかの性質を表していると考えればよい．また， 皿1：σ1，．．．1鵯刊1σ刊レM1σ をr型半1」断式」と呼ぶ．ここでr〉」の左辺はr型宣言列」と呼ばれ，変数に対して型を 割り当てている（ただし，型宣言列に現れる変数は互いに異なるものとする）、型手一」断式 を定式化する公理系は以下である． r〉M：σ→τr〉N＝σ r，皿1σ［・M：τ （ax10Hl） （apP） （乱bs〕 r＞配1σ r〉Mw1τ r〉λ旭σ．M：σ一÷τ ただし，rは型宣言列を表す・また，／aXiOm）ではrには征：σが含まれているとする・ ところで，ラムダ計算は関数の一般理論であり，ラムダ項はある種の関数を表す．たと えば，λ血．坦は，何らかのラムダ項を入力するとそれ自身を返す関数（恒等関数）を表す． 一般に，（λ曲。〃〕Mは関数を表す畑．MにWを入力することを意味し，結果はM中の自 由変数配をすべてMで置き換えたもの（これをM山／π］と表す）となる。（λπ．M’〕〃を M山ノ皿］に書き換えることを「β一簡約」と呼ぶ。（λ皿．M〕Wは関数に値を入力するという 見取り図を表しているに過ぎないのであり，実際の計算結果はMlwノ皿1なのである・β一簡 約はラムダ計算での計算の実行に当たる． さてここで，ラムダ項をその命題の証明と考えることにする．つまり，M＝σを「Mは 命題σの証明である」と読むのである（命題の意味をその命題の証明と考えることに当た る）、このとき，NJ→とλ→の間にはある種の類似性があることがわかる．ま．ずλ→の 推論規貝■1（app〕を見よう。型のところだけ注目すれば，これはNJ→での（→E〕である． （→E）ではλ→3の証明図とλの証明図とから3の言正明図が得られることを表して いるが，これをλ→ではMWと表現しているのである。また。（ab昌〕では左辺のσがな くなるのは（→I）での前提のdischaIgeに当たると考えられ，λ→ではMという証明図 を畑．Mという証明図に書き換えることと表している．この意味で，ラムダ項はNJ→で の証明図をコード化していると考えられるのである．もちろん，ある命題に対する証明は 一般に複数存在するので，同一の型を持っラムダ項も複数存在する2Iこうした類似性をカ リー王ハワード対応と呼ぶ． この対応で興味深いのは，自然演繹での証明の正規化とラムダ項の計算（β一簡約）とが 対応していることである．すなわち，NJ→での廻り道のある証明図πに対応するラムダ ！たとえば，畑ん→月、凪λ皿ん→眉〆．囮智、如月→B〆。（（ルん．伽）型〕の型はすべて｛λ→B）→（λ→月〕で 線形論理とはどんな論理か 73 項をMとするとき，Mをβ一簡約した結果〃’はπを正規化して得られる証明図π’に ぴったり対応しているのである3．前小節で確認したように，自然演繹での証明の正規化は 式計算でのカット除去に対応するから，今の結桑と合わせると，カット除去はラムダ項が 表すプログラムの実行に対応するわけである．証明の持つダイナミックな（計算論的な） 側面がここに見られるのである、以上，「→」に絞って論を進めてきたが，これまでの議論 は，各論理定項に対応する型構成子を導入し，その簡約規則を定めることにより，直観主 義論理の他の結合子や量化子に関しても拡張できる． 2．3 構造規貝割とカット除去 この小節で見るのは、「証明＝プログラム」という見方の元では構造規則がカット除去手 続きに対してトリヴィアルではない影響を及ぼすことである． 前小節で見たように，証明と計算には密接なつながりがある．直観主義論理の証明の持つ 計算論的な側面は型付きラムダ計算により抽出することができるのである．しかしこの議論 を古典論理にまで拡張しようとすると次のような問題に出会う．これは左右のweakeni皿g に関する問題（カット除去手続きの非決定性〕である4．いま古典論理の式計算rKでの トλのカットを含まない証明図で互いに異なるものπ1とπ2をとる5．この2つの証明図 を元に次のような証明図πを考える． π1 π2 トλ トーλ トλヨ。（RW）。・λ（LW） （㎝t〕 トAλ トλ（RC） さてこのπに対してカット除去の手続きを実行するとき，π∼π1，または，π∼π2とい う2つの可能性が考えられる．ここまではよい．しかしいまカット除去はある種のプログ ある．それぞれ以下のようなNJ→の証明図に対応する． tλ→B］3［列1 B 1 ［λ→B12［列1 』→月 ［刈2 B 月 ［λ→B1’ λ→月1 λ→B2 工 2 3 （λ→月〕→｛λ→月） （λ→到→（λ→B） （λ→眉〕→（λ→B〕 3前の註の証明図で右端のものが廻り道のある証明図であるが、これを正規化したものが真ん中の証明図であ る・他方、3番目のラムダ項をβ一簡約すると2番目のラムダ項が得られる． ｛以下に挙げる例はエ5，pp．150＿152］でのLafontの例を少し変えたものである。この例は古典論理の証明に 対して表示的意味論ωe口。tation引冒ema皿ti6s）を与えられないことを述べるために挙げられた例である． 5式計算の証明図の同一性条件をどう与えるかは問題である．ここでは註。1で挙げたような現員1」の適矧頂が違 うだけの書正明図も区別する非常に細かい分類原理を採用することにする．ただし，カットを含む証明図π丑にカッ ト除去の手続きを実行して得られる証明図π2は同一視する．先に自然演縄と型付きラムダ計算の関係を述べた 際，（工。．M〕Mは計算の見取り図を述べているに過ぎず、実際の計算結果は〃［Nノ皿］であると述べた。カットを 含む言正明図はある種の廻り道を含んでいるが，カット除去によりこうした廻り道をなくすことができる．そして， その結果となるカットなしの証明図が元の証明図の意味だ，と考えているのである．2＋3と5の関係も考えて みよ。前者は計算の手続きを含んでいるが，後者はそうではない，これはFregeのSinnとBedeutungの区別 を思い起こさせる． 74 一橋研究第29巻1号 ラムの実行と考えているのだから，計算結果は一意になって欲しい．だが，π1とπ2はど ちらもカットを含まない証明図であるから，これ以上計算（＝カット除去）すべきところ はない．ということは，計算結果の一意性を望むならばπ1と物という計算結果を同一視 するしかない．これはトλの証明図（＝プログラム）をすべて同一視することを意味する のである6． 直観主義論理の場合，同じ型を持ち互いに異なるそれ以上β一簡約できないラムダ項が複 数存在した．これはカット除去（計算）の実行により，証明図を分類できることを意味す る、しかし古典論理の場合にはカット除去により証明図から新たに得られる情報がほとん どないのである． この小節を終えるに当たって，C㎝t正aCti㎝がカット除去手続きの実行に対して及ぼす影 響も見ておこう．COnt正aCti㎝によって得られた論理式をカット式とする証明図にカット除 去手続きを適用すると，結果する証明図のサイズが指数関数的に増大するのである．この ことを理解するために，次のような書き換えを見よう． π1・ ：π2 π。 1π。rトム，λλ，λ，b←皇 （舳） π。λ，λ，b←富 rト△，λ λ，r，◎←△，亘 叶・，λA・ト目（LC㌧ ・，・，θト・，・，冨 （cut〕 （c皿t） （LC〕．（RC〕 r，◎←△，冨 F，θト△，冨 書き換えの後ではπ1の証明が複製されている、・π1の中にもカットが含まれている可能性 はあり，それぞ洲こ対してカット除去の手続きを適用することになるので，カット除去が 終了するまでの手続きの数（計算量）も指数関数的に増大するのである． 3 線形論理とはどんな論理か 前節で，証明と計算との関係（カリー＝ハワード対応），そして，計算に対する婿造規 則の影響を見た一線形論理はLKから，（1）構造規則weakeni㎎と。㎝tracti㎝．を取り除 き，（2〕新たに様相オペレータを用いて（1）で取り除いた規則を再導入する，ことにより 得られる． まず（1〕についてであるが，前節で見たようにこれらの規則はカット除去（計算）に対 してトリヴィアルではない影響を及ぼした．そこで一旦これらの構造規則を取り除いてみ る．ではそれはどのような論理体系なのだろうか． まず，WeakeningはあるがCOnt肥C七iOnがない場合，λ1，．．．，んトBという式はr＾ からんのそれぞれを高々ユ回使えば8が導かれる」ことを意味する（左辺に現れる命 題をすべて使う必要はない）．他方，OOnt正aCtiOnはあるがWeakeningがない場合，この 式は「λ1からんのそれぞれを1回以上使えばBが導かれる」ことを意味する。よっ て，contractionとweakeningの両方がない場合，この式は「λ1からんのそれぞれをす べてちょうど1回使えば8が導かれる」という意味になることがわかる、co瓦t胞。ti㎝と ○この間慶に対する一つの回答は．πのカット除去の結果をたとえば物に定めてしまうことである．これは P趾igotのルー。阯。uluヨで採られる方法である．ムμ一〇alou1usについてはI71を見よ。 75 線形論理とはどんな論理か weakeningの両方を持たない線形論理では，同一の命題が複数現れてもそれらは互いに区 別されるので，たとえば，前提が証明の中で何回使われるか，といった分析が可能になる． 線形論理がreSOu正Ce−SenSitiVeな論理と言われる訴以である． ところで，これらの構造規則を取り除くご一とにより，LKでは同値な次の「〈（かっ）」 の規則は区別されることになる（「V（または〕」に関しても同様の区別がなされる）． λ，r←△ B，r←△ r←△，A rト△，B λ。。，・ト・（L〈王〕〃。，。ト。（L〈2〕・ト・，λ。・（R〈〕 λ，8，r←△ rト△，λ θト三，3 λ。・、。ト。（L’〈）。，θト・，・，〃・（R’〈） プライムなしの規則によって表される「かっ」は「加法的な（add油王ve）連言」と呼ばれ， プライム付きの規則によるものは「乗法的な（mu1tip王icative）連言」と呼ばれる．線形論 理では，前者の連言は叱」，後者の連言は『⑳」で表される．これらの連言の意味だが， A＆Bはrλと擾のどちらか一方が成り立ち，どちらかは選ぶことができる」であり，連 言肢の選択惟を表している．他方，λ⑱βは「λとBの両方ともが同時に成り立つ」を 意味し，連言肢の並行性を表す．古典論理や直観主義論理の連言は選択性と並行性を共に 持つ．これは。ontIactionとweakeni㎎があることの結果である．しかし線形論理ではこ れらの規則は取り除かれるため，この性質の異なる2つの連言ははっきりと区別されるの である． 次に（2）に進もう・これらの構造規則を取り除いた体系は，加法的（選択性を表す）・桑 法的（並行性を表す）という論理定項の区別を見出したが，この体系の表現力は古輿論理や 直観主義論理に比べて著しく低い．そこでr制御可能な仕方で」contractionとweakoning が再導入される．このときに！と？という様相オペレータが用いられる．より具体的には， c㎝tractio皿やweakeni㎎が適用される論理式には，！や？という様相オペレータを付け るのである一は式の左辺で，？は右辺で，COntraCtiOnやWeakeningが適用される論理式 に付けられる．また，ここでの様相はS4であるτ．たとえば1λの意珠はrλぱ何度でも 成り立つ（Oでもよい）」である。ところで，1．3で見た左右のweak㎝ingの問題は線形論 理では起こらないことに注意しよう．なぜなら，weakeni㎎によって増える式の形が左右 で異なるからである（式の左辺では！λ，右辺では？λとなることに注意）．それゆえ，左 右で増やした式同士をカットすることはできない、 こうして線形論理の体系が得られる．カット除去（計算）の手続きの違いに注目し，そ の違いを様相オペレータによって顕在化させていることがわかるだろう．この線形論理で も，古典論理や蜜観主義論理の場合と同様，カット除去定理を証明することができる． ところで，直観主義論理や古典論理から線形論理への忠実な（faith舳）埋め込みとなる 翻訳が存在する8．これは次のように考えればよい． 7S4の必然憧オペレータロはりこ，可能性オペレータ◇は？に，それ岩れ対応する．S4の定理は到達可 能性が反射的で推移的な任意のフレームで妥当である．こうしたフレームが対応するのは「ト」が反射的（公理 に現れている）で推移的（カットに現れている）だから．と考えられる． ただし厳密には通常の様相論理S4とは異なる．それは通常の様相論理は様相オペレータを加えて古典論理を 拡張することによって得られるからである一線形論理は（1〕で得られた体系に様相オペレータを加えているので ある． 岳ziから￡，への翻訳（一〕。が忠実な埋め込みであるとは， r←△がf1で証明可能⇔roト△oが￡2で証明可能 76 一橋研究 第29巻1号 線形論理にはCOnt誠CtionやWeakeni㎎を制御するためのオペレータ！や？があるが， これらはS4様相であった．ところで直観主義論理をS4様相論理に忠実に埋め込む翻訳 には，Gδdelの翻訳がある．よってこの翻訳を使えば直観主義論理を線形論理に埋め込む ことができる．次に古典論理であるが，直観主義論理が線形論理に埋め込めることがすで にわかったので，古典論理を直観主義論理に埋め込むことができればよい．これについて は・Gent呂㎝，G6de｝，Kolmogo正。vらのnegative translati㎝を用いればよい・ ここから，線形論理により古典論理や直観主義論理の計算論的側面を分析する可能性が 見えてくるのである9． 4 証明の意味論 これまで，証明と計算の関係を見た上で，線形論理を概観してきた．線形論理は，証明 をある種のプログラムと見るカリー土ハワード対応を素直に受け止めて得られる体系と考 えることができる．古典論理や直観主義論理などの計算論的倒面を分析するために開発さ れた，きめが細かくかつ表現力の高い体系なのである10． 通衛の論理学の講義では，証明論（シンタクス）と意味論（セマンディックス）の岡方 が教えられる．意味論は，ある論理式が証明できるか否かを判定するのに用いられる（証 明できるならば証明図を構成できるが，証明できない場合が問題である．その形式体系で は証明できないことを示すには，意味論的考察（反例モデルを構成すること）が必要であ る）．つまり，意味論はr証明可能性（p正。vabi1ity）」を扱うのである． 他方，これまでの議論ではいわば一r証明そのもの」を扱っている．証明があるかないか （証明可能性）ではなく，証明が持つダイナミックな側面（カット除去）に注目するのであ る．カット除去により同じカットなしの証明図に至る証明図を同一のものとみなし，証明 図を分類することにより，証明という行為の意味論を与えていると考えられる、 冒頭でも少し述べたように，カリー＝ハワード対応の源泉の一つはBHK解釈であり， この解釈は直観主義論理をの意味論のべ一スになるものであった．直観主義論理は排申律 λVrλを認めない体系であるが，式計算で見たとき，古典論理との違いがはっきりする． 古典論理に対する式計算の体系I−Kの式では，「←」の左右に任意有限個の論理式が現れる が，直観主義論理に対する式計算の体系LJでは「←」の右辺には高々1つの論理式しか現 れなし）．このL』の場合，式は，左辺を入力，右辺を出力とするある種の関数を表してい ると考えることができる．複数の入力に対して結果が1っ，とはわれわれの素朴な関数概 念と合致し，関数型プログラムであるラムダ計算とも適合する、各推論規則は，ある証明 図から別の証明図を構成する手続きを述べるものと解釈でき，これはあるプログラムから 別のプログラムを構成することに当たるのである． ところで，直観主義論理に対応する型付きラムダ計算の体系では，強正規化定理（すべ ての正しく型付けされたラムダ項は有限ステップで正規形に簡約できる）が成り立ち，ま た，チャーチ・ロッサー性（あるラムダ項から複数の簡約の仕方があっても，それらから が成り立つことである． 宮技術的な内容の詳細こっいては［3，4］を参照のこと・また，線形論理の哲学的側副こついては何を見よ． lOカリー＝ハワード対応に基づいた線形論理の計算論的意蜘こついては王1，2］を参照のこと． 線形論理とはどんな論理か 77 同一のラムダ項に簡約できる．系として正規形の一意性が得られる）を持つ、これらは証 明の意味論を考える場合には望ましい性質であると考えられる．これは次のように考えれ ばよい．証明の意味論の目標は，証明図の申に隠されている意味を明示化することにある． これまでの議論ではカット除去によって得られるカットなしの証明図が，その証明図の明 示的な意味を表していると考えてきた．論理規則の適用を余すところなく明示したものが カットなしの証明図だからである1ユ．カット除去定理（強正規化定理）により，証明できる 式はカットなしで証明できるわけだから，これを元の証明図の値と考える（こうした値が 必ずある）．他方，チャーチ・ロッサー性により，この値は一位に定まる．つまり，この2 つの性質により，証明図の意味を一通りに与えることができることになるのである．そし て実際に証明の意味論を与える際には『表示的意味論」と呼ばれる手法が用いられる（表示 的意味論はF正egeのSin皿とBedeut皿ngの区別を応用したものである・各証明図（Si皿n・ 定理の様々な与え方）に対してその証明図の意味（Bedeutu皿g，その証明図からカット除 去により得られる証明図）を与えるのである．この意味論では通常「ドメイン」と呼ばれ る数学的構造が用いられる）． さて，以上を踏まえた上で線形論理に戻ろう．線形論理の証明にも直観主義論理の場合 と同様に表示的意味論を与えることが可能である（coherent昌paceという特殊なドメイン が用いられる［3，41）・ところで，前節で見たように，線形論理には加法的・乗法的などの 区別があるが，これはr文脈（COnteXt）」の扱いに関わっている（規則中でrや△などで 表されている部分がその規則の文脈と呼ばれる）．たとえば，加法的な規則であれば文脈 の共有，乗法的な規則であれば文脈の並列が行われている．さらに，！などの様相オペレー タはこうした文脈の重ね合わせが行われている（1λが「λを任意有限回」を意味したこ とを思い出そう．λが。個の文脈・λが1つの文脈等々をまとめて扱っているのである）． こうした点が。oherent昌paceより見て取れる、古典論理や直観主義論理では隠れてしまっ ていた論理的操作の違いを線形論理は明らかにするのである．これは伝統的に論理定項と 呼ばれてきたものの見直しを要求している、加えて，線形論理への翻訳を通じて，古典論 理の証明に対して表示的意味論を与える可能性が示唆されているのであう（ただしいずれ にせよ，線形論理の証明を実装するプログラムの理解が必要である．本稿では紙幅の都合 上・この点に関しては論じない・先に註で挙げた［1，21を参照のこと）・ 参考文献 ［1］S．Abramsky，Computationa1i口terpretatioIls of1i皿ear logic，Z局。o解加。o’0o榊ρωer 3c｛once王11．1993，pp．3−57． 工2］G．M．Bier】Tlan，Aclassicalhnea正λ一〇aIcu1us，乃eo冊加。ofOompωer3c｛帥。ε227．1999， pp．43−78． ［3］J．一Y．Gi閉止d，Li雌ar logic，Thoo㎎加。o’0omρωer3o｛enoe50．1987，pp．1−102． l1証明図の単純化を可能にするという意味で，カット規貝1』は証明をするわれわれ1ことづて都合のよい現員■』なの である．カット除去定理は，われわれにとって都合のよい規則が自由に使えることを保証する定理なのである（そ して，うまいカット式を探すことが証明者であるわれわれの仕事なのである）． 78 一橋研究 第29巻1号 一4］J・一Y・Gi正ard，Line趾1ogic1it昌sy皿t乱x a皿d sem乱皿tics，in J・一Y・GiI趾d，Y・r乱font and L．脹gnier（eds．〕，〃螂。no跳伽〃鵬。rム。φo，1二〇皿don Mathem乱ticai Socioty Lectu正e Note Series222，Cambridge Unive鵬ity P燗s，Cambridge，1995，pp一一42． エ5］』．一Y．Gir乱rd，Y．Lafont and P．不乱ylo正，〃。θ角口nd理p髄，Camb正idge Universiもy PIess， Camb正idge，1989一 正61岡田光弘r矛盾は矛盾か」，科学哲学会編，r科学哲学』36−2．2003，pp，79−102・ 一7コM・Pミ㎜igot，λμ一。a1c皿1皿s，i皿A．Voronkov〔ed．〕，工。φo Pm四m㎜肌伽g舳dλ刊fom口加d 五εo畠。n伽g，Lecture Notes in A正t拍。iaHnte11igence624，Sp正inge正一VeIlag，Be正hnヨ1992， PP．190−201．
© Copyright 2024 ExpyDoc
