このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

演繹系とお絵描き圏論

雑記／備忘

次の2つの事情からこのエントリーを書きます。

  1. oskimuraさんのコメントに対して、あまりにそっけない対応でちと申し訳ない。
  2. 「ラムダ計算、論理、圏」セミナーで、圏の話はほとんど出なかったんじゃないの？ というご指摘に少しだけ応えたい。

「ラムダ計算、論理、圏」セミナーの楽屋裏を紹介するような意図もあります。論理と圏論の知識が若干必要なので、この記事は自己完結的とは言えません。が、流し読みしても大意は伝わると思います。「命題論理とデカルト閉圏」のセクションにある対応表がメダマのつもり。

内容

十人十色な演繹系

図書館に行って論理学の教科書を端から眺めてみると、採用している論理記号、公理系、推論規則などが著者ごとにバラバラなのがわかると思います。有名どころの演繹系（演繹システム、論理システム）には、提唱者の名前やアルファベット2,3文字による固有名詞が付けられていますが、有象無象・無名の系まで入れれば演繹系は無闇とイッパイあります。よって、「THE・演繹系」なんてものはあり得ません（人気投票で決めることは出来るかもしれませんが :-)）。使用目的や趣味嗜好に応じて、公理や推論規則を選んで、その場で演繹系を適当に組み立てているのが実情だと思います。

以前に書いたエントリー「論理とはなにか？」の「個別の論理達から論理の一般論へ」というセクションを（ちと長いですが）引用しましょう。

説明の便宜上、証明論的システムとモデル論的システムに分けました。しかし、ストラスバーガーの意図は、そういう区別や流儀を越えて、より一般的な“論理の定義”を提出することです。

実際、ナントカ論理／カントカ論理という区別や流儀にはウンザリ。ほとんど常に、命題論理と述語論理は区別されますが、この区別は教育的に有害じゃないかと僕は思っています。構文論（証明論）と意味論（モデル論）の区別もまた伝統的です -- これは区別したほうがいいかも知れない、、、たぶん。

論理式にどんな論理記号を許すかも、すごくバリエーションがあります。∧、∨、¬が一番普通でしょうが、⊃（含意）と⊥（矛盾）を採用する流儀もあります。論理記号を1つだけしか使わない体系もできます（これ変態ですけど）。許される推論の多寡＜たか＞によって古典論理と直観主義的論理、その他のナンタラ論理に別れるし、様相記号や、さらにもっと目新しい論理記号を入れた体系もあります。（形式的）証明もヒルベルト方式、ゲンツェン方式（シーケント計算）、タブロー方式なんてのがありますね。

こういう多様性は「論理の豊饒＜ほうじょう＞さ」を示すものでしょうが、僕は、「なんだか博物学・分類学みたいだなー」とも感じます。ストラスバーガーの質問と答えは、こういう不満感を多少は解消してくれます。

複数の演繹系を比較するのは良い練習問題にはなりますが、論理を普通にお勉強するときは博物学・分類学にこだわってもしょうがないと思います。（もちろん、博物学・分類学が好きな人は、それはそれでいいですよ）。

自然演繹とシーケント計算

演繹系のスタイルとして「自然演繹とシーケント計算がある」とされていますが、先に言った事情で、「THE・自然演繹」とか「THE・シーケント計算」が特定できるわけじゃありません。

形の上では、シーケントと呼ばれる表現を使えばシーケント計算なのでしょう。シーケントは、論理式（formula）をカンマで区切った列を、さらに左右に並べたものです。

  • シーケントの形： A1, ..., An ⇒ B1, ..., Bm

右側はたかだか1個の論理式に制限することもあります（直観論理）。

ところがですね、ゲンツェン／テイト（Gentzen-Tait）とかゲンツェン／シュッテ（Gentzen-Shutte）と呼ばれるシステムだと、片側シーケント（one-sided sequent）なんてのが登場するんですよ。

片側シーケントの形は、 ⇒A1, ..., An と、左側がカラッポです（右をカラッポにすることもあります）。片側シーケントの推論規則を挙げてみると：

   ⇒Γ,φ   ⇒Γ,ψ
  ------------------[∧-導入]
     ⇒Γ,φ∧ψ

Γ（大文字ガンマ）は論理式の列ですが、これを1個の論理式γに置き換えると、次の自然演繹の推論規則に対応します。

   γ∨φ   γ∨ψ
  ----------------[∧導入]
    γ∨(φ∧ψ)

Γが空（γが偽）のときは：

   φ    ψ
  ---------[∧-導入]
    φ∧ψ

と、自然演繹の∧-導入に一致します。片側シーケント計算は、両側シーケント計算（例えばLK）と自然演繹（例えばNK）の中間的な雰囲気です。実際、片側シーケント計算は、典型的両側シーケント計算と典型的自然演繹を結ぶときの中間形式として便利です。

こんな例もあるので、こっからここまでは自然演繹、ここから先がシーケント計算なんて境界を明確に設定するのは無理だし、たいした意味もないってことです。もちろん、境界領域から遠く離れた典型的な自然演繹、典型的なシーケント計算と呼べるシステムが存在しますがね。

論理の圏論的意味論

演繹系の意味論を圏を使って定義するときは、単一の論理式、論理式の列、両側シーケント、片側シーケントの違いは割とクリアです。

  1. 論理式 -- 圏の対象
  2. 論理式の列 -- いくつかの対象のモノイド積
  3. 両側シーケント -- 任意の対象のあいだの射
  4. 片側シーケント -- 特定の対象（終対象や単位対象）からの射

連言∧と選言∨を持つ論理だと、圏のモノイド積も2つ必要になり、事情は複雑になります。∧だけの論理なら普通のモノイド圏で解釈できます。特にデカルト圏なら、∧は直積に対応し、真を表す特別な対象として終対象が取れて、片側シーケントの意味は終対象からの射となります。

含意⊃の解釈には、∧に対応するモノイド積に関する指数（べき）が必要です。モノイド積を□、指数は右肩添字で表記するとして、次の対応が欲しいわけです。

  • 射 f:A□B→C と 射 f^:A→CB が1:1に対応する

これが、(-)□B と (-)B の随伴性です。随伴性は、ラムダ計算の基本等式を与えます。これを論理に持ってくると演繹定理（Deduction Theorem, DT）ですね。

  • A, B |- C ⇔ A |- B⊃C
  • 詳しく言うと、「A, Bを仮定してのCの証明」と「Aを仮定してのB⊃Cの証明」が1:1に対応する

指数（べき）を持つモノイド圏はモノイド閉圏と呼ぶのですが、モノイド閉圏においては、連言（∧）と含意（⊃）を含む命題論理の計算（証明）に対して、その意味論をうまいこと構成できます。

圏論的意味論を前提にするなら、自然演繹とシーケント計算の区別はおおよそ次のようになるでしょう。

  1. 推論規則を圏の射に対応させるのが自然演繹
  2. 推論規則をホムセット間の変換に対応させるのがシーケント計算

これも「おおよそ」であって、ちゃんと考えてみると、やっぱり境界線は曖昧です。

演繹系の健全性

前の節で、連言（∧）と含意（⊃）を含む命題論理の意味論は、モノイド閉圏を使って構成できると言いました。モノイド閉圏を(C, □, I, (-)(-), Λ)と書きましょう。Cは台となる圏（underlying category）、□がモノイド積、Iは特定された単位対象です。(-)(-)は指数で、反変共変の双関手として定義できます；(A, B|→BA):Cop×C→C 。Λはラムダ抽象（カリー化）に相当するオペレータです；Λ=ΛA,B,C:C(A×B, C)→C(A, CB)。

演繹系が、圏Cで“まともに解釈できる”とは次のことです。

  • 自然演繹システムにより A, B |- C （A, Bを仮定してCが証明可能）であるとき、A□B→C の射fが圏C内で具体的に構成できる。

論理式も圏の対象も同じ記号A, B, Cで表してもいますが、まーいいとしましょう。

今述べた条件 -- 「演繹系で証明できるなら、圏で射が構成できる」は、圏論的意味論に関する演繹系の健全性になります。意味論なしで演繹系を作ったら、たまたま健全だったということは余りないでしょう。たいていは、健全になるように最初から意図して演繹系を設計します。

命題論理とデカルト閉圏

僕も、健全になるように最初から意図してセミナー向け演繹系を構成しました。

論理 圏
論理式 A 対象 A
連言 A∧B モノイド積 A□B
連言の導入 射のモノイド積 f□g
含意 A⊃B 指数 BA
含意の導入（演繹定理） 随伴によるカリー化（転置射）
含意の消去（モダスポネンス） 評価射 ev

ここまでは、一般のモノイド閉圏でも解釈できます。対称モノイド圏で意味を取る場合は、論理式の位置の交換が許されるので：

論理 圏
入れ替え（換） 対称

デカルト閉圏特有な事情としては：

論理 圏
連言の消去 直積からの射影
複製（増） 対角射
破棄（減） 終対象への唯一射
デカルトペアの構成 対角射と射の直積の組合せ

デカルト閉圏に関して全部寄せ集めてまとめると：

連言と含意の命題論理 デカルト閉圏
論理式 A 対象 A
連言 A∧B 直積 A×B
連言の導入 射のデカルト積 f×g、またはデカルトペア <f, g>
含意 A⊃B 指数 BA
含意の導入（演繹定理） 対応 (f:A×B→C)→(f^:A→CB)
含意の消去（モダスポネンス） 評価射 evA,B:BA×A→B
入れ替え（換） 対称 σA,B:A×B→B×A
連言の消去 1 第1射影 π1A,B:A×B→A
連言の消去 2 第2射影 π2A,B:A×B→B
複製（増） 対角射 ΔA:A→A×A
破棄（減） 終対象への唯一射 !A:A→1

構造規則とお絵描き

oskimuraさんがコメントされているように、自然演繹風の演繹系で構造規則をあからさまに入れるのは珍しいと思います。しかし、どんな演繹系でも構造規則（複製や入れ替え）に相当する機能を他の公理や推論規則に潜伏させています。構造規則と論理規則は性格が違うので、自然演繹であっても明確に分離したほうがいいと僕は思います。構造規則をあからさまに使えば、変な技巧は不要になります*1。

それと、構造規則を分離しておくと、演繹系と圏を並行に扱えます。入れ替え規則（換）を禁止すれば、非対称なモノイド圏の議論になります。入れ替え規則をブレイドに置き換えれば、ブレイド付きモノイド圏に対応する演繹系が出来上がります。破棄を禁止すると終対象がない圏の話になります。複製を禁止すると、リソースのコピーができない圏を扱うことになり、量子系や線形論理のシステムになるでしょう（たぶん）。

さらに、構造規則は回路図（ボックス＆ワイヤー図、ストリング図）と相性がいいのです。一般的な「n-入力 m-出力」の回路図の全体は、圏というより多圏（polycategory）という構造を作るのですが、お絵描き計算には非常に都合がいい舞台です。

僕が想定しているシナリオでは、ラムダ計算も命題論理もお絵描き（回路図）ありきなので、絵が描きやすいことが最優先の定式化になっているのです。

*1:セミナーで提示した系では、破棄を禁止したので技巧的変形が残ってしまいました。証明図＝大きなラムダ式の出力を1つに限りたかったので、0-出力を止めたのですが、複製／交換は2-出力だから徹底はできませんね。