演繹系の話題と練習 - (保存用) 檜山正幸のキマイラ飼育記メモ編

演繹系（証明系）を、技術者の言葉で語ることが課題。まだ、いろいろと思案中だがね。

まず、基本的な態度あるいは視点としては；演繹系も計算システムであるので、通常のコンピュータシステムやプログラミング言語システム（言語処理系と実行環境）と同じだ！ということ。

算術のマクロ計算システム

最初に算術のマクロ計算システムを導入する。ユーザーが定義できるのはマクロだとして、マクロの使用と展開は自由に出来るとする。基本演算は組み込み関数で提供される。組み込み関数とマクロの区別は構文的にはしない（そのほうが便利）。あえてマクロとするのは、証明図との対応はマクロのほうが幾分自然だと感じるから。計算図＝計算回路図と証明図を対応させる。

算術のマクロ計算システムと論理的演繹系の対応は：

算術	論理
定数リテラル	公理の論理式
変数	メタ変数
組み込み関数（基本演算）	基本推論ルール
マクロ	マクロ（induced）推論ルール
マクロライブラリ	推論ルールのセット

マクロ定義は次のようにする



macro F x is
           x

  ----------------[Dup]

  x           x

 ----[Dup]

 x  x

 ------[*]

  x*x         x

 ----------------[+]  ---[Const]

     x*x + x           1

    ----------------------[+]

       x*x + x + 1

end

書式は：



macro 名前 引数変数並び（カンマ区切り） is 

 計算図

end

計算図は常に算術回路図と対応する。算術回路図のほうが簡明直接的で、計算図のほうが表現力も便宜性は劣るが、テキスト形式で記述できる点がメリット。

マクロの使用は



     3

   -------[F]

     13

とか

     x + y

  ------------------------------[F]

   (x + y)*(x + y) + (x + y) + 1

このマクロFは x*x + x + 1 を計算するが、マクロの場合はその場で展開されるので、f(x) = x*x + x + 1 という新しい関数（ブラックボックス）を定義したわけではない。略記（テキスト展開）という位置づけ。マクロは常に展開形を参照できる。証明では、展開形を参照できることが重要でブラックボックス化はしない。

マクロの入出力に関する言明は次の形に書く。

[F] x |- x*x + x + 1
[F] x + y |- (x + y)*(x + y) + (x + y) + 1
[F] 3 |- 13

これは、

F(x) = x*x + x + 1
F(x + y) = (x + y)*(x + y) + (x + y) + 1
F(3) = 13

と同じと考えてよい。。

計算システムが実際の評価（加減乗除の実行、デルタ変換）を持たず、単なる式の構成規則であれば、計算図が算術式を意味し、マクロは算術式の生成器（term froming operator）、あるいいは算術式の変換器（converter）となる。

懸案：記号計算と数値計算をどう分けるか、あるいは統合するか。マクロ展開は、あくまで図を変型するだけで、関数（演算）呼び出し＝デルタ変換はしない、とするか。

算術式のパーズは、パーズツリー＝計算図の再現になっている。論理でも、論理式をパーズしたら証明図が再現できればうれしい（が、できるかどうかは別問題）。

システム設計における論点

ハードウェアとソフトウェアの境界（インストラクションセット）
マイクロ（プア）カーネルかリッチ（ファット）カーネルか
言語の組み込み機能とライブラリの境界
標準ライブラリとユーザープログラミングの境界
関数にするか制御構造構文にするか

演繹系でも：

公理にするか定理にするか（公理の最小性を気にしないとして）
公理にするか基本推論規則にするか
基本推論にするかマクロ推論（ユーザー定義）にするか

組み込みにすれば高速だがコストがかかるし、基本部分のスリムさが失われる。かといって、あまりにプリミティブな基本機能だけでは使い勝手が悪い。

ライブラリが充実すれば便利だが、大きなライブラリは記憶が大変。重複機能も増え、選択に悩む。小さなライブラリではユーザーの負担が大きい。

事例

等式的理論、項は多変数の多項式（算術式）、定数は有理数リテラル、論理式は：

等式（原子論理式、基本論理式）
P∧Q （連言）
P⊃Q （含意）

注意：マイナス記号の扱いは構文的には煩雑。

公理か推論か、の例：

(ref) x = x
(symm) x = y ⊃ y = x
(tran) x = y ∧ y = z ⊃ x = z

推論ルール（シェマ、パターン）なら：



   A = B

  ------[Symm]

   B = A
   A = B,  B = C

  ---------------[Tran]

     A = C

置換ルールの例



/* 2つのルール */
      A  = B

  ----------------[両辺に同一置換]

  A[C/x] = B[C/x]


     A =  B

  ---------------[1つの項に左右で置換]

  C[A/x] = C[B/x]



/* 1つのルール */
   A  = B    M = N

  ----------------[置換]

  A[M/x] = B[N/x]

練習問題：移項（transposeだが、transitive lawと紛らしいからラベルMoveがいいか）をマクロ規則として導入するにはどうしたらいいか？

注意：1 + 1 = 2 のような定数の計算結果は、すべて公理に入っているとすべきだろう。デルタ規則といってもよさそうだ。あるいは、変数なしの論理式（文）にはオラクル判断してよい。

演繹原理

演繹原理（定理つうより原理）が一番難しそうだ。

「仮定＝仮の前提」を結論に繰り込むこと
集合の包含関係を、「集合が全体に一致すること」に帰着させる

という説明が可能か？ただし、包含関係を持ち出すには、「解＝モデル」の説明が必要だ。

恒等式（公式）と方程式の違いとしても説明可能かも？

|- P のとき、Pは恒等式
P |- Q のとき、Pは方程式でQは解の記述

とはいえ、PよりQが単純化されている保証は全然ない。x = 1 ∧ y = 2 |- x+y = 3 。「方程式を解く」の定義があまりハッキリしない。正規系（あるいは被約系）を決めて、Qが正規系のとき「解けた」とするか。

懸案：trueとfalseの扱いを、連立方程式の文脈で説明するか。

証明図の描き方

横線を使う方式は普通どおり。ワイヤーを使うバージョンは、

∧導入は黒く塗った四角つうか、太く短い横棒
モダスポネンスはオダンゴ
公理は三角、オダンゴでもいいのだが、公理であることを強調
⊃導入は、ワイヤーをつなぐ、適当に交差させてレイアウト
構造規則として換（公差、クロス）と、増（重複、コピー）

横線方式の「⊃導入」は、消える仮定に番号（ラベル）を付けて、対応する推論にも同じ番号を付ける。

懸案：明白な分岐（並列処理） A∧B |- A, B を入れたほうがいいか？あるいは、構造規則として離（分離）とか合（合流）を入れるとか。並行処理＝モノイド積を入れるなら、分岐（フォーク）がないとおかしいな。どこで入れるか？ A |- A, A を分岐にするか、Unixのforkとソックリだし。

並列処理、データフロー計算との関係

考え中。