このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

スパイダーパズル (A17P10)

RSS練習問題

※この記事は「記事17 問題集10」

この記事の問題をやれば、形式化された証明や演繹システムに対して、（詳細はともかくとして）かなりの程度のイメージが持てると思います。問題の解答例は、早めに（たぶん次回）出す予定です。[追記]解答はこちら → 問題集10の目的と解答と追加説明 (A19R10)[/追記]

内容：

  1. 必要な知識とスキル
  2. ノード・ワイヤー図のプロファイル
  3. スパイダー
  4. 汎用のスパイダー
  5. スパイダーの構成問題
  6. 構成可能性／構成不可能性定理
  7. スパイダーパズル

必要な知識とスキル

ノード・ワイヤー図〈ストリング図〉について知っている必要があります（次の記事）。

ノード・ワイヤー図の実例や操作にある程度は慣れている必要があります。次の練習問題はやっている（やったことにより獲得できるスキルを持っている）と仮定します。

次の練習問題もやってあると望ましいです。（必須とは言わないが。）

以下もやってあれば、申し分ないです。

ノード・ワイヤー図のプロファイル

ノード・ワイヤー図〈ストリング図〉は、↓→の描画方向で描くとして、一番上に現れるワイヤーラベルの並び〈リスト〉を入力列と呼びます。同様に、一番下に現れるワイヤーラベルの並びを出力列と呼びます。そして、「カンマで区切った入力列 → カンマで区切った出力列」という形を、ノード・ワイヤー図のプロファイル〈profile〉と呼びます。

形の上では、プロファイルはシーケントと同じ形になります。実際、シーケントはプロファイルとしても使われるのですが、今回は、シーケントを忘れても（知らなくても、思い出さなくても）いいです。

次の図（「ノード・ワイヤー図〈ストリング図〉 (A1)」で出した図）のプロファイルは、A, X → C, Y です。

  A
 ---f
  B    X
 ---g ---u
  C    Y

次の図（「整数式の構文解析木 (A4P3)」で出した図）のプロファイルは、x, y → yy + xx です。

   x           y
 ----- dup   ----- dup
  x  x        y  y
 ------ prod ------ prod
   xx         yy
  --------------- swap
   yy    xx
  ---------- sum
   yy + xx

ノード・ワイヤー図のワイヤーラベルはいくらでも複雑になりえます。ラベルが再び絵図になることもあります。例えば、「問題集1の目的と解答と追加説明 重要！ (A13R1)」で出した次のノード・ワイヤー図（の横棒記法による表現）がその例です。

              ☆
            ====== Ent
             A  B       A∧B
             ----γ    -----
   ☆        A∧B        C
 ====== Ent ================= Comp
  B  A          A  B
  ----σ        -----
  A  B           C
 ===================== Comp
         B  A
        -----
          C
      ========= Lamb
          A
        ------
         B⇒C
      ========= Ins(up 1, T)
         A T
        ------
         B⇒C
      ========= Lamb
          T
       ---------
       A⇒(B⇒C)

こういう図のプロファイルは、1行のテキストではどうにもならないので、例えば、

         A∧B             T
☆, ☆, ------ ＝＝＞ ---------
          C           A⇒(B⇒C)

繰り返し言いますが、テキストでは表現しにくいものを無理にテキストで表現しようとすることで、（無駄な）難解さが生み出されています。それは承知の上で、無理に書けば：

  • 上の図のプロファイルは、 ☆, ☆, (A∧B → C) =▷ (T → A⇒(B⇒C))

※注意： 星（☆）は、何もないことを表すマーカーなので、通常は星を省略して、(A∧B → C) =▷ (T → A⇒(B⇒C)) をプロファイルとします。

矢印が三種類も出てきています。

  1. '⇒' は、含意を表す論理記号
  2. '→' は、横棒の上下を左右で表すための矢印
  3. '=▷' は、プロファイルにおける入力列と出力例を区切る矢印

論理では、ほんとにイッパイ矢印が出てきます。興味があれば本編記事：

さて次は、「問題集1の目的と解答と追加説明 重要！ (A13R1)」で出した、連立方程式を解く過程の図（省略部分あり）。

         2x - 3y + 1 = x - 2
         x + y = 5
       ---------------------- Ins(-x - 1)
         2x - 3y + 1 = x - 2
         x + y = 5
         -x - 1 = -x - 1
       -------------------- Add(#1,#3)
         x - 3y = -3
         x +  y =  5
         -x - 1 = -x - 1
  ---------------------------------- Fork
   x - 3y = -3       x - 3y = -3
   x +  y =  5       x +  y =  5
   -x - 1 = -x - 1   -x - 1 = -x - 1
  〜〜〜〜〜〜〜〜   〜〜〜〜〜〜〜〜〜
  〜〜〜〜〜〜〜〜   〜〜〜〜〜〜〜〜〜
    x = 3             y = 2
   -------------------------- Merge
            x = 3
            y = 2

これのプロファイルは、次のように書けば伝わるでしょう。

  • 上の図のプロファイルは、 {2x - 3y + 1 = x - 2, x + y = 5} → {x = 3, y = 2}

今まで出たプロファイルの書き方は、色々です。



A, X → C, Y
x, y → yy + xx
         A∧B             T

☆, ☆, ------ ＝＝＞ ---------

          C           A⇒(B⇒C)
☆, ☆, (A∧B → C) =▷ (T → A⇒(B⇒C))
{2x - 3y + 1 = x - 2, x + y = 5} → {x = 3, y = 2}

書き方というものは（困ったことには）、歴史的経緯とかその他諸々の事情で、根拠も節操もなく多様化（膨大な方言が発生）してしまいます。そのような無駄な多様性／迷惑な多様性に慣れる必要があります。記号に振り回されるのではなくて、記号を操る立場になりましょう。次の記事にトレーニング用問題があります。

スパイダー

ノード・ワイヤー図のノードのことをスパイダー〈spider〉とも呼びます。ノードとスパイダーは完全に同義語です。あえて同義語を新しく導入するにはいくつかの理由があります。

「ノード」というと、グラフ理論におけるグラフのノードのように、ワイヤー（辺）から切り離した単なる点としても存在できる印象がありますが、そうではありません。ノード・ワイヤー図のノードは、ワイヤー（の一部）と分離不可能です。点やアイコンというよりは、電子デバイスを思い浮かべてください。

*1

電子デバイスには脚が生えており、脚もデバイスの一部です。脚がないデバイスはどことも接続できません。同様に、ノード・ワイヤー図のノードには、入るワイヤーと出るワイヤーが脚としてくっついているのです。このことを強調するために、ノードをスパイダーとも呼ぶことにします。蜘蛛〈スパイダー〉の脚をもぎ取ったら死んでしまうでしょう、そんな可哀想なことをしてはいけません！

実は、用語「スパイダー」は用語「ノード・ワイヤー図」とも同義です。奇妙に感じるでしょうが。

図の左のようなスパイダー a があったとします。そのプロファイルは A, B, C → B, D です。しかし、a は実際はクラスターであり、図の右のように、内部に s, t, u が入っているとします。右側は、全体として名前'a'で識別されるノード・ワイヤー図です。

ノードは、それ以上は分解できない〈原子的 | 基本 | 原始的 | アトミック | プリミティブ〉ノードとは限りません。他のノード達から構成されるクラスターかも知れません。よって、「ノード」「クラスター」「ノード・ワイヤー図」をちゃんと区別するのは不可能なのです。

用語「スパイダー」は、「ノード」「クラスター」「ノード・ワイヤー図」のどれの意味でも使用し（もともと区別がないんだし）、特に分解不可能（と想定する）ならば基本スパイダー〈primitive spider〉と呼びます。

汎用のスパイダー

ノード・ワイヤー図を描くとき、たいてい（常にとは言ってない）使ってよい汎用の基本スパイダーがあります。

左から、

  1. Xの恒等〈identity〉
  2. Xの複製〈duplication〉
  3. XとYの入れ替え〈swap〉

これらもりっぱなスパイダーですが、ノードのアイコンは描かずに、ワイヤー／ワイヤーの分岐／ワイヤーの交差 として描きます。

ここで使っている文字'X', 'Y'は、具体的なワイヤーラベルではなくて、勝手なラベルに置き換えてよいパラメータです。具体的なラベルではないパラメータを持つスパイダー〈ノード・ワイヤー図〉は総称スパイダー〈総称ノード・ワイヤー図〉と呼びます。ちなみに、「汎用」も「総称」も"generic"の訳語です。

※注意： id, dup, swap以外に、discと書かれる「入力を捨ててしまう操作」もよく使われる汎用スパイダーです。id, dup, swap, discは、象形文字で、I, X, 人, ! とも書かれます。象形文字については、「整数式の構文解析木 (A4P3) // IXY記法」、「単純式の操作の操作 (A5P4) // 例題」にも象形文字が登場します。

今述べた id, dup, swap のように、最初から使ってよいと約束した総称パイダーを基本総称スパイダー〈primitive generic spider〉と呼びます。

念の為、言葉の注意をしておくと：

  • 「汎用」と「総称」はどちらも"generic"の訳語で同義。
  • 「基本」の代わりに、「原始」、「原子」、「組み込み」なども使う。

いちいちは注意しないでしょうが、ほとんど常に、山のような同義語・類義語があります。

スパイダーの構成問題

次のようなスパイダーのセット {a, b, c, d} があるとします。

これらのスパイダーを分解する気はないので、a, b, c, d は基本スパイダーと考えます。
問題： これら基本スパイダーと基本総称スパイダー（前節）を素材として、結合（演算子記号は';'）と併置（演算子記号は'\otimes'）により、次のプロファイルを持つスパイダー〈ノード・ワイヤー図〉を構成してください。ただし、構成できる保証はありません。解答の形式はすぐ下の例題を見てください。

  1. B, A → A
  2. B, A → B
  3. B, A → C
  4. A → A, B
  5. B → A, B
  6. C → A, B
  7. C, C, B → A, A
  8. B, B → A, A

例題： A, B, B → A, A, B というプロファイルを持つスパイダーを構成せよ。

要求されているプロファイルを持つスパイダーを横棒記法の図で書けば：

   A  B       B
  ------ a ------ b
    A       B  A
  ---- id  ------ swap
    A       A  B

このスパイダーが構成される過程を書けば：

    ☆        ☆             ☆          ☆
  ====== Ent ===== Ent      ===== Ent  ====== Ent
   A  B        B              A         B  A
  ------ a   ----- b         --- id    ------ swap
    A         A  B            A         A  B
  =========+========= Prod  =========+========= Prod
     A  B      B                A      B  A
    ------ a ----- b           --- id ------ swap
       A      B  A              A      A  B
   ======================+======================= Comp
                  A  B       B
                 ------ a ------ b
                   A       B  A
                 ---- id  ------ swap
                   A       A  B

ここで、

  • Ent ： Enter -- 基本スパイダー（総称スパイダーの具体化も含む）を登場（入場）させる。
  • Prod ： Product -- スパイダーの併置（直積ともいう）を作る。
  • Comp ： Composition -- スパイダーを結合する。

併置〈直積〉を表す演算子記号'\otimes'を使ったほうが分かりやすいかも知れません。



    ☆        ☆             ☆          ☆

  ====== Ent ===== Ent      ===== Ent  ====== Ent

   A  B        B              A         B  A

  ------ a   ----- b         --- id    ------ swap

    A         A  B            A         A  B

  =========+========= Prod  =========+========= Prod

       A  B   B                  A   B  A

      ------------ a\otimesb         ---------- id\otimesswap

       A   B  A                  A   A  B

   ======================+======================= Comp

                      A  B  B

                     --------- a\otimesb

                      A  B  A

                     --------- id\otimesswap

                      A  A  B

出来たスパイダー（上の図の最下段）をテキストの式で書けば：

  • (a\otimesb);(id\otimesswap)

なお、横棒記法よりは入れ子のノード・ワイヤー図のほうが望ましいです。描くのがめんどくさいけど、圧倒的に望ましいです。是非に描いてみてください。入れ子のノード・ワイヤー図の例は、次のアンカー〈リンク〉をクリックしてください。

描き方の説明は：

最も基本的なことは：

結局、この節冒頭の問題の解答は、次の3つの形式をすべて書いて（描いて）ください。

  1. （もしあれば）目的のスパイダーのノード・ワイヤー図
  2. 目的のスパイダーを作る過程を描いた入れ子のノード・ワイヤー図
  3. 目的のスパイダーのテキスト表現

問題： 構成できるものに関しては、もうひとつ別なスパイダー（別ならなんでもいいです）も作ってください。

構成可能性／構成不可能性定理

プロファイルを勝手に指定されたときに、そのプロファイルを持つスパイダーが構成できるとは限りません。構成できないときもあります。しかし、「頑張ったけれども構成できなかった」では、構成不可能性は言えません。「これこれのタイプのプロファイルに対しては、スパイダーを構成できない」という定理を示せば構成不可能性が言えます。

一方、「これこれのタイプのプロファイルに対しては、スパイダーを必ず構成できる」という定理があれば、実際に構成しなくても構成可能性が言えます。

前節の設定で、次の定理が成立します。

  1. 構成不可能性定理： プロファイルの形が Γ → B であるプロファイルに対して、スパイダーは構成できない。ただし、Γは、A, B, C からなるリストで、B（単一のB）ではない。（[追記]←Γに関する条件が抜けていたので追記した。[/追記]）
  2. 構成不可能性定理： プロファイルの形が Γ → Δ で、リストΓ内にBが出現せず、リストΔ内にBが出現するとき、このプロファイルに対してスパイダーは構成できない。（[追記]この定理は変更しました。「スパイダーの構成不可能性定理を変更 (A18)」を参照。[/追記]）
  3. 構成可能性定理： プロファイルの形が B → Δ で、ΔはAとCから構成されるリスト（非空でBは含まないリスト）のとき、このプロファイルに対してスパイダーは構成できる。

問題： これらの定理を証明せよ。

これは、ごく普通の問題で、ごく普通の証明を書けばいいのです。形式化した命題や、形式化した証明ではなくて、今までどおり、いつもどおりの自然言語で書かれた通常の証明を要求しています。

スパイダーパズル

前々節の問題のように、プロファイルを与えて、そのプロファイルを持つスパイダーを構成する問題をスパイダーパズル〈spider puzzle〉と呼びましょう。ちょっとピクチャーパズル（ジグソーパズル）と似てます。

*2

ピクチャーパズルと同様に、使ってよい素材〈ピース〉のストックと、組み合わせ方のルールがあります。前々節のスパイダーパズルのルールは：

  1. id, dup, swap という総称スパイダーを具体化して素材として使ってよい。
  2. a, b, c, d という4つのスパイダーは素材として使ってよい。
  3. 併置により組み合わせてよい。
  4. 結合により組み合わせてよい。

ルールは、いくらでもカスタマイズできます。決めるべきは：

  1. 使ってよい基本スパイダー（総称と総称ではないもの）のセット
  2. 使ってよい組み合わせ方のセット

スパイダーパズルの遊び方は、ピクチャーパズルとは違って：

  1. 出題者が、プロファイルを指定する。
  2. 解答者が、そのプロファイルを持つスパイダーを構成しようと頑張る。

当然に、解答者は最初に決めた素材と組み合わせ方の範囲内で構成を行います。ルールを守らないとダメです。

形式化された証明は、スパイダーパズルと同じ構造を持ちます。素材や組み合わせ方がもっと複雑になるだけです。人間が現実世界で行っている証明という行為を、ルールを持つパズル（ゲーム）として定式化して、それをコンピュータ上で動くソフトウェアシステムとして実現可能なほどに明確にしよう、ということです。必然的に、証明を行ったり助けたりするソフトウェアはゲームソフトに近くなります（「業務ソフトまたはゲームソフトとしてのCoq （誰も書かないCoq入門以前 2）」参照）。

*1:画像： https://www.mitsuiwa.co.jp/product/list/msview/device/ より

*2:画像： https://www.mudpuppy.com/collections/puzzles より