檜山正幸のキマイラ飼育記 メモ編 このページをアンテナに追加 RSSフィード

キマイラ・サイト
キマイラ飼育記 本編
メモ編のアーカイブ
檜山の公開プライベート(なんじゃそりゃ?)メモ
檜山本人以外の読者を考慮しておりません。あしからず。

hiyama{at}chimaira{dot}org

2009-02-28(土)

演繹系の話題と練習

| 17:28

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

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

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

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

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

算術 論理
定数リテラル 公理の論理式
変数 メタ変数
組み込み関数(基本演算) 基本推論ルール
マクロ マクロ(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 (含意)

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

公理か推論か、の例:

  1. (ref) x = x
  2. (symm) x = y ⊃ y = x
  3. (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とソックリだし。

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

考え中。