問題集11「小学生でも…」の解答と補足説明 (A23R11) - (保存用) 檜山正幸のキマイラ飼育記メモ編

※この記事は「記事23 問題集11の解答」

問題集11とは、次の記事（の問題部分）のことです：

小学生でも分かる論理計算 (A22P11)

上記記事への追記で次の文言を入れました。

「全部乗せで、完全にグラフィカルなリーズニング図」を描くのはムチャクチャ大変だわー。ゴメン、そこまでやんなくていいわ。真面目にやると、どの程度の労力と面積が必要かの見当がついたら、あとはテキトーに手を抜いていいです。

やっぱり、ガッツリ完全に描画はシンドすぎる。このシンドさを実感すれば、どうして省略記法しか使われないか、の理由も明らかでしょう。

内容：

ゲンツェンのLKシーケント計算をご存知の方への注意
とりあえず描くぞ
プロファイルを調べてみると
連言命題を構成する／連言命題を分解する基本推論

ゲンツェンのLKシーケント計算をご存知の方への注意

検索などでたまたまここに辿り着いた人が誤解するのも困るので、毎回この節を挿入することにします。

'⇒'は含意〈条件法〉の論理結合子で、'→'がシーケントの左右を区切る記号である。
ゲンツェンのLKシーケントでは、左辺のカンマは連言的に、右辺のカンマは選言的に解釈をする。ここでのシーケントでは、出現位置の情報を使わずに、カンマは常に連言的であり、選言的な区切り記号に縦棒'|'を使う。
(x∈R, n∈N) のような書き方は、集合論の命題ではなくて、自由変数の型宣言（のリスト）である。自由変数の型宣言のリストをコンテキストと呼ぶ。
暗黙のコンテキストを使う場合もあるが、できるだけ、シーケント内に明示的にコンテキストを書き込むようにしている。
NK/NJの証明図を推論図、LK/LJの証明図をリーズニング図と呼んで区別している。両方を同時に使うことがある。推論規則は、基本推論／基本リーズニングと呼ぶ。
LK/LJのように、公理（基本推論）がひとつではなくて、けっこうたくさんの公理がある。その代わり、推論規則（基本リーズニング）の数を減らすようにしている。

とりあえず描くぞ

全体を一度には描けない（面積の関係で）ので、いくつかの部分に分けます。描き方は、「面積問題への対策（あるいは無策） (A21) // お約束」に従います。が、全部乗せしません。

この図1を、テキストの式とプロファイルで書くと：



                ☆

            ---------- Ent

 f:A,B→C   dup:C→C,C                                 ☆

 ---------------------- Comp                      ------------- Ent

   f;dup:A,B→C,C          g:C,C→D      h:A→C,D  swap:C,D→D,C

 ---------------------------------- Comp ------------------------ Comp

           f;dup;g:A,B→D                  h;swap:A→D,C

          ------------------------------------------------ Prod

          (f;dup;g)(h;swap):A,B,A→D,D,C

これも、グラフィカルな図と同じ情報を持ちます。欠点は、テキストの式だと2次元の構造が見えなくなることです。リーズニング名の代わりに演算子記号を使うのもいいかも知れません（Entは省略）。



                ☆

            ----------

 f:A,B→C   dup:C→C,C                                 ☆

 ---------------------- ;                          -------------

   f;dup:A,B→C,C          g:C,C→D      h:A→C,D  swap:C,D→D,C

 ---------------------------------- ;    ------------------------ ;

           f;dup;g:A,B→D                  h;swap:A→D,C

          ------------------------------------------------ 

          (f;dup;g)(h;swap):A,B,A→D,D,C

マイク・シュルマン〈Mike/Michael Shulman〉はこれと同じ描画法を使ってます*1。ただし、左右は逆です（その他、細かい違いはあります）。

話を戻して、図1のプロファイルだけなら：



            ☆

          ------- Ent

  A,B→C   C→C,C                                 ☆

 ----------------- Comp                       ---------- Ent

     A,B→C,C           C,C→D        A→C,D   C,D→D,C

    --------------------------- Comp  ------------------ Comp

            A,B→D                      A→D,C

          -------------------------------------- Prod

                      A,B,A→D,D,C

次に、図1を一部に埋め込んだ図2。図1をはめ込む部分が目立ち過ぎだわ。斜線とピンクでキタネー。

図2のプロファイルだけ：

                  ☆          ☆
 〜〜〜         ------- Ent ------ Ent
  図1           D,D→D       C→C
 〜〜〜         ------------------ Prod
 A,B,A→D,D,C       D,D,C→D,C
 ------------------------------- Comp
         A,B,A→D,C

ここまでで、もとの絵の左側ができました。念の為、もとの絵を再掲。

次は、右側のほうを作っていきます。アレッ、図3で、C, Dのスワップとiのラベルが間違ってる、直さん（描き直すの面倒だから）。

プロファイルだけなら（間違いは修正）：

   ☆
 --------- Ent
  C,D→D,C    D,C→A
 -------------------- Comp
       C,D→A
      --------- Lamb
       D→C⇒A

これで、絵の左側と右側が出来たので、Sumリーズニングで選言的に併置します。あのさー、ピンクの塊が目立ち過ぎなんだけど、、、なんでこんな描き方しちゃったかなー (後悔)。

以上で、絵の構成過程であるリーズニング図が出来上がりです。注釈の区切り線や囲み線が描いてあれば、最後の絵からリーズニング図を（ほぼ）一意的に再現できます。

これは、括弧付けをきちんとした式から構文解析木が一意的に構成できることと同じです。構文解析木については「整数式の構文解析木 (A4P3)」に解説と練習問題があります。ちなみに、今回の絵の“括弧付けをきちんとした式”は：

( ( ((f;dup_C);g) $\otimes$ (h;swap_C,D) );(codup_D $\otimes$ id_C) ) $\oplus$ ( Λ(swap_C,D;i) )

この式の構文解析木がリーズニング図なわけです。

プロファイルを調べてみると

プロファイルだけなら一枚の絵に書けるかな？できるだけ圧縮するため、Ent, Prod, Comp, Lamb を、E, P, C, L の一文字にして、空白も空けないで詰めます。



         ☆

       ------E

A,B→C C→C,C                  ☆

-------------C               -------E

 A,B→C,C     C,C→D  A→C,D C,D→D,C    ☆     ☆      ☆

 -------------------C ---------------C ------E ----E --------E

       A,B→D           A→D,C         D,D→D  C→C  C,D→D,C D,C→A

       -------------------------P      ------------P ---------------C

                      A,B,A→D,D,C     D,D,C→D,C       C,D→A

                      ---------------------------C      -------L

                             A,B,A→D,C                 D→C⇒A

これ、最下段を書いてません。最下段まで描くと、次のようになっちゃうのです。

   ：：：          ：：：
   ：：：          ：：：
 ------------    ---------
  A,B,A→D,C      D→C⇒A
 ----------------------------- Sum
      A,B,A | D → D,C | C⇒A

最下段の推論図（＝もとの推論図）のプロファイルに、カンマと縦棒の入れ子ができちゃうのです。括弧で包んでみると：

((A,B,A) | D) → ((D,C) | C⇒A)

こういう入れ子が、絶対にダメってわけじゃないのですが、リーズニングの計算を（極度に）複雑にしてしまうために禁止してます。もともと、推論図からリーズニング図に移行した動機が「計算が簡単になるから」*2なので、計算が複雑になる要因を許すと元も子もないのですわ。

対策として、図2のところを次の図2'のように修正します。

これは何をやっているのかと言うと；もとの図の左側のプロファイルが A,B,A → D,C だったのを、論理式のリストを単一論理式にしてしまうのです。

連言的リスト A,B,A を、単一論理式 A∧B∧C にする。
連言的リスト D,C を、単一論理式 D∧C にする。
すると、A∧B∧A → D∧C というプロファイルの推論図になる。

ゲンツェンの（オリジナルの）システムだと、基本リーズニングが20個以上あり、こういうことを一発で出来る基本リーズニングも最初から備えているのだけど、基本リーズニングを6個に減らしてしまったので、次のような手順が必要です。

 (A∧B)∧A→A,B,A  A,B,A → D,C        ☆
 -------------------------------C  ---------E
           (A∧B)∧A→D,C          D,C→D∧C
           ---------------------------------C
                   (A∧B)∧A→D∧C

このリーズニング図（のプロファイルのみ略記）の最上段左の (A∧B)∧A→A,B,A は、基本推論ではないので、これも次のようにして作る必要があります。

                             ☆         ☆
                         -----------E  ----E
         ☆              A∧B → A, B  A→A
 --------------------E  --------------------P
 (A∧B)∧A → A∧B, A   A∧B, A → A, B, A
 ------------------------------------------C
         (A∧B)∧A → A, B, A

基本リーズニングがたった6個じゃ不便だろう？って。いやっ、全然平気。マクロ・リーズニング（ユーザー定義のリーズニング）やマクロ推論（ユーザー定義の推論）をどんどん足していけば、システムの能力はいくらでも上がります。小さなコアのプログラミング言語でも、ライブラリで能力を足せるのと同じです。

僕が基本リーズニングを減らしている（代わりに基本推論がけっこう多い）のは、カリー／ハワード対応と圏論的意味論の観点を重視してるからで、趣味の問題とも言えます。