問題集1の目的と解答と追加説明重要！ (A13R1) - (保存用) 檜山正幸のキマイラ飼育記メモ編

※この記事は「記事13 解答1」

「だ・である調」から「です・ます調」に変更します。

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

ノード・ワイヤー図と横棒記法の例と練習 (A2P1)

解答だけでなく、「どうしてこのような練習をするか？」や、関連する事項の説明もします。

内容：

この問題は重要
解答
形式化された証明のだいたい

この問題は重要

「ノード・ワイヤー図と横棒記法の例と練習 (A2P1)」の問題は、証明の形式化の準備として最も重要な問題です。もしまだやってなかったら、是非にやってみてください。

「ノード・ワイヤー図と横棒記法の例と練習 (A2P1)」にも書いておいたように、こういう練習をしておかないと、証明の形式化がまったくピンと来ないでしょう。

形式化とは、我々生きている人間が現実世界で扱っているモノや行っているコトを、コンピュータでも扱えるデータやコンピュータでも実行できるアルゴリズムとして再定義することです。（次も参照。）

ともかくシーケントなんだから、頼むよ、皆んな (A12) // 形式化とシーケント

形式化された証明とは、ある種のデータをある種の基本コマンドだけで操作していく一連の過程です。コンピュータで動く演繹システムは、そのような過程を遂行することにより、人間の知的行為である証明をシミュレートします。ソフトウェアシステムではなくて、理論的に構築された概念的演繹システムでも事情は同じです。

我々は、演繹システムの挙動や能力を外から観測して調べるのですが、内部動作をある程度は自分で経験しておかないと、何の実感も湧かないでしょう。例えば、掛け算を遂行する電子回路の仕組みを理解するとき、自分自身はまったく掛け算した経験がないと無理がありますよね。

それと、竹内外史先生の言葉を思い出しましょう。

[論理／数学基礎論を]理解するに多大な煩わしさを経なければならない。

この「多大な煩わしさ」を事前に実感し、煩わしさに対する慣れと耐性を身につけるようにしましょう。

以下に解答です。解答の後に、より具体的な説明が書いてあります。

解答

Ins, Del, Fork, Merge, Add, Mult の操作だけを用いて、二元連立一次方程式 {2x - 3y + 1 = x - 2, x + y = 5} を解け。

解き方は色々ありますし、それらに優劣はありません。ここに書くのはあくまで一例です。

方針としては、2つの流れに分岐して、左側の流れでxを求め（yを消去し）、右側の流れでyを求めます（xを消去します）。テキストで書くのを楽にするため、左側と右側の操作が同じになるようにしました。中間で使った不要な等式を消して、最後に合流します。

「ノード・ワイヤー図と横棒記法の例と練習 (A2P1)」の最後の追記で述べたような略記を使います。

(1) 2x - 3y + 1 = x - 2
(2) x + y = 5
-------- Ins(-x - 1)
(1), (2)
(3) -x = -x
-------- Add(#1,#3)
(1) x - 3y = -3
(2) x +  y =  5
(3)
-------- Fork
(1),(2),(3)           (1),(2),(3)
-------- Ins(3)       -------- Ins(-1)
(1),(2),(3)           (1),(2),(3)
(4) 3 = 3             (4) -1 = -1
-------- Mult(#2, #-1)-------- Mult(#2, #-1)
(1) x - 3y = -3       (1) x - 3y = -3
(2) 3x + 3y = 15      (2) -x - y = -5
(3),(4)               (3),(4)
-------- Add(#1, #2)  -------- Add(#1, #2)
(1) 4x = 12           (1) -4y = -8
(2),(3),(4)           (2),(3),(4)
-------- Ins(1/4)     -------- Ins(-1/4)
(1) 4x = 12           (1) -4y = -8
(2),(3),(4)           (2),(3),(4)
(5) 1/4 = 1/4         (5) -1/4 = -1/4
-------- Mult(#1, #-1)-------- Mult(#1, #-1)
(1) x = 3             (1) y = 2
(2),(3),(4),(5)       (2),(3),(4),(5)
-------- Del(#-1)     -------- Del(#-1)
(1),(2),(3),(4)       (1),(2),(3),(4)
-------- Del(#-1)     -------- Del(#-1)
(1),(2),(3)           (1),(2),(3)
-------- Del(#-1)     -------- Del(#-1)
(1),(2)               (1),(2)
-------- Del(#-1)     -------- Del(#-1)
(1) x = 3             (1) y = 2
-------- Merge
(1) x = 3
(2) y = 2

横棒記法による図をノード・ワイヤー図にせよ。

描画方向は、先の横棒記法の図をそのまま写し取った↓→（上から下、左から右）です。

前問のノード・ワイヤー図を、すべての描画方向（↑→, ↑←, ↓→, ↓←, →↑, →↓, ←↑, ←↓）で描いてみよ。

この解答は省略しますが、このテのトレーニングが必要なことは、次の記事をザッと眺めてみてください。内容を理解する必要はありません。眺めるだけ。

双対や随伴に強くなるためのトレーニング

前問のノード・ワイヤー図をテキスト記法で表現せよ。

Ins(-x - 1);Add(#1,#3);Fork;(Ins(3) $\otimes$ Ins(-1));(Mult(#2, #-1) $\otimes$ Mult(#2, #-1));(Add(#1, #2) $\otimes$ Add(#1, #2));(Ins(1/4) $\otimes$ Ins(-1/4));(Mult(#1, #-1) $\otimes$ Mult(#1, #-1));(Del(#-1) $\otimes$ Del(#-1));(Del(#-1) $\otimes$ Del(#-1));(Del(#-1) $\otimes$ Del(#-1));(Del(#-1) $\otimes$ Del(#-1));Merge

[追記 date="2018-12-07"]↑最後のMergeが抜けていたので追加。[/追記]

ひとつの図に対するテキスト記法も、ひと通りではありません。図のクラスター分割〈ブラケティング〉により、対応するテキスト記法も変わります。このことについては、「ノード・ワイヤー図〈ストリング図〉 (A1) // グルーピング〈ブラケティング〉と描き換え」をもう一度見てください。

もし可能なら、…

これは実際にやってみる話。「自分以外の人」の代わりに「時間がたった自分」でやってみるとよいでしょう。

解き方（出来上がる図）は一通りではない。違った解き方も考えよ。

唯一の正解はないので、他もやってみてください。

適当な二元連立一次方程式に対して、上の問題群と同じ作業を行え。

必要があれば追加の練習をしましょう。

形式化された証明のだいたい

二元連立一次方程式 {2x - 3y + 1 = x - 2, x + y = 5} を解く一連の過程を図示したノード・ワイヤー図〈ストリング図〉では、等式系（縦に等式を並べたもの）をラベルするのは煩雑なので省略しました。省略しないで、等式系も記入すると次のようになります。

四角の枠は、ノードではなく、ワイヤーラベルを記入するための枠です。これを、ラベルフレーム、または単にフレームと呼びます。ノードは水色に塗ってあります。

ノードラベルがテキストではなくて再びノード・ワイヤー図であれば、例えば（単なる一例）、次のような図になるでしょう。

今、この図を理解する必要はありません。しかし、次のことは知っておいてください。

形式化された証明を分かりやすく図示するには、この程度の絵が必要になる。これでも、相当に省略していて、もっと細部を描き込むとさらに複雑になる。
良心的な著者・編集者・出版社が、十分なゼニ（予算）をかければ、このような絵をふんだんに使った教科書を作れるだろう。
さらに十分なゼニ（予算）があれば、ラベルフレームをアニメーションのフレームとした、マルチスクリーン（同時に複数のシーンを映し出す）アニメーションムービーを制作できるだろう。
さらにもっとゼニ（予算）があれば、アニメーションムービーの制作環境や対話的な再生環境（プレイヤー）も作れるだろう。
現実には、それだけの手間・コストをかけることは、ほぼ不可能。

次善の策として、横棒記法を使ってみます。

ラベルフレーム内の黄色のノードは一本棒の横線にする。
水色のノードは二本棒の横線にする。
何も描いてない白いフレームは☆で示す。

              ☆
            ====== 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)

入れ子の内側の横棒記法の図をシーケント形式（「シーケントに親しもう (A11P9)」参照）に直せば、横幅が広がりますが、縦方向は節約できます。

                                  ☆
                         ================== 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)

さらに実際に使われている図では：

一本棒をもう使ってないので、二本棒を一本棒にする。
☆のようなマーカーは置かないで空白にする。
→ の左にTだけがあるときは、何も書かない。（この規則は、リストの種類を明示的に示す我々の流儀では使えない。）

他にも、絵の情報（幾何的／グラフ理論的な情報）を、イラストなしの通常文字組版で印刷可能にするための工夫が色々とあります。しかし、そのような制約と工夫（苦し紛れの方便）が、本来は簡単なものを、非常に煩雑にしてしまっている事実があります。興味があれば、次の本編記事も参照してください。

アニメーションとしての証明