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

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2017-10-18 (水)

巨大ロボットバトルの興行は成立するか?

| 16:53 | 巨大ロボットバトルの興行は成立するか?を含むブックマーク

水道橋重工 vs MegaBots の巨大ロボットバトル:

D

  • 第1戦は Iron Glory (MK2) vs Kuratas : Kuratasがパンチ一撃でIron Gloryを横倒しにして勝利
  • 第2戦は Eagle Prime(MK3) vs Kuratas : Eagle PrimeがチェーンソーでKuratasを切り裂きにかかり ……

巨大ロボットは、多くのマンガ・アニメ・映画に描かれた題材ですが、僕が思い出したのは、『リアル・スチール』。リアル・スチールの世界では、ロボット格闘技がスポーツ・エンタテインメントとしてビジネスになっています。

水道橋重工 vs MegaBots のバトルは、観客無しで行われて、撮影された動画が公開されているだけです。安全面などを考慮してのことでしょう。観客とパイロットの安全が担保されて、ルールが整備されれば、興行として成立するのかな?

一試合を行う準備にけっこうな資金と労力がかかりそうだし、試合でロボットが壊されること考えると、ちょっとペイしない気もしますね。戦闘用ロボットを量産して、一定の範囲内のカスタマイズとパイロットの腕前を競う、ならコストを抑えられか。あるいは、ロボット企業が自社製品の技術をアピールする場として、広告のために参戦するとか。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171018

2017-10-16 (月)

証明の“お膳立て”のやり方 5: 証明可能性判断と推論規則

| 14:19 | 証明の“お膳立て”のやり方 5: 証明可能性判断と推論規則を含むブックマーク

このシリーズのひとつ前の記事「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」の「前提の命題を推論法則として使う」において、証明可能性判断と推論規則を同義語のように使ったのですが、これはミスリーディングかも、と思うので補足します。

内容:

  1. メタな立場と証明可能性判断
  2. 推論規則と証明可能性判断
  3. 仮定の命題を推論規則に変換して使う

メタな立場と証明可能性判断

証明を実行する主体であるあなた、あなたが行う証明行為、そのときのあなたの頭の中などを外から観察している超越的存在がいるとします。手っ取り早いのは、超越的存在として神様を想定することです(「論理を身に付けるには」参照)。

上記のような、証明行為を外から眺める超越者は、メタなヤツと言えます。メタなヤツによる観察や主張はメタな立場からなされます。そういうメタな立場からの発言として証明可能性判断(provability judgement)があります。

  • P1, ..., Pn |- Q

メタな立場から、行為主体(コイツと呼ぶ)の証明行為を眺めて、「コイツは確かに、P1, ..., Pn からQを証明しているぞ」と発言している、あるいは保証しているのが証明可能性判断です。

我々人間は、証明可能性判断を発言できるメタな立場に立つことができるでしょうか。ある状況では、ハッキリとメタな立場に立てます。あなたが、証明を実行するソフトウェアの実装者であり利用者でもあるとします。あなたは、証明を実行するソフトウェアの挙動を外から観察できるし、その動作のメカニズムも理解しているでしょう。そして次のような発言ができます。

  • 「このソフトウェアは確かに、P1, ..., Pn からQを証明しているぞ」

生きている人間であれ、ソフトウェアであれ、抽象的・概念的な仕掛けであれ、証明を行うようなシステムは演繹系(deductive system; 証明系、論理系、推論系)と呼びます。証明可能性判断は、演繹系を外から眺めて記述するときの命題(メタな立場の命題なのでメタ命題)です。

演繹系の性質は、結局はメタ命題=証明可能性判断により記述されるので、もとの演繹系の研究が、証明可能性判断の体系の研究に移ってしまうことになります。対象物である演繹系と、外側にある証明可能性判断の体系を一緒に扱うべきだ、といった話になります。

今言ったことは、数理論理学や形式的体系の方法論というだけではなくて、普通の非形式的(半形式的)証明の場合にも適用されるのです。我々は、ほとんど無意識にメタな立場を使っています。証明ソフトウェアに対してメタな立場に立つだけでなくて、自分自身に対してもメタな立場に立つことがあるのです。このシリーズで話題にしている“証明のお膳立て”も、メタな立場からの発想だと言っていいでしょう。「自分自身に対してもメタな立場に立つ」現象の不思議さに付いては次の記事で述べています。

推論規則と証明可能性判断

「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」の「前提の命題を推論規則として使う」では、推論規則と証明可能性判断を同じ形で書きました。同じ形で書いて差し支えないですが、厳密には、推論規則と証明可能性判断は別物です。

推論規則とは、その名のとおり、どのような推論が可能かを書き下したものです。例えば、命題Pが証明済み、命題Qも証明済みのとき、連言命題P∧Qを導いてかまいません。これは次のように書けます。

     証明済みの命題  P    Q
 -----------------------------[推論のステップ]
 推論で導出された命題 P∧Q

縦の図式を横1行で書けば、

  • P, Q |- P∧Q

これは証明可能性判断と同じです。

推論規則と証明可能性判断が違う点は、推論規則が演繹系の内部にあり、証明可能性判断は演繹系の外にあることです。

今我々はメタな立場ではなくて、地面を這いつくばってひたすら証明作業に従事しているとします。そのときでも、推論規則は見えています。見えてないと作業ができないので、推論規則は地面にあるのです。それに対して、我々を上空から(文字通り上から目線で)観察している超越者の発言(つぶやきやナイショ話かも知れない)を、地上の我々は知ることができません。

仮定の命題を推論規則に変換して使う

論理学では通常、証明の最中に演繹系を変化させることはしません。しかし、我々が実際に行う証明行為(リーズニング)では、必要なら推論規則を足していくことは普通です。そのことを「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」の「前提の命題を推論規則として使う」で述べたかったのです。

混同と混乱を避けるために、推論規則を横書きにしたものは、次の形で書くことにします。

  • Γ/ Δ |-! P

ビックリマークを付けています。'|-?'と'|-!'だとバランスがいいかな、と思って。

推論規則はビックリマーク付きで書く、という約束で「証明の“お膳立て”のやり方 4: 随伴による集合差の定義」で述べたお膳立てを書き直しましょう。

  Γ/ ∀x∈X.(P(x)⇒Q(x)), Δ |-? R
 ---------------------------------------------[前提を推論規則に]
  Γ/ Δ |-? R     Γ/ (x : X), P(x) |-! Q(x)

右下の Γ/ (x : X), P(x) |-! Q(x) は推論規則なので、次のように解釈します。

  • Γは文脈(予備知識、背景知識)。
  • (x : X) と P(x) は既に証明済みで、得られている。
  • この状況で、推論の1ステップの結果として、Q(x)を結論してよい。Q(x)は証明済みとなる。

これは超越者が上空(メタな立場)で言っていることではなくて、地上の作業者が利用してよい手順です。

証明の“お膳立て”のやり方 4: 随伴による集合差の定義」で出した具体例を再掲すると; 証明要求は次です。

  • Γ/ ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T), (x : X), x∈S, ¬(x∈W) |-? x∈T

前提に、命題 ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T) が含まれます。これを推論規則に直すと:

  • Γ/ (x : X), x∈S, ¬(x∈W) |-! x∈T

したがって、もとの証明要求は、新しい証明要求と新しい推論規則に分解されます。

  1. 新しい証明要求 : もとの証明要求の前提から ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T) を除いた*1証明要求
  2. 新しい推論規則 : ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T) を推論規則に直したもの

具体的には、

  1. Γ/ (x : X), x∈S, ¬(x∈W) |-? x∈T
  2. Γ/ (x : X), x∈S, ¬(x∈W) |-! x∈T

要求のほうが「… を(可能なら)証明せよ」であるのに対して、推論規則が「… は1ステップ推論で証明済みとしてよい」と保証しているので、実質的な作業は何もしなくても、「証明できました」と納品(「証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル』参照)できます。

*1:前提の命題を取り除かなくても問題は起きないのですが、同じ知識が二重にエンコードされる冗長性を排除するために取り除いています。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171016

2017-10-14 (土)

証明の“お膳立て”のやり方 4: 随伴による集合差の定義

| 10:02 | 証明の“お膳立て”のやり方 4: 随伴による集合差の定義を含むブックマーク

証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル」において、証明要求のターゲットに選言(論理OR)が入る場合に触れました。しかし、説明が不十分だったので補足します。また、前提に含まれる命題を推論規則として使う方法も説明します。

例題は、タイトルにある「随伴による集合差の定義」です。これは、それ自体としても面白い話題です。

内容:

  1. ターゲットに選言が含まれる証明要求のお膳立て
  2. 前提の命題を推論法則として使う
  3. 例題: 随伴による集合差の定義
  4. ターゲットが選言の場合のお膳立て
  5. 仮定を推論規則として使う
  6. バックワード・リーズニングによる証明

ターゲットに選言が含まれる証明要求のお膳立て

次の証明要求を考えます。(この書き方に対する詳細は、「証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル」を参照。)

  • Γ/ Δ |-? P∨Q

ここで、Γは論理式の集まり*1で、文脈(予備知識、背景知識)と呼びます。Δも論理式の集まりで仮定です。'|-?'の右側がターゲットで、2つの命題の選言の形です。この証明要求に応えるには、次の証明要求のどちらか一方に応えればいいのでした。

  1. Γ/ Δ |-? P
  2. Γ/ Δ |-? Q

しかし、選言の場合に証明要求を2つに分けるのはうまくいかないことが多いです。

証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル」の追記で、次の方法を紹介しました。

  Γ/ Δ |-? P∨Q
 -------------------------[同値]
  Γ/ Δ |-? ¬(¬P∧¬Q)
 -------------------------[背理法]
  Γ/ Δ, ¬P, ¬Q |-? ⊥

この書き換えに続けて仮定に入った¬Qを、ターゲット側に戻すと:

  • Γ/ Δ, ¬P |-? Q

お膳立ての手順としては、「選言の片方の否定を仮定に移す」となります。このお膳立ては実用性が高いものです。

前提の命題を推論法則として使う

[追記]この節に対する補足説明が「証明の“お膳立て”のやり方 5: 証明可能性判断と推論規則」にあります。[/追記]

証明要求の'|-?'の右側全体を前提と呼ぶと約束しました。前提は文脈と仮定を一緒にしたものです。その前提のなかに、次の形の命題が入っていることが多いですね。

  • ∀x∈X.(P(x)⇒Q(x))

既知の定理とかはこの形で前提に含まれるでしょう。

上記の命題は、次のような証明可能性判断に書き換えてもいいです。

  • (x : X), P(x) |- Q(x)

お膳立て手順としては、

  Γ/ ∀x∈X.(P(x)⇒Q(x)), Δ |-? R
 --------------------------------------------[前提を判断に]
  Γ/ Δ |-? R     Γ/ (x : X), P(x) |- Q(x)

別な言い方をすると、本チャンの証明のとき、(x : X), P(x) が出てきたら、Q(x) を推論して(導いて)いいということです。前提に入っている命題を、推論の規則として使うことになります。

この説明だけでは分かりにくいでしょうから、後で実例のなかで使ってみます。

例題: 随伴による集合差の定義

随伴は圏論の概念ですが、順序に関する随伴性はより単純です。「順序随伴性: ガロア接続の圏論」で述べています。順序随伴の例を挙げます(今引用した記事からの再掲)。

Xを集合、Pow(X)はXのベキ集合とします。W∈Pow(X) を選んで固定します。F, G:Pow(X)→Pow(X) を次のように定義しましょう。

  • F(S) := S∩W
  • G(S) := Wc∪S ((-)cは補集合)

このとき、次が成立します。

  • F(S) ⊆ T ⇔ S ⊆ G(T)

このような関係にあるF, Gのペアを随伴ペア(adjoint pair)と呼びます。

もうひとつ別な例を挙げます。Wは同じく固定したPow(X)の要素です。

  • F(S) := S\W (集合の差)
  • G(S) := S∪W

この場合、FとGは随伴ペアです。つまり、次が成立します。

  • S\W ⊆ T ⇔ S ⊆ T∪W

簡略に言うと、集合に関する差と和が随伴になっています。この「差と和の随伴性」をターゲット命題とします。証明要求は次のようになるでしょう。

  • Γ/ (X : Set), (W : Pow(X)), (S, T : Pow(X)) |-? S\W ⊆ T ⇔ S ⊆ T∪W

記述を簡略にするために、仮定(自由変数 X, W, S, T の型宣言)も文脈に詰め込んで、次の形にします。

  • Γ |-? S\W ⊆ T ⇔ S ⊆ T∪W

ターゲットが選言の場合のお膳立て

まずは、いつもどおりのお膳立てをしましょう。もう慣れてきたと思うので、証明要求の書き換え理由(根拠)は省略します。

           Γ |-? S\W ⊆ T ⇔ S ⊆ T∪W
 ----------------------------------------------------------------
  Γ |-? S\W ⊆ T ⇒ S ⊆ T∪W    Γ |-? S ⊆ T∪W ⇒ S\W ⊆ T
 -------------------------------  -------------------------------
  Γ/ S\W ⊆ T |-? S ⊆ T∪W      Γ/ S ⊆ T∪W |-? S\W ⊆ T

左下の証明要求について考えます。

  • Γ/ S\W ⊆ T |-? S ⊆ T∪W

ターゲットは ∀x∈X.(x∈S ⇒ x∈T∨x∈W) と書けるので:

  Γ/ S\W ⊆ T |-? S ⊆ T∪W
 -----------------------------------------------
  Γ/ S\W ⊆ T |-? ∀x∈X.(x∈S ⇒ x∈T∨x∈W)
 -----------------------------------------------
  Γ/ S\W ⊆ T, (x : X) |-? x∈S ⇒ x∈T∨x∈W
 -----------------------------------------------
  Γ/ S\W ⊆ T, (x : X), x∈S |-? x∈T∨x∈W

ここで、ターゲットが選言である形が登場しました。「選言の片方の否定を仮定に移す」変形を施すと:

  • Γ/ S\W ⊆ T, (x : X), x∈S, ¬(x∈W) |-? x∈T

ここまで来てしまうと、直感でも分かる気はしますが、論理的な推論(リーズニング)を続けます。

仮定を推論規則として使う

前節最後の証明要求には、S\W ⊆ T という仮定がありました。これは次の命題と同じです。

  • ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T)

この命題を証明可能性判断の形で、証明要求と並べて書くと:

  • (判断) Γ/ (x : X), x∈S, ¬(x∈W) |- x∈T
  • (要求) Γ/ (x : X), x∈S, ¬(x∈W) |-? x∈T

んっ、アレ、証明のお膳立てをしてるうちに証明が終わってしまったよ。要求されていた証明が、最初の仮定のなかに(命題の形で)そっくり入っていたわけです。

残っている証明要求も見てみましょう。

  Γ/ S ⊆ T∪W |-? S\W ⊆ T
 ---------------------------------------------------
  Γ/ S ⊆ T∪W |-? ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T)
 ---------------------------------------------------
  Γ/ S ⊆ T∪W, (x : X) |-? x∈S∧¬(x∈W) ⇒ x∈T
 ---------------------------------------------------
  Γ/ S ⊆ T∪W, (x : X), x∈S, ¬(x∈W) |-? x∈T

仮定のなかに S ⊆ T∪W がありますが、これは次の証明可能性判断として書けます。

  • (x : X), x∈S |- x∈T∨x∈W

証明可能性判断においても「選言の片方の否定を仮定に移す」は使えます。

  • (x : X), x∈S, ¬(x∈W) |- x∈T

仮定の命題を証明可能性判断に書き換えた全体は:

  • Γ/ (x : X), x∈S, ¬(x∈W) |- x∈T

これまた証明が終わってしまいました(もう、やることがない)。

バックワード・リーズニングによる証明

今回の例では、証明のお膳立てをしているうちに、やることがなくなってしまいました。つまり、本チャンの証明部分がないのです。

こうしてみると、証明のお膳立てと本チャンの証明という区別はさして意味がないことが分かります。実は、今まで“証明のお膳立て”と呼んでいた行為は、ターゲット(結論)をより簡単な形に分解していくスタイルの“証明”でもあるのです。このスタイルの証明(行為)をバックワード・リーズニングと呼びます。ターゲットを作り出すスタイルのほうがフォワード・リーズニングです。

人間は、フォワード・リーズニングとバックワード・リーズニングを組み合わせて証明行為を実行しています。証明支援系(ソフトウェア)では、バックワード・リーズニングだけをサポートしているものが多数派です。人間による証明でも、バックワード・リーズニング、すなわちお膳立て方式で全てを済ましてしまうことも可能です(今回の例)。とはいえ、フォワード・リーズニングを禁止されると辛いので、バックワード/フォワードを柔軟に組み合わるのが得策です。

*1:論理式のあいだには依存関係があるので、単なる集合ではありません。依存関係を順序とした順序集合とみなすとよいでしょう。

2017-10-12 (木)

データベースへの論理的アプローチ: NULLについてチャンと考えよう

| 19:24 | データベースへの論理的アプローチ: NULLについてチャンと考えようを含むブックマーク

奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか」のなかで、ピンクで「(詳細は別途記述予定。)」と書いてあるところが6箇所あります。これらの“ピンクの宿題”を順不同で片付けていきます(全部、片付くかは不明)。

ピンクの宿題 その1

単なるベキ集合でも(ある意味)重ね合わせです。[...今回の話題に関係ないので省略...]この枠組内でNULLの意味も(ヨタ話じゃなくて)分析できます。(詳細は別途記述予定。)

NULLに関する基本的な事項についてゼロから考察してみます*1。予備知識として、ラーメン屋さんに行った経験を仮定しますが、その経験がなくても読めるように心がけました。この記事を読めば、NULLの使用法とダメさ加減がハッキリと分かるでしょう。

内容:

  1. NULLはダメなの? なんで??
  2. 型と型構成子
  3. ベキ集合の型
  4. ラーメン屋さんの食券販売機
  5. 繰り返し型と不明型
  6. 繰り返し型を禁止する
  7. 不明型の値があるとき
  8. 繰り返し型の値が不明なとき
  9. NULLの使われ方
  10. NULLがダメなホントの理由

NULLはダメなの? なんで??

「データベースにおけるNULLはダメだ」というのがおおかたの意見だと思います。僕もダメだと思います。しかし、天下りにダメだと禁止するのは、子供の教育上好ましくないですよね。大人の教育でも好ましくないでしょう。

どうしてダメなのかを納得がいくように説明して、もしそれが必要悪だとしたら、どんなときなら使うことが許されるのか、あるいは代替案にどんなものがあるのかも説明すべきです。

この記事では、NULLそのものより、NULLを使いたくなる状況の背後にあるデータ型を分析することにします。それにより、NULLに関する明快な理解を得られると思います。「ダメなモノだから曖昧な理解でもよい」と考えるのは危険です。ダメなモノのダメさをハッキリと知っておきましょう。

型と型構成子

「型とは何か?」については色々な立場・考え方がありますが、ここでは一番単純な「型とは集合である」(Sets-as-Types)の立場を採用します。例えば、Z = {..., -2, -1, 0, 1, 2, ...} を整数の集合として、「nの型は整数である」は、「n∈Z」とまったく同じ意味です。

要素(項目、メンバー)が整数であるリストを、ブラケットとカンマを使って、[2, 1, 3] とか [-1, 0] とか書くことにします。[0] や [] もリストです。Intは整数型を表すとして、整数のリストの型を List<Int> と書きます。[2, 1, 3], [-1, 0], [0], [] の型はすべて List<Int> です。

伝統と習慣により、“プログラミング言語の型”と“数学の集合”では違う記法を使います。

意味 型の記法 集合の記法
nは整数の値を取る n : Int n∈Z
xは整数リストの値を取る x : List<Int> x∈Z*

Z* の右肩の星はクリーネスターと呼ばれ、形式言語理論で常用される記法です。[2, 1, 3], [-1, 0], [0], [] ∈Z* ですね。

僕はどっちの記法も使うので、n : Z とか、[2, 1, 3]∈List<Int> とか、ごちゃ混ぜ記法を使ってしまうかも知れません。どうせ意味は変わらないので、分野の垣根や方言を気にするのはバカバカしいと思います(と、ごちゃ混ぜに対する言い訳をしておく)。

Listは、型Intに対して新しい型 List<Int> を作り出すので型構成子と呼びます。山形括弧 < > 内に入る型を、型パラメータとか型引数と呼びます。型パラメータを囲むのに山形括弧を使うのはプログラミング言語型理論の習慣ですが、Scala言語やEiffel言語では List[Int] だし、圏論では List(Z) です。括弧の種類がバンバラなんです。繰り返し言いますが、分野の垣根や方言を気にするのはバカバカしいと思います(つまり、ごちゃ混ぜになっても許してね)。

ベキ集合の型

Aが集合だとして、Aの部分集合の全体からなる集合をAのベキ集合*2と呼びます。例えば、A = {1, 2, 3} のとき、Aのベキ集合は次の集合です。

  • {{}, {1}, {2}, {3}, {1, 2}, {1, 3}, {2, 3}, {1, 2, 3}}

ベキ集合は power set なので、Aのベキ集合を Pow(A) と書くことにします*3

もとの集合Aが演算を持っていると、Pow(A) にも演算を定義することが出来ます; B = {True, False} として、Bは論理演算(AND, ORなど)を持つとします。Pow(B) = {{}, {True}, {False}, {True, False}} に論理演算を定義することが出来て4値論理になります。興味がある方は次の記事をどうぞ。

Pow(A) は数学的記法ですが、対応する型構成子記法は Subset<A> としましょう。例えば、集合Bの型名をBoolとして、Subset<Bool> は4値論理の真偽値の型になります。Aが無限集合、例えば A = Z のとき、Pow(Z) には、Z自身や偶数の全体などの無限集合も入ります。コンピュータで無限集合は扱いにくいので、Z(型Int)の有限部分集合だけを考えることがあります。そのときは、(ちょっと長ったらしいけど)FiniteSubset<Int> と書くことにします。Aが有限集合のときは、Subset<A> = FiniteSubset<A> です。記法に慣れるために幾つかの例を挙げておきます。

  • {}∈Pow(B), {True}∈Pow(B)
  • {} : Subset<Bool>, {True} : Subset<Bool>
  • {}∈Pow(Z), {1, 2, 3}∈Pow(Z), {k∈Z| k≧0}∈Pow(Z)
  • {} : Subset<Int>, {1, 2, 3} : Subset<Int>, {k∈Z| k≧0} : Subset<Int>
  • {} : FiniteSubset<Int>, {1, 2, 3} : FiniteSubset<Int>

ラーメン屋さんの食券販売機

前節までで、理論的準備はすっかり整いました。説明に使う事例を紹介します。

とあるラーメン屋さんがあり、事前に食券を自動販売機で買う方式だとします。ラーメンが3種類、トッピングが2種類です。タッチパネル食券販売機は次のように操作します。

  1. 最初に、醤油ラーメン、塩ラーメン、味噌ラーメンのなかから、一種類を選ぶ。
  2. 次にトッピング選択画面が出るので、チャーシューか味玉を選ぶ。どっちか片方でも両方でも、ひとつも選ばなくてもよい(トッピングはオプション)。
  3. 決定ボタンを押すと、食券が発券される。

この食券販売機は、内部に記録(ログ)を持っていて、次のようなデータが蓄積されるとします。

注文 ラーメン トッピング
1 醤油
2 味玉
3 醤油 チャーシュー
4 醤油 チャーシュー, 味玉
5 味噌

この記録データをデータベースのテーブルのように考えましょう。テーブルは3つのカラムを持ちます。それぞれのカラムのデータ型を考えましょう。データベース用語ではカラムのデータ型をドメインと呼ぶので、それぞれのデータ型(=ドメイン)を、D_注文, D_ラーメン, D_トッピング とします。

  • D_注文 = {i∈Z | i ≧ 1}
  • D_ラーメン = {醤油, 塩, 味噌}
  • D_トッピング = Pow({チャーシュー, 味玉}) = {{}, {チャーシュー}, {味玉}, {チャーシュー, 味玉}}

プログラミング言語っぽい書き方だと(enumは列挙型として):

  • D_注文 = Int (カラムのドメイン制約: 注文 ≧ 1)
  • D_ラーメン = enum {醤油, 塩, 味噌}
  • D_トッピング = Subset<enum {チャーシュー, 味玉}>

くどいけど、書き方なんてどうでもいいんです、意味・内容を理解してください。

この食券販売機の記録は、RDB(リレーショナル・データベース)に保存して管理することにします。

繰り返し型と不明型

いよいよRDB登場 … ちょっと待ってください。我々の目的はNULLの分析なので、ベキ集合の型(Subset型、FiniteSubset型)をもう少し詳しく見ておきます。

食券販売機の記録におけるトッピングの型は、Subset<enum {チャーシュー, 味玉}> でした。トッピング・カラムの値は集合になっています。集合である値を、RDB用語では繰り返しグループ(Repeating Group)と呼びます。この用語法に合わせて、Subset<A> を Repeat<A> とも書くことにします -- Aの繰り返し型と呼ぶことにしましょう。

さて、食券販売機の故障かバグで、記録が次のようになってしまった状況を考えます。

注文 ラーメン トッピング
1 醤油
2 味玉
3 醤油 チャーシュー
4 醤油 チャーシュー, 味玉
5 ?

5番の注文が不明です。不明ではありますが、ラーメン・カラムの可能性としては 醤油, 塩, 味噌 のどれかです。つまり、'?'の意味は集合 {醤油, 塩, 味噌} と言えるでしょう。となると、次のように書き換えてもいいでしょうか?

注文 ラーメン トッピング
1 醤油
2 味玉
3 醤油 チャーシュー
4 醤油 チャーシュー, 味玉
5 醤油, 塩, 味噌

これだと、繰り返しグループと見分けが付きません。将来、複数のラーメンを一度に注文できるように変わったとき困ることになります。そこで、「よくわからん」を表すために、先頭に疑問符を付けておきましょう。

注文 ラーメン トッピング
1 醤油
2 味玉
3 醤油 チャーシュー
4 醤油 チャーシュー, 味玉
5 ?醤油, ?塩, ?味噌

この表を見ると、チャーシュー, 味玉 のような繰り返しグループと、?醤油, ?塩, ?味噌 のような不明さを表す集合が現れます。数学的にはどちらもベキ集合の型(の値)ですが、意味・使用状況まで考えると違う型です。次のように定義しましょう。

  • 繰り返し型 Repeat<A> : Aの部分集合の型だが、値は繰り返しグループを表す。
  • 不明型 Unknown<A> : Aの部分集合の型だが、値は可能な候補を表す。実際の値は、集合Aの要素のどれか。

不明型(Unknown型)の値である集合を ?{醤油, 塩, 味噌} と書くことにします。疑問符を分配すれば {?醤油, ?塩, ?味噌} だから、辻褄は合ってます :-)

ところで、?{醤油, 塩} という不明な値は意味があるでしょうか。これは意味あります。ある日、味噌ラーメンが売り切れている状態で、次の記録が発生したとします。

注文 ラーメン トッピング
1 醤油
2 味玉
3 醤油 チャーシュー
4 醤油 チャーシュー, 味玉
5 ?

不明な箇所の可能性は ?{醤油, 塩, 味噌} ではなくて、?{醤油, 塩} です。他からの情報で、不明さを絞り込めることもあるのです。

?{醤油} という不明な値はどう解釈すべきでしょうか。不明ではあるが、可能な値は'醤油'だけ、となります。つまりこれは、確定した単一の値'醤油'と同じです。塩ラーメンと味噌ラーメンが売り切れている日に'?'が現れた状況を考えれば明らかですね。

繰り返し型を禁止する

食券販売機の記録をRDBのテーブルに入れましょう。生の記録だと、「第1正規形でない」としかられるので、2つのテーブルに分けて、トッピング・テーブルを次のようにします。

注文 トッピング
2 味玉
3 チャーシュー
4 チャーシュー
4 味玉

このテーブルのトッピング・カラムの型(集合)は D_トッピング = {チャーシュー, 味玉} で、生データのような繰り返し型は現れてません。

NULLの使用場面のひとつに、繰り返し型の空{}をNULLで表すものがあります。上記の方法で繰り返し型を追い出せば、ついでに空集合を意味するNULLもなくなってしまいます。

繰り返し型の空{}を表すNULLは、もっとも排除しやすいものです。しかし、排除した後で、もとの空集合{}はどう表現されているかには注意してください。今のラーメンの例で、注文1のトッピングが空集合であることは、トッピング・テーブル(注文とトッピングのテーブル)を検索したときの検索結果が空であることに反映されます。このケースの検索は次の問い合わせで実行できます。

  • select トッピング from トッピング・テーブル where 注文=1

「正規化」という言葉を使って述べれば、次の2つの事実が同値です。

  • 正規化前に、特定注文のトッピング・カラムの値が空
  • 正規化後に、特定注文のトッピングの検索(問い合わ)結果が空

不明型の値があるとき

だんだん話が厄介になりますよ。次の生データをRDBに格納することにします。

注文 ラーメン トッピング
1 醤油
2 味玉
3 醤油 チャーシュー
4 醤油 チャーシュー, 味玉
5 ?

不明を表す'?'を、Unknown<enum {醤油, 塩, 味噌}> の値で展開すると:

注文 ラーメン トッピング
1 醤油
2 味玉
3 醤油 チャーシュー
4 醤油 チャーシュー, 味玉
5 ?醤油, ?塩, ?味噌

繰り返し型の排除と同じ方法で複数の行(ロー、レコード)に展開すると:

注文 ラーメン
1 醤油
2
3 醤油
4 醤油
5 醤油
5
5 味噌

しかしこれは、既に述べたように、将来、複数ラーメンを一回に注文できるようになったら困ります。確実な値か不明な値かを識別するカラムを設けてはどうでしょう。

注文 ラーメン 確実性
1 醤油
2
3 醤油
4 醤油
5 醤油 ×
5 ×
5 味噌 ×

一見うまくいきそうで、実際多少は使える方法かもしれません。しかし、このテーブルの情報から、真実のテーブルの候補を判断する方法がありません。例えば、次の2つのテーブルを較べてみてください。

注文 ラーメン
1 醤油
2
3 醤油
4 醤油
5 醤油

 

注文 ラーメン
1 醤油
2
3 醤油
4 醤油
5 醤油
5

一番目のテーブルは、食券販売機が正常に動いていればあり得るデータです。しかし、二番目のテーブルは、現状の(一回の注文でラーメンひとつ)食券販売機からは出現しない異常なデータです。

単に不明だ(不確実だ)というだけでなく、真実のテーブルの候補(あり得る正常データ)をキチンと列挙できることが望ましいのです。この例では、「ひとつの注文にはラーメンがひとつだけ」というルールがあればうまくいきます。が、そのようなルールは、テーブルの構造とは別に手続き的に書かなくてはなりません*4

次の節で述べる「繰り返し値が不明」の場合と比べると、より事情がハッキリするでしょう。

繰り返し型の値が不明なとき

今度は、次の生データを考えます。

注文 ラーメン トッピング
1 醤油
2 味玉
3 醤油 チャーシュー
4 醤油 チャーシュー, 味玉
5 味噌 ?

正規化しない生の状態で、注文5のトッピングの値になり得る値は次の4つです。

  1. {}
  2. {チャーシュー}
  3. {味玉}
  4. {チャーシュー, 味玉}

この4つのどれであるか不明なので、その不明値を書き下すと:

  • ?{{}, {チャーシュー}, {味玉}, {チャーシュー, 味玉}}

上のごとき、繰り返しと不明さを含む生データを、正規化したテーブルで表現することができるのでしょうか? なんか絶望的な感じがします。

ですが、意外にも簡単なんです。前節と同様、確実性のカラムを設けてみると:

注文 トッピング 確実性
2 味玉
3 チャーシュー
4 チャーシュー
4 味玉
5 チャーシュー ×
5 味玉 ×

確実性が×の行に関しては、その行が存在する場合と存在しない場合の二通りがあると解釈して、すべての可能性を列挙してみます。

2行ともに存在する

注文 トッピング
2 味玉
3 チャーシュー
4 チャーシュー
4 味玉
5 チャーシュー
5 味玉

チャーシューの行だけ存在する

注文 トッピング
2 味玉
3 チャーシュー
4 チャーシュー
4 味玉
5 チャーシュー

味玉の行だけ存在する

注文 トッピング
2 味玉
3 チャーシュー
4 チャーシュー
4 味玉
5 味玉

2行ともに存在しない

注文 トッピング
2 味玉
3 チャーシュー
4 チャーシュー
4 味玉

これら4つのケースは、あり得る真実のデータを全て尽くしています。不明さを含んだデータから、真実のデータの候補を列挙できました。

この例では、繰り返し型と不明型がうまいこと相互作用して、結果的に話が単純になったのです。一般論を展開するには、繰り返し型構成子Repeatと不明型構成子Unknownが混じった型の計算法則を準備する必要があります。そのことは、またいずれかの機会にしましょう*5

NULLの使われ方

今までの話で、ベキ集合の型が、現実の場面では繰り返し(Repeat)型と不明(Unknown)型として現れることが分かりました。

NULLの使われ方はたくさんあるそうです。どれくらいあるのか僕は知りませんが、繰り返し型と不明型の文脈で考えると、3種類になります。

繰り返し型の空

ラーメンのトッピングなしの例です。このタイプのNULLは簡単に排除できます。そもそも意味が簡単なので、排除しなくてもあんまり悪さはしません。

ただし、繰り返し型の空だけなら弊害が少ないということで、他のタイプのNULLと混在するような状況では悲劇になるでしょう。

不明型の全体集合=まったく不明

ラーメンの種類が'?'の例です。ラーメンの種類の全体集合は {醤油, 塩, 味噌} ですが、この全体集合が値なら、意味としては「まったく不明」ということです。

データベースの場合、まったく不明であっても、カラムのドメイン(データ型)はあるので、ラーメンの種類が'豚骨'は排除されています。つまり、不明のマーカーとしてNULLだけを使っている場合でも、可能な値の集合はドメインごとに違うのです。たくさんの「まったく不明」があります。「ラーメンの種類がまったく不明」「整数値がまったく不明」「二値真偽値がまったく不明」とかです。

不明型の空=禁止

不明な値 ?{醤油} は、単一の値'醤油'と同じだと言いました。では、不明な値 ?{} はどうでしょう。'?{'と'}'のあいだには、「可能性がある値を並べる」というルールを思い出してください。?{} には可能な値がひとつもありません。つまり、値は未定義(undefined)、あるいは値を持つことを禁止(forbidden)されています。

繰り返し型の空 {} と、不明型の空 ?{} は違います。{}は、「トッピングなし」のように正常な値です。それに対して、ある条件下で値があってはいけないことを ?{} で表します。

ラーメン屋さんで具体例を挙げましょう。味噌ラーメンを赤味噌ラーメンと白味噌ラーメンから選べるようにしたとします。今までの記録データを大きく変えたくないので、次の形を採用します。

注文 ラーメン トッピング 味噌
1 醤油 -
2 味玉 -
3 醤油 チャーシュー -
4 醤油 チャーシュー, 味玉 -
5 味噌 赤味噌

醤油ラーメンと塩ラーメンでは、味噌カラムは無意味です。ハイフンの意味は、未定義または禁止で、不明な型の空 ?{} がふさわしいでしょう。

未定義または禁止を表す値は、不明な型を持ち出さなくても、通常の値に特殊値として追加する方法でも導入できます。しかしそれは、繰り返し型の空や、不明型の「まったく不明」とは別物です。

NULLがダメなホントの理由

NULLにいろいろな種類があり、その扱いはけっこう難しいことが分かったでしょう。とはいえ、それぞれの種類のNULLをそのデータ型と共に分析すれば、NULLの正体は明らかになり、利用法・対処法も見えてきます。

データベースにおけるNULLがダメなのは、そのように様々なNULL達を、エヌ・ユー・エル・エルと綴る単一の記号で表そうとしているところです。つまり、性質も振る舞いも異なる様々なNULL達を区別して扱う手段がないのです。

性質も振る舞いも異なるモノ達を、ミソもクソも一緒に単一の呼び名で指し示せば、破綻することは目に見えています。どれかひとつのセマンティクスに限ってNULLを使う、という方法はありますが、そのひとつのセマンティクスの選び方が人により違うので、違った選択が出会ったとき、やはり破綻します。

結局、「NULLは使わない、使うときは外部に影響が及ばない閉じた範囲で使う」というような処方箋になるかと思います。

*1:もとの“ピンクの宿題”に書いてあった凸結合の話とかは今回はしません。これは、さらに先延ばし。

*2:「ベキ」は古い難しい字で「冪」と書くか、あるいは略字の「巾」を使います。どちらも難読なので、僕はカタカナ書きしています。

*3:印刷物では、ドイツ文字(フラクトゥール)のペー(P相当)が使われることが多いです。しかし、プレーンテキストでペーを書くのは難しいので、僕はPowを使っています。

*4:「奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか」のなかで説明した演繹データベースならば、手続きではなくて論理式として「ひとつの注文にはラーメンがひとつだけ」を書けます。

*5:RepeatとUnknownはどちらベキ集合を作る型構成子です。その点では同じ。しかし、現実的な解釈は違います。「同じだけど違う」をうまく定式化するのはけっこう難しそうです。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171012

2017-10-10 (火)

奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか

| 11:02 | 奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのかを含むブックマーク

言い訳から始めます。この記事を(途中まででも)読んだ人は、次のように言いたくなるでしょう。

  • 『理論から学ぶデータベース実践入門』は良い本なのか悪い本なのか、いったいどっちなんだよ?!

この本は間違いや説明不足があり、誤読されやすい表現も多く、その点では残念な本です。しかし、面白いアイディア、するどい観察も含まれていて、行間を補い深読みすれば、多くの示唆を得られる本でもあります。

よって、「良い/悪い」の二択では答えられません。良い点と悪い点の両方を、できるだけ客観的に記述するしかないのです。それをした結果、長い記事となりました。

内容:

  1. ことの発端: zhanponさんの批判
  2. 奥野本擁護と奥野本批判
  3. 僕の擁護・批判の方針
  4. zhanponさんの指摘の再検討
    1. 論理的な矛盾とデータの不整合を混同している
    2. 命題論理の限界についての説明がおかしい
    3. 古典論理の定義を間違えている
    4. 集合と集合論、述語と述語論理を混同して使っている
    5. 二階論理の説明がおかしい
  5. 消極的提案: 第2章を削除する
  6. 積極的提案: 述語論理を活用した解説
  7. 奥野さんの発想の源泉(ただし想像)
  8. 「矛盾」て何なんだろう?
  9. 演繹データベースと矛盾: 奥野さんは(まーまー)正しかった
  10. 演繹データベースで出来ること
  11. 述語論理をチャンと使おう
  12. 外部世界をチャンと考慮しよう
  13. おわりに

ことの発端: zhanponさんの批判

先日、次のQiita記事をみつけました。

タイトルにある本の第2章がオカシイという話です。もとの本をまったく知らないので、“著者の説明が舌足らずな程度”なのか、“トンデモ本と呼べるひどさ”なのか分かりません。

そこで、渋谷のMARUZEN&ジュンク堂書店で立ち読みすることにしました。立ってるのが辛くなったし、(幾つかの意味で)面白い本なので購入しました。

奥野本擁護と奥野本批判

先のQuiita記事で、zhanponさんは5つの問題点を指摘しています。そのうちの1つはどうにも擁護できませんが、残る4つは(ある程度は)擁護できます。zhanponさんの批判は、著者・奥野さんの真意を理解してないように思います。(真意を汲み取るのが困難なので、zhanponさんを責める気はありません。)

僕の批判・批判=擁護の弱いところは、「奥野さんの真意」なるものが僕(檜山)の想像である点です。想像が妄想だったら、僕の言い分はデタラメになります。この点は奥野さんご本人しかジャッジできないことです。

では、奥野本には問題がないのかというと、大いに問題あります。zhanponさんが指摘した諸点より、もっと重大な問題があります。zhanponさんに誤解を与えたこと*1も、おそらくは多くの人を困惑・混乱させていることも、「重大な問題」に起因しています。

先にその問題点を言っておくと:

  1. 論理をほとんど使ってない。
  2. 外部世界を考慮してない。

「書きたかったはずのこと/書くべきだったこと」が書いてないと言えます。zhanponさんは注意深く断り書きを付けています:

著者の意図が本文に正しく反映されていない可能性もある。

まさに、著者の意図が本文に正しく反映されていない本だと思います。

僕の擁護・批判の方針

問題点はありますが、だからといってこの本が無価値だとは思いません(zhanponさんも同じ断り書きをしています)。ほんとにダメダメだったら、そもそも擁護・批判する価値さえないので無視するか、トンデモ本ネタとして茶化すかです。擁護・批判に値する程度に、示唆に富む内容だということです。激しく同意する点も、「なるほど」とうなずく所も多々あります。

この本の企画の意図と志は素晴らしいものです。その意図・志が実現できていない、むしろミスリーディングな記述が目立つ、という事が僕が批判的になる理由です。「企画に無理があったかも」と感じるし、一方で「こうすればウマクいくんじゃないか」という思いもあります。

今回、擁護・批判の対象にするのは、『理論から学ぶデータベース実践入門』の第8章までです(すぐ下に目次)。第9章以降は、各論と応用なので、実務に疎い僕がどうこう言える内容ではありません(よって、対象外)。

  • 第1章 SQLとリレーショナルモデル
  • 第2章 述語論理とリレーショナルモデル
  • 第3章 正規化理論(その1)―― 関数従属性 ――
  • 第4章 正規化理論(その2)―― 結合従属性 ――
  • 第5章 リレーションの直交性
  • 第6章 ドメインの設計戦略
  • 第7章 NULLとの戦い
  • 第8章 SELECTを攻略する
  • 第9章 履歴データとうまく付き合う
  • 第10章 グラフに立ち向かう
  • 第11章 インデックスの設計戦略
  • 第12章 Webアプリケーションのためのデータ構造
  • 第13章 リファクタリングの最適解
  • 第14章 トランザクションの本質

「述語論理に関して幾つか誤りが見られる」とか「論理に詳しい人なら「なにを今更」「間違いだらけ」だ」とかほのめかして、その根拠を明らかにしない事は、僕が最も忌み嫌う卑怯なクズ野郎のやり口なので、僕はしません。しかし、擁護・批判の詳細な根拠は、短時間では書けないし、ひとつの記事が長大になるのも好ましくありません(って、いいかげん長大なんだが)。そこで、概略しか書いてない所では、「(詳細は別途記述予定。)」という断り書きを入れます。後日記事にしたら、リンクを張ります。

文句を言うだけでは建設的でないので、消極的提案と積極的提案をします。消極的提案とは、間違いと不適切な記述の削除・修正の案です。積極的提案とは、企画意図を実現するための加筆・敷衍の案です。

zhanponさんの指摘の再検討

zhanponさんの5点の指摘を引用します。「…」の後は僕のコメントです。

  1. 論理的な矛盾とデータの不整合を混同している … これは重要な論点
  2. 命題論理の限界についての説明がおかしい … それほどおかしくない
  3. 古典論理の定義を間違えている … 完全に間違えている、アウト
  4. 集合と集合論、述語と述語論理を混同して使っている … 言葉遣いが杜撰とは言えるが
  5. 二階論理の説明がおかしい … それほどおかしくない

この節は、著者・奥野さんを擁護する論調です。論理学の予備知識を仮定するので分からない所は飛ばしてください。

1. 論理的な矛盾とデータの不整合を混同している

これは、奥野さんの真意を想定(想像)しないと擁護できないので、次節以降(結論はココ)に回します。

2. 命題論理の限界についての説明がおかしい

zhanponさんは奥野本p.42の説明をまるまる引用しています。

命題論理は、突き詰めて言えば命題同士の関係性について、あれこれと考える学問です。ある事実を単に真偽値を持った命題として表現できる限りは、それで十分ですが、そうではない場合、つまり事実をシンプルな命題を用いて表現できないケースには対応できません。

たとえば、「この村のすべての村人が正直者だというわけではない」という文章は、どのような論理式で表現すれば良いでしょうか?

この文章をたとえば、P という命題だと仮定すると、「この村には正直でない者がいる」という命題の真偽は、どうやって証明すれば良いでしょうか? ほかにも「この村の村人は全員誰かと友だちである」という文章は、どのような論理式で表現すれば良いでしょうか? この文章と、「この村には村人全員と友だちの村人がいる」という文章との違いを、どのように確認すれば良いのでしょうか。

この部分、僕はあんまり違和感なかったです。

奥野さんの言いたいことは、次のようなことでしょう; 「この村のすべての村人が正直者だというわけではない」という内部構造を持つ文、述語論理を使えば「¬∀x∈この村の村人.(正直者だ(x))」と書ける文を、命題論理の命題Pと見なしてしまうと(つまり、量化子による内部構造を隠してしまうと)、内容的には同値である「この村には正直でない者がいる」をPから導出するすべがない。

順番に書くと:

  1. 命題Pを ¬∀x∈この村の村人.(正直者だ(x)) と置こう。(述語論理の書き方先取りしちゃってるけどさ。)
  2. 命題Qを ∃x∈この村の村人.(¬正直者だ(x)) と置こう。
  3. 内容的に P⊃Q かつ Q⊃P だよね。
  4. 命題論理の範囲内で、P⊃Q や Q⊃P を証明できますか?
  5. できないよね。
  6. 命題論理だけでは不十分だね。

これは、“著者の説明が舌足らずな程度”だと思います。

3. 古典論理の定義を間違えている

これはアウト。古典論理の定義(奥野本p.49)「一階述語論理は、古典論理とも呼ばれます」は間違ってます。でも、定義の一文を削除すればすむ話です。古典論理という概念を後で使いません(デフォルトが古典論理なので)。しかし、正しい定義をしておけば、後の説明を少し面白くできるでしょう。

p.145から3値論理の話があります。T(真), F(偽), U(未知)が真偽値です。論理演算の仕方はp.146にあります。それに従って真理値表を書いてみると、排中律(A∨¬A)は恒真式にならず、矛盾を表す式(A∧¬A)は恒偽式になりません。背理法も使えません。

A ¬A A∨¬A A∧¬A
T F T F
F T T F
U U U U

排中律や背理法は、古典論理における法則/推論手法です。そして、我々が使い慣れているのは古典論理なので、古典論理ではない3値論理は辛いよね、という説明ができます。

{T, F, U}の3値論理は、次の記事の4値論理からボトム(⊥)を除いたものと同じです。

2値以外の真偽値にもし興味があるなら:

奥野本p.147のコラム「量子コンピュータとNULL」は悪い意味でヨタ話になっているので、削除したほうがいいでしょう。「量子」とかリスキーなワードを持ち出さなくても、単なるベキ集合でも(ある意味)重ね合わせです。計量的な重ね合わせをしたいなら、凸結合(重心結合)や劣凸結合の空間で出来ます。この枠組内でNULLの意味も(ヨタ話じゃなくて)分析できます。(詳細は別途記述予定。)[追記]データベースへの論理的アプローチ: NULLについてチャンと考えよう」参照[/追記]

4. 集合と集合論、述語と述語論理を混同して使っている

不注意と説明不足な点があるけど、まー、許容範囲かな。

  • 奥野本p. 50「集合は一階述語論理と1:1対応する」

「集合」は「集合論」の書き間違いとすれば、次の文と同じです。

  • 奥野本p.64 「述語論理と集合論は1:1で対応しています」

これは、述語論理のある特定の体系に対して、ある種の集合論(ZFCってことではない)の宇宙が健全な(ひょっとすると完全な)モデルになっている、ってことを言いたいのだと思います。(詳細は別途記述予定。)

5. 二階論理の説明がおかしい

他の部分(例えばp.136)も読むと、奥野さんは、二階論理に関してだいぶ誤解をしているようです。単なる二階論理で自己言及ができないのもzhanponさんのおっしゃる通り -- 「自己言及は二階論理では不可能である。」

ですが、ちょっと細工すれば自己言及はできます。アトム(とみなすモノ)の集合をDとして、Dの要素を引数とする単項述語の集合をPred(D)とします。Pred(D)をD内に埋め込むゲーデル・エンコーディング g:Pred(D)→D があれば、p∈Pred(D)に対して p[p] := p(g(p)) と自己言及できます。(「「わたしはウソをつきません」と言い張る命題やプログラムを書けるのか?」も参考になるかも。)

つまり、gというレイフィケーション機能を付けた一階述語論理内で自己言及が可能です。しかしgは、構文領域の存在物Pred(D)と意味領域の存在物Dをまたぐ写像なので、当該の一階述語論理体系内で表現されていません。ニ階述語論理体系を使えば、体系内でgを記述できるでしょうか? たぶんできます。そのうちやってみます。(詳細は別途記述予定。)

とはいえ、奥野本の趣旨と構成からいえば、自己言及への“言及”はそもそもアラズモガナなので、一段落(p.49からp.50)削除すべきです。

消極的提案: 第2章を削除する

僕が感じたこの本の問題点のひとつは「論理をほとんど使ってない」ことです。どうせ使わないのなら、第2章「述語論理とリレーショナルモデル」は不要です。奥野さんは、

  • 論理学に触れない正規化の解説は、でたらめだと言っても過言ではありません。

と思いっきり強調太字で書いてますが、過言です。実際に、第3章以降で、述語論理を実質的・本質的に使っている所はないです。読む側としては、第2章を飛ばして、他で論理学の用語が出てきたら、そこも飛ばすようにしても差し支えないです。

「自己言及」「閉世界仮説」「フレーム問題」「量子力学的重ね合わせ」とかの言葉の使用も、間違いとは言いませんが、衒学的臭いがします。第2章は、まるまる衒学趣味の産物に見えます。

第3章以降でしばしば登場する論理的概念は「矛盾」です。論理的矛盾を引き合いに出して「データ不整合は怖いぞ、ダメだぞ」と訴えています。しかし、データ不整合がマズイことは、論理学で説明するまでもないことです。原稿修正作業としては、「矛盾」を文字列検索して、データ不整合と論理的矛盾を絡めている記述は全部削除するだけです。

今述べた削除修正によって、この本の価値は下がりません。むしろ、読みやすくなって歓迎されるでしょう。

積極的提案: 述語論理を活用した解説

「第2章は、まるまる衒学趣味の産物に見えます」と失礼なことを書きました。読む側からはそう見える(かも知れない)ということです。著者・奥野さんがそんなつもりではないことは承知です。曖昧な物言いや事例を出すだけでごまかさないで、述語論理を使ってキチンとした説明をしたい、というのが奥野さんの意図・志でしょう。

もちろん、その意図・志は支持します。しかしながら、一階述語論理の述語(が定義する命題関数)とリレーショナルモデルのリレーションとの対応だけでは、いうほど役に立つものでもなく、ありていに言って「別になくてもいい」ものです。

リレーショナルモデルについて語る人は、数学や論理を基盤としていることを強調することが多いのですが、その割に数学的/論理的記述はスベっているきらいがあります。奥野さんの記述も現象としてはスベっています。衒学趣味とみなされかねないのです。

しかし、奥野さんには(皮肉ではなく)高邁な志があるように思えます。リレーショナルモデルだけでなく、奥野流データベース理論を語ろうとしているのではないか、と。その理論が断片的に、ときに間違いを含んだ形で発露されているように僕には見えます。

僕が想像する(想像し過ぎか?)奥野流データベース理論を説明するには、一階述語論理では不十分です。二階で済むのか、それ以上の階数が必要なのかちょっと分からないのですが、高階(ニ階以上)の述語論理が必要です。

もし、意図・志を実現したいなら、高階述語論理まで積極的に使うべきです。それと同時に、論理のモデル*2としての外部世界(現実世界でも仮想世界でも抽象世界でもいい)を考慮すべきです。つまりは、次の2つの問題点を解決すべきです。

  1. 論理をほとんど使ってない。
  2. 外部世界を考慮してない。

奥野さんの発想の源泉(ただし想像)

僕が想像するには(あくまで想像ですが)、奥野さんの心のなかには(仮称)奥野流データベース理論がおぼろげに芽生えているようです。その理論の基盤となる概念は次の3つでしょう。

  1. (仮称)リレーショナル集合論
  2. (仮称)リレーショナル述語論理
  3. 演繹データベース

(仮称)リレーショナル集合論とは、リレーショナルモデルを説明するのに適した集合論です。ZFC公理的集合論のようなものではなく、アトムと型(または階数)を持ち帰納的に構成できるものです。

(仮称)リレーショナル述語論理は、基本リレーションを基本述語記号とみなして構成される、古典論理のひとつの体系です。

奥野さんが「集合論と述語論理は1:1対応する」と再三述べているのは、「(仮称)リレーショナル集合論と(仮称)リレーショナル述語論理は1:1対応する」ということです。あくまでリレーショナルモデル界隈を説明・分析する道具・枠組みのことであって、一般的集合論と一般的述語論理の話ではありません。(詳細は別途記述予定。)

推論や証明のことを演繹〈えんえき〉といいます。演繹能力を備えたデータベースが演繹データベースです。ここで言う演繹データベースは、特に(仮称)リレーショナル述語論理の演繹能力を備えたものです。そのような演繹データベースが、奥野さんにとっての理想のデータベースなのではないでしょうか。

(仮称)奥野流データベース理論の問題点は:

  1. アイディアはある(ように見える)が、明確な定式化には至っていない。
  2. アイディアの(断片的)記述においても、勘違いや過ちがある。

この残念さが『理論から学ぶデータベース実践入門』の各所に影を落としていると言えるでしょう。

「矛盾」て何なんだろう?

奥野本p.68の表データ(リレーション)の一部を例にします。背後に、IT系の学校のデータベースがある、という設定です。あくまで説明用の事例なので、現実性はありません。

氏名 授業 学年
桂小五郎 リレーショナルモデル 2
坂本龍馬 リレーショナルモデル 1
坂本龍馬 コンピュータアーキテクチャ 2

奥野さんは、同一人物(学生)'坂本龍馬'の学年が1と2になっているから、「矛盾が生じた」(p.69)と述べています。一方zhanponさんは、この状況は「論理的な矛盾ではなく、「1人の人間が異なる2つの学年をもつことはない」という大学のルールに対する不整合である。」と指摘しています。

ここでは、奥野さんの表現を採用して「矛盾」を使います。ただし、注意を喚起するために《矛盾》と書きます。

さて、この《矛盾》は何に由来するのでしょうか? これが《矛盾》だと判断する根拠は何でしょうか? ここでちょっとした実験をしてみます。先の表データは《矛盾》しているとして、次の表データならどうでしょうか?

氏名 授業 成績
桂小五郎 リレーショナルモデル 2
坂本龍馬 リレーショナルモデル 1
坂本龍馬 コンピュータアーキテクチャ 2

《矛盾》していると感じますか? 「'坂本龍馬'君の'リレーショナルモデル'の成績が1」「「'坂本龍馬'君の'コンピュータアーキテクチャ'の成績が2」と解釈すれば、《矛盾》はありません。次の表データならどうでしょう。

評者 書籍 評価
桂小五郎 リレーショナルモデル 2
坂本龍馬 リレーショナルモデル 1
坂本龍馬 コンピュータアーキテクチャ 2

「'坂本龍馬'氏による書籍'リレーショナルモデル'の評価は星1つ」、「'坂本龍馬'氏による書籍'コンピュータアーキテクチャ'の評価は星2つ」と解釈すれば、《矛盾》はありません。

僕がやったことは、表の属性名(見出しの名前)を変えただけです。属性名の変更に関して、奥野本p.62から引用すると:

既存の属性名を変更するだけであれば、特に、論理式としての構造に変化はありませんので、リレーションが表す意味にも変化はありません。どのような名称で呼ぼうが、論理的な意味は同じです。

論理的な意味が同じなのに、どうして《矛盾》したり《矛盾》しなかったりするのでしょうか? これこそ矛盾(オカシナこと)じゃないでしょうか。

演繹データベースと矛盾: 奥野さんは(まーまー)正しかった

前節の種明かしをしましょう。我々は、「'氏名'、'授業'、'学年'、'成績'、'評者'、'書籍'、'評価'」といった言葉から、無意識に意味を連想します。連想した意味に基づき常識を働かせます。

  • 同一学生が異なる2つの学年をもつのはオカシイ。
  • 同一学生が異なる2つの授業で異なる成績なのはオカシクない。
  • 同一人物が異なる2つの書籍に対して異なる評価をするのはオカシクない。

オカシイかオカシクないか(《矛盾》があるかないか)の判断は、解釈と常識によるのです。zhanponさんの指摘どおり、大学(学校)のルール/世間のルールとの整合・不整合の問題です。

となると、学校なり世間なりを考慮しないと《矛盾》の判定はできないことになります。無意味・無味・無臭な表データ(リレーション)だけ見ても、《矛盾》の検出なんて出来っこありません。先入観なしに次の表データを見てください。《矛盾》のあるなしは、サッパリ分からないはずです。

属性-1 属性-2 属性-3
桂小五郎 リレーショナルモデル 2
坂本龍馬 リレーショナルモデル 1
坂本龍馬 コンピュータアーキテクチャ 2

《矛盾》の判定基準は、外部世界のルールに由来するのです。演繹データベースのメリットのひとつは、外部世界のルールも、データベース内に格納できることです。「同一学生は同一の学年をもつべし」は次の論理式で書けます。

  • ∀x∈D_氏名.∀i, j∈D_学年.( 学生学年(x, i)∧学生学年(x, j) ⊃ i = j )

これだけだと分からないかな、説明を補足:

  • D_氏名 は氏名の値(たぶん文字列)全体の集合です。RDB用語では、基本的値の集合をドメインと呼ぶので接頭辞'D_'を付けました。
  • D_学年 も同様に、学年の値(たぶん整数)全体の集合です。
  • 学生学年(x, i) は、氏名xの学生が学年iであることです。

さて、上の表データから、学生学年(x, i) の形の述語を抽出します。

  • 学生学年(坂本龍馬, 1)
  • 学生学年(坂本龍馬, 2)

外部世界(学校)のルールと、表データの一部から、3つの論理式が得られました。これらに対して、述語論理の推論を施してみます。

 ∀x∈D_氏名.∀i, j∈D_学年.( 学生学年(x, i)∧学生学年(x, j) ⊃ i = j )
-------------------------------------------------------------------------
    ↓ x = 坂本龍馬 と具体化する。
 ∀i, j∈D_学年.( 学生学年(坂本龍馬, i)∧学生学年(坂本龍馬, j) ⊃ i = j )
--------------------------------------------------------------------------
    ↓ i = 1, j = 2 と具体化する。
 学生学年(坂本龍馬, 1)∧学生学年(坂本龍馬, 2) ⊃ 1 = 2

学生学年(坂本龍馬, 1)、学生学年(坂本龍馬, 2) を仮定として使えるので、

 学生学年(坂本龍馬, 1)∧学生学年(坂本龍馬, 2)
 学生学年(坂本龍馬, 1)∧学生学年(坂本龍馬, 2) ⊃ 1 = 2
-------------------------------------------------------
    ↓ モダスポネンス
   1 = 2

一方で、「1 = 2 じゃない」ことは真だと認められるので、

 1 = 2    ¬(1 = 2)
--------------------
    ↓ ∧の導入
 (1 = 2)∧¬(1 = 2)
--------------------
    ↓ 矛盾の導入
    ⊥

最後の⊥は論理的矛盾を表す記号です。ほんまもんの矛盾です。

外部世界のルールと、表データ(リレーション)の情報を、述語論理の論理式の形に書いて、述語論理の推論をすれば、論理的矛盾が導けます。つまり、この演繹データベース=述語論理系は矛盾を含むのです。

結果的に、奥野さんの《矛盾》は確かに論理的矛盾であり、「矛盾」の使用法に(少なくともこのケースでは)間違いはありません*3

しかしこれは、演繹データベースを想定した場合のことです。そういう想定が読み取れる書き方はされてません。それ相応の深読み、忖度が必要です。また、矛盾が生じるのは演繹データベース=述語論理系全体の性質であって、「リレーションに矛盾が生じる」という言い方は不用意に過ぎます。そもそも、「矛盾」を滅多矢鱈と使い過ぎなんですよね*4

演繹データベースで出来ること

せっかくなので、演繹データベースでもう少し遊んでみましょう。次のように仮定します。

  • 履修(x, m, y) とは、氏名xの学生が名前mの授業をy年度に履修すること。
  • yが今年度なら、現在履修中。
  • yが過去なら、履修済み(落第してない)。

授業'SQL入門'を履修するには、'リレーショナルモデル'を履修している必要があるとします。同様に、'SQL応用'を履修するには、'SQL入門'を履修している必要があるとします。これらの条件は次のように書けます。

  • ∀x∈D_氏名.∀y, z∈D_年度.( 履修(x, SQL入門, y) ⊃ 履修(x, リレーショナルモデル, z)∧(z < y) )
  • ∀x∈D_氏名.∀y, z∈D_年度.( 履修(x, SQL応用, y) ⊃ 履修(x, SQL入門, z)∧(z < y) )

こんな学校のルールが演繹データベースに入っていれば、履修(勝海舟, SQL応用, 2017) から、履修(勝海舟, SQL入門, y)∧(y < 2017) や 履修(勝海舟, リレーショナルモデル, z)∧(z < 2016) が、論理的な推論で導出できます。

また、'リレーショナルモデル'を受けてない学生が'SQL入門'を履修登録していれば、矛盾が生じます。矛盾検出機構や矛盾防止機構が付いていれば、学校のルールが破られる事態に対処できます。

次に否定(論理記号¬)を含む例を考えてみましょう。

  • ∀x∈D_氏名.∀y∈D_年度.( 学生学年(x, 1) ⊃ ¬履修(x, Javaプログラミング, y) )

これは、「1年生は'javaプログラミング'を受けられない」という意味です。x = '坂本龍馬', y = 2017 として、このルールが守られているかチェック(真偽判定)するにはどうするのでしょう。まず、学年学生(坂本龍馬, 1) という情報が見つかり、含意(論理記号⊃)の左が真だと分かったとしましょう。あとは、¬履修(坂本龍馬, Javaプログラミング, 2017) の真偽判定です。

奥野本p.51で説明(?)されている閉世界仮説の眼目は、¬履修(坂本龍馬, Javaプログラミング, 2017) のような否定命題の証明を、履修(坂本龍馬, Javaプログラミング, 2017) の検索(一種の証明と考える)失敗で代用していいよ、ってことです。「Pである証拠が見つからなかったら、Pでない」と考えるのです。閉世界仮説のもとで、否定命題も扱えるようになります。

と、こんな感じで、現状、CHECK制約/表明/トリガーなどの手段で実現していることが、演繹データベースにおいては一様かつクリアに表現できるのです。カッコイイですよね。奥野さんはたぶん、次のように考えているのでしょう。

  • 理想のデータベースは、演繹データベースである。
  • リレーショナルデータベースは、不完全な演繹データベースである。
  • リレーショナルデータベースを、演繹データベースに(その部分系として)埋め込める。

述語論理をチャンと使おう

奥野本『理論から学ぶデータベース実践入門』において、次の2点を改善すべきだと述べました。

  1. 論理をほとんど使ってない。 → 述語論理をチャンと使う。
  2. 外部世界を考慮してない。 → 外部世界をチャンと考慮する。

「本の第2章を削除する」修正案だと、「論理をほとんど使ってない」のは問題になりませんが、現状だと「何のための第2章か?」なんですよ。

p.61で射影を論理的に説明するとき、なぜか存在量化子(限量子)に触れてないんです。ここで存在量化子使わなかったら、どこで使うんじゃい?! p.57の結合(ジョイン)の論理的説明でも、肝心の存在量化子付けてないし、p.51のリレーション=述語の説明では、不要な全称量化子を付けちゃっているし、p.136では事例と論理を絡めたけど、論理側の説明がスッカリ間違っているので、これはないほうがいいし。使うべきところで使ってないか、使わないほうがマシかです。

奥野さんは、リレーショナルモデルは一階述語論理に基づくので、二階述語論理は要らないと書いてますが、それは違います。そういうことじゃない。キー制約関数従属性制約結合従属性制約などの制約を、チャンと定義・説明するなら、二階述語論理を使わざるを得ないです。「いつでもチャンと説明しろ」とは言いませんが、論理を使って説明するなら、そうなります。以下に例を挙げましょう。

Aを属性集合として、タプルtのAによる射影を t[A] と書くことにします。例えば、A = {氏名, 生年月日} のとき、t[{氏名, 生年月日}] が射影したタプルです。二重の括弧が煩雑なので、t[氏名, 生年月日] と略記します。

{氏名, 生年月日}がRのキー(候補キー)になっていることは、次のように書けます。

  • ∀s, t∈R.(s[氏名, 生年月日] = t[氏名, 生年月日] ⊃ s = t)

この論理式自体はスーパーキーの条件ですが、現実には候補キーの条件しか書きません。

さて、上記の論理式は、固定したRに関しては一階述語論理の論理式です。しかし、Rを動かしたらどうでしょうか。現実のデータベーステーブルを考えれば、そこに格納されるリレーションは変化します。Rが変化してもキー制約を満たすことを言いたいなら次の論理式でしょう。

  • ∀R∈R.∀s, t∈R.(s[氏名, 生年月日] = t[氏名, 生年月日] ⊃ s = t)

ここで太字斜体のRは、テーブルに許容されるリレーションの集合です。リレーション(タプルの集合)の集合であるRや、リレーションの束縛変数Rなどが登場しているので、上記論理式は高階(二階以上)の述語論理式です*5

属性集合AとBのあいだに関数従属性があることは次のように書けます。

  • ∀R∈R.∀s, t∈R.(s[A] = t[A] ⊃ s[B] = t[B])

これももちろん、高階の述語論理式です。A = {氏名}、B = {学年} とすると、

  • ∀R∈R.∀s, t∈R.(s[氏名] = t[氏名] ⊃ s[学年] = t[学年])

そうです、最初の例に挙げた「1人の人間が異なる2つの学年をもつことはない」です。詳しく言えば、「sとtが同じ氏名を持つ(同一人物)ならば、sの学年とtの学年は同じ」です。この制約条件は、特定のリレーションでたまたま成立することではなくて、時間がたとうが別な学校であろうが成立する普遍的法則です。その普遍性の表現のためには、高階の述語論理式が必要なのです。

露骨に高階述語論理を出すのは憚〈はばか〉られるにしろ、制約や正規化の背景に高階の構造があることは意識して説明すべきだと僕は思います。

外部世界をチャンと考慮しよう

前節で、「1人の人間が異なる2つの学年をもつことはない」のようなルール/制約が登場しました。これらのルール/制約は、どこからやって来るのでしょうか? リレーションをいくら眺めても、ルール/制約は書き込まれていません。ルール/制約は、リレーションの世界で発生したものではなくて、外部世界に由来します。

つまり、外部世界に対する認識がなければ、データベースのルール/制約を書き下すことは出来ません。外部世界の構造は、例えばER図で表現されるでしょう。そのER図にルール/制約は写し取られているはずです。(詳細は別途記述予定。)

奥野さんはp.4で、「実は、ER図とリレーショナルモデルは何の関係もありません。」と書いています。外部世界のモデリングと、リレーショナルモデルを混同するな! という趣旨でしょうが、「何の関係もありません」は言い過ぎです。もし、外部世界とリレーショナルモデルが無関係なら、ルールや制約は、その動機も根拠も失います*6

別な思考実験をしてみます。今、矛盾検出が出来る演繹データベースがあるとしましょう。学生の履修登録をしたら矛盾が生じたとします。履修テーブルのデータが悪かったのでしょうか? それとも学校の履修ルールに間違いがあったのでしょうか? どちらが悪いのかはシステム内で判断できません。

そんなとき我々は、外部世界、つまり現実を見ます。現実と較べて、履修登録を取り消すか、または履修ルールを修正します。最終的な拠り所は、リレーションでもルール/制約でもなく、現実=外部世界です。

論理には構文論(証明論)と意味論(モデル論)があります。リレーション/ルール/制約を記述する論理式は構文論に属します。矛盾が生じることは構文論的(証明論的)現象です。「で、どっちが実際に正しいの?」は意味論的(モデル論的)判断です。構文論/意味論的のどちらも必要なのです。

おわりに

冒頭で、「良い点と悪い点の両方を、できるだけ客観的に記述する」と言いましたが、悪い点の指摘のほうが多かったようです。まー、タイトルが「どこがダメなのか」なんでお許しを。

『理論から学ぶデータベース実践入門』の良い点は、純正リレーショナル主義が徹底しているところです。「リレーションは値である」と強調し、リレーショナルなモノと非リレーショナルなモノを区別して話を進めています。

“値であるリレーション”と“器であるテーブル”を区別するために、リレーション変数(p.26)*7という概念も紹介しています。データベースの各種操作を、値と変数というプログラミングの概念で説明できるでしょう。(詳細は別途記述予定。)

僕が目を通してない第9章以降では、一流のデータベース技術者である著者の経験と知見が活かされていることが期待できます。

と、そろそろこの記事はおしまいにします。それにしても、「(詳細は別途記述予定。)」をイッパイ入れちゃったな。いつになるか分からないし、全部書けるかも不安ですが、出来る限り宿題は果たしたいと思います。

*1:奥野さんの書きっぷりは、論理をやった人間を苛立たせるものがあるように僕は感じます。想像ですが、zhanponさんも、幾分か感情的に反応したのではないでしょうか。感情的だったので勇み足をしたんだろう、と -- そう思うのは、僕が若干感情的だからです。つまり、「ムッとなってやった 反省はしていない」。なので、僕も勇み足や言い過ぎがあるかも知れません。
[追記]zhanponさんに確認をとったところ、Qiita記事は「完全に怒り駆動で」書いた、とのことでした。https://twitter.com/zhanpon/status/917759680360751104 ; 文面は怒ってないし、「論理学を誤解して欲しくないので」という名目もちゃんと付いているけど、判断力に影響が出てたと思います。[/追記]

*2:このモデルは、モデル論における“モデル”で、構文としての論理に意味や妥当性を与える実在としての構造物のことです。

*3:要するに、「オカシイことが起きた」とき、オカシイかどうかを判断する論理式を体系内に放り込んでおけば、「矛盾が生じた」と言い直せるのです。

*4:執筆当時のマイブームだったのでしょう。

*5:実際的には、KeyConstraint氏名,生年月日(R) := ∀s, t∈R.(s[氏名, 生年月日] = t[氏名, 生年月日] ⊃ s = t) と高階述語KeyConstraint氏名,生年月日を定義して、それを使ってリレーション型(外延としてはリレーションの集合)を定義することになるでしょう。

*6:リレーショナルモデルをリレーションの算術(代数的演算体系)とだけ捉えて、「ER図とは無関係」と言ったのかも知れません。そうだとしても、その演算体系によりモデル化する世界を無視するのはいかがなものでしょう。

*7:「リレーション」という言葉をずっと使っているのに、なぜかここだけは「関係変数」となってます。

ntgaurantgaura 2017/10/10 22:19 これ読みながらずっと関係論理( https://ja.wikipedia.org/wiki/%E9%96%A2%E4%BF%82%E8%AB%96%E7%90%86 )と述語論理 を言葉として間違えてるのかなー・・・?って思っていました。それ以外の記述が完璧なのでその辺が作者にとって苦手な所なのかなーって思って、それ以外の面白い部分を取り入れさせてもらった感じです。
というわけで多分著者が言いたかったのは関係論理か関係モデルかのどっちかで語るべきなのかなあという印象を持ってるんですがどうでしょう。

m-hiyamam-hiyama 2017/10/11 09:57 ntgauraさん、
> 関係論理と述語論理を言葉として間違えてるのかなー・・・?って思っていました。
さすがにそれはないでしょう。著書のなかで、簡単ではありますが、限量子の説明も、自然演繹に基づく証明の話もしてます。(間違いがあるけど)二階論理にも触れてます。
> 多分著者が言いたかったのは ...
著者が実際に何を言いたかったのかは分かりません。が、このブログ記事に推測は述べています。著者・奥野さんは述語論理を必要と感じていたと思います。だから第2章をいれたのでしょう。

ntgaurantgaura 2017/10/15 21:33 m-hiyama さん
お返事ありがとうございます。
えーとまず限量子については関係論理にも存在します。(念のために、関係論理であって、命題論理じゃないですよ)

ただ確かに二階論理に拡張したものは(存在するようですが)基礎的に使われているかというと疑問がありますね。
何がいいたいかというと、関係論理が述語論理のアイディアを元に確かに作られていて、しかし関係論理という言葉があまり使われないものだから、著者の方は「これこそが述語論理」と思って関係論理を学んでいたのではないか、ということです。実際に技術を使うことを主な仕事にしている技術者としては、この手の用語の混乱はよくある話で、あまり目くじらを立てるモノでもないなあと思っています。(と言うのは個人の邪推と感想ですが。)

とにかく一連の話で、歴史的にも関係データベースの基礎理論であるはずの、関係論理という言葉があまりにも使われないので、一つ触れておきたかった感じです。お気に触ったらすいません。

m-hiyamam-hiyama 2017/10/16 12:02 ntgauraさん、
返答が短すぎましたね。補足します。

> 関係論理という言葉があまりにも使われないので、
まず、著者・奥野さんが「関係論理」という言葉と内容を知らなかったとは考えにくいです。勉強家ですからね。
著書で「関係論理」を使わなかったのは、「使う必要がない」または「使うべきではない」と考えたからでしょう。
以上は推測ですが、(奥野さんではなく)僕の意見は「『関係論理』という言葉は使うべきではない」です。
関係論理に固有なアイディアや概念は特になく、「リレーショナルの演算を説明する目的」「データベースの教科書に引用する目的」で述語論理の一部を切り取ったものを関係論理と呼んでいるだけだからです。この言葉が必要なのは、歴史の話をするときだけでしょう。
リレーショナルモデルは、そうじゃなくても独特の方言・隠語が多くて苦労するのに、これ以上変な方言・隠語を増やしてほしくないです。
その意味で、奥野さんが標準的な用語を選んだ事に賛同します。

2017-10-03 (火)

IT業界は素粒子がお好き?

| 12:22 | IT業界は素粒子がお好き?を含むブックマーク

RSSの配信フォーマットのひとつにAtomという仕様がありました。いや、今でもあります。が、現時点でAtomというと、Atomエディタを思い浮かべる人のほうが多いでしょう。

Atomエディタの基本部分をアプリケーション・フレームワークとして切り出したものはElectronという名前です。原子の構成要素だから電子なんでしょう。

電子があるなら陽子もあるかな? と検索してみたらProton Mailってのがありました。

安全な機密メール機能を提供するサービスのようです。同様な趣旨のProton VPNというのもあるので、Protonファミリーと呼べるかも知れません。(ほんとの陽子はファミリーを形成しないと思うけど。)

中性子(neutron)、ニュートリノ(neutrino)、レプトン(lepton)という名前のソフトウェアもあるようです。

こんな検索をしてみたは、次の記事で紹介されているFirefoxのバージョン(あるいは世代)がFirefox Quantumで、そのUIの名称はPhoton UIだと知ったからです。

量子だ光子だって、なんかカッコイイ -- って感じるメンタリティは幼稚な気もするけど、僕もそういうメンタリティだから、このテの名前を付けたくなる気持ちは分かります。

目ぼしいソフトウェアで重力子(graviton)って名前のはまだないようです。早い者勝ちだね。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171003

2017-10-02 (月)

証明の“お膳立て”のやり方 3: さらに事例

| 10:15 | 証明の“お膳立て”のやり方 3: さらに事例を含むブックマーク

証明の“お膳立て”のやり方」、「証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル」の続きです。このテの話は具体例がないとなかなかピンと来ないので事例を追加します。

内容:

  1. 証明要求の事例
  2. “お膳立て”の全体像
  3. 証明要求の書き換え
  4. 証明に必要なこと

証明要求の事例

A, Bを集合として、f:A→B は写像とします。この状況で次の命題を考えます。

この命題が真か偽か、現時点では分かりません。そこで、次の証明要求を発行します。

  • Γ/ (A, B : Set), f:A→B |-? fは可逆 ⇔ fは全単射

証明要求とは、「証明できますか?」という疑問文、または「証明をしなさい」という(命令的)問題文です。証明可能性判断とは違って、証明の存在を保証してはいません。結局は証明できない(証明が存在しない)って事もあります。

Γ(大文字ガンマ)は、証明に使う諸々の予備知識・背景知識を表しています。`(A, B : Set)`は「A, Bを集合とする」を意味し、`f:A→B`は「fがAからBへの写像である」ことを述べています。記述が簡単になるように、`(A, B : Set), f:A→B`をΓに含めてしまって、以下、次のように書くことにします。

この証明要求(疑問文、問題文)に応える証明が在るにしろ無いにしろ、証明要求をより簡単な形に書き換えることは出来ます。これからその書き換えをします。証明要求は、証明という作業の仕様書・発注書のように考えることができます。このような比喩については「証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル」に書いています。

証明要求の書き換えとは、論理の言葉で言えば、シーケント計算の一部を逆向きに実行することです。しかしここでは、形式的体系の話ではなくて、実際の非形式的証明(半形式的証明かな)のやり方として取り扱います。証明要求の書き換えは、本チャンの証明の事前準備と捉えています。よって、証明の“お膳立て”と呼んでいるのです。

“お膳立て”の全体像

証明要求「Γ |-? fは可逆 ⇔ fは全単射」に対する“お膳立て”をしてみると、作業ステップが意外と多いので、証明要求に番号を付けて整理します。枝番方式を採用します。番号付けルールは:

  1. 番号xの要求が2つの要求に分解されたときは、x-1, x-2 と番号を付ける。
  2. 番号xの要求が順次変形されていくときは、x → x.1 → x.2 → ... と番号を付けていく。

もとの証明要求にRと名前を付けて、お膳立ての作業進行に従って枝番を付けていくと、全体は次のようになります。

                        R
  -----------------------------------------------[∧]
            R-1                      R-2
           --------[⇒]             -------[⇒]
            R-1.1                    R-2.1
           --------[同値]           -------[同値]
            R-1.2                    R-2.2
  --------------------------[∧]    -------[同値]
   R-1.2-1         R-1.2-2           R-2.3
  ---------[同値] ----------[同値]
   R-1.2-1.1       R-1.2-2.1
  ---------[∀]   -----------[∀]
   R-1.2-1.2       R-1.2-2.2
                  -----------[⇒]
                   R-1.2-2.3

横線右に添えられているラベルは、証明要求の書き換え方法で、次の意味です。

  1. [∧] 結論が連言'∧'を含むとき、2つの証明要求に分解する。
  2. [⇒] 結論が含意'⇒'を含むとき、含意の前件('⇒'の左側)を前提('|-?'の左側)に移動する。
  3. [同値] 結論、または前提の命題を同値な命題で置き換える。
  4. [∀] 全称限量子を取り去り、前提に自由変数の型宣言を加える。

証明要求の書き換え

以下、上段に書き換え前(before)の証明要求、下段に書き換え後(after)の証明要求を書くフォーマットで書き換えを記述していきます。適宜、前節の全体像を参照してください。

RからR-1とR2への分解、R-1.2からR-1.2-1とR-1.2-2への分解は省略します。次の4つの部分を記述します。

  1. R-1 から R-1.2 まで
  2. R-2 から R-2.3 まで
  3. R-1.2-1 から R-1.2-1.2 まで
  4. R-1.2-2 から R-1.2-2.3 まで
R-1 から R-1.2 まで
  (R-1) Γ |-? fは可逆 ⇒ fは全単射
 --------------------------------------------[⇒]
  (R-1.1) Γ/ fは可逆 |-? fは全単射
 --------------------------------------------[同値]
  (R-1.2) Γ/ fは可逆 |-? fは全射 ∧ fは単射
R-2 から R-2.3 まで

  (R-2) Γ |-? fは全単射 ⇒ fは可逆
 -------------------------------------[⇒]
  (R-2.1) Γ/ fは全単射 |-? fは可逆
 ------------------------------------------[同値]
  (R-2.2) Γ/ fは全単射 |-?
          ∃g:B→A.(f;g = idA ∧ g;f = idB)
 ------------------------------------------[同値]
  (R-2.3) Γ/ fは全射, fは単射 |-?
          ∃g:B→A.(f;g = idA ∧ g;f = idB)

R-1.2-1 から R-1.2-1.2 まで
  (R-1.2-1) Γ/ fは可逆 |-? fは全射
 ------------------------------------------------------[同値]
  (R-1.2-1.1) Γ/ fは可逆 |-? ∀y∈B.∃x∈A.(f(x) = y)
 ------------------------------------------------------[∀]
  (R-1.2-1.2) Γ/ fは可逆, y : B |-? ∃x∈A.(f(x) = y)
R-1.2-2 から R-1.2-2.3 まで
  (R-1.2-2) Γ/ fは可逆 |-? fは単射
 --------------------------------------------------------------[同値]
  (R-1.2-2.1) Γ/ fは可逆 |-? ∀x, y∈A.(f(x) = f(y) ⇒ x = y)
 --------------------------------------------------------------[∀]
  (R-1.2-2.2) Γ/ fは可逆, (x, y : A) |-? f(x) = f(y) ⇒ x = y
 --------------------------------------------------------------[⇒]
  (R-1.2-2.3) Γ/ fは可逆, (x, y : A), f(x) = f(y) |-?  x = y

証明に必要なこと

“お膳立て”の全体像は、上から下に広がるツリーの形をしています。最上部(ルート)がもとの証明要求です。末端(葉)が書き換えを終えた証明要求です。末端の証明要求だけを並べると次の3つです。

  1. (R-2.3) Γ/ fは全射, fは単射 |-? ∃g:B→A.(f;g = idA ∧ g;f = idB)
  2. (R-1.2-1.2) Γ/ fは可逆, y : B |-? ∃x∈A.(f(x) = y)
  3. (R-1.2-2.3) Γ/ fは可逆, (x, y : A), f(x) = f(y) |-? x = y

この3つの証明要求に応える証明を書けば、もとの証明要求に応えたことになります。(R-1.2-1.2)と(R-1.2-2.3)は簡単なので、証明のハイライトは(R-2.3)に対する証明です。

写像 f:A→B に対して、点ごとの逆像を対応させる写像 f*:B→Pow(A) を定義して、次の補題を利用するのがよいでしょう。([追記]証明の“お膳立て”のやり方」でもf*という記号を使いましたが、あっちは f*:Pow(B)→Pow(A)、今回は f*:B→Pow(A) なので違います。注意してください。[/追記]補題の利用法については「証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル」に書いてあります。

  • fが全射 ⇔ ∀y∈B.(f*(y) は空集合ではない)
  • fが単射 ⇔ ∀y∈B.(f*(y) は空集合または単元集合)

予備知識・背景知識の集合であるΓには、次の命題が入っているとします。

  • 写像 G:B→Pow(A) において、∀y∈B.(G(y) は空集合ではない) ⇒ ∀y∈B.(g(y)∈G(y)) となる g:B→A が存在する

すべて論理記号を使って書くなら:

  • ∀G:B→Pow(A).( (∀y∈B.(G(y) ≠ 空集合)) ⇒ ∃g:B→A.∀y∈B.(g(y)∈G(y)) )

この命題は選択公理と呼ばれる命題で、通常は証明なしに認めます。なので、Γに入れておきます。

ここまでお膳立てが済んでいるなら、残りの証明は難しくはないと思います。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171002

2017-09-29 (金)

おススメのネコ動画

| 10:33 | おススメのネコ動画を含むブックマーク

ネコパンチの動画は色々ありますが、↓これはホントに凄い。ガチのボクシング・ファンです。

D

傑出した身体能力を持つネコちゃん↓のジャンプ。カメラワークと編集も素晴らしい。カッコイイ!

D

なんか笑っちゃう↓。ズンズン歩いてくるところが面白い。

D

[追記]動画のオーナーである楽小漫(a.k.a. フェイリス)さんがYouTubeのチャンネルを閉鎖してしまったので、この下にあった動画へのリンク(埋め込みプレイヤー)は削除します。コピーされた動画なら残っていますがリンクはしません。中国版ニコ動bilibiliに、同じ曲・同じ二人の「踊ってみた」がありますが、ネコがいない(泣)→ http://www.bilibili.com/video/av683152/[/追記]

歩くフィギュアみたいな女の子二人↓。そのうちの一人が咬人猫だからネコ? じゃなくて、画面をよく見るとネコがいます。1:00で一旦退場後に1:17で再登場、1:40に二人のあいだを走り抜けます。

こちらの「踊ってみた」↓ではネコ出ずっぱり。ほとんど動かないけど。

D

最後に、リアルな猫の生態を捉えたネコ動画。ちょっとホロッとする。

D

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170929

2017-09-26 (火)

証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル

| 16:48 | 証明の“お膳立て”のやり方 2: 証明の顧客・業者モデルを含むブックマーク

昨日の記事「証明の“お膳立て”のやり方」の続きを書きます。発展編と言えるかも知れません。

昨日“お膳立て”という言葉を使った理由は、形式的論理体系の話ではなく、コンピュータによる証明の話でもなく、人間が例えば「f:A→B は全射 ⇔ f*:Pow(B)→Pow(A) は単射」のような命題を手動で証明するときの“やり方”に関わる話だったからです。

今回も“やり方”の話です。メイヤー流の顧客・業者モデルを導入して、“お膳立て”の意義を確認・整理したいと思います。

内容:

  1. 文脈知識と仮定
  2. ターゲットからの論理記号の除去
  3. 背理法を使うとき
  4. 証明における顧客と業者
  5. インテグレーターの憂鬱
  6. 定義と補題の利用
  7. ターゲットの取り替え
  8. まとめ

文脈知識と仮定

証明可能性判断(provability judgement)から話を始めます。証明可能性判断は次の形に書くのでした。

  • P1, ..., Pn |- Q

nは任意の自然数なので、もの凄く大量の仮定があってもかまいません。しかし、通常は2,3個の仮定を書く程度でしょう。実際にはその他の仮定があっても、それは暗黙の仮定として書かないと思います。

この暗黙の仮定のために、事情が不透明になることがあるので、証明可能性判断の左側にはすべての仮定を書くことにします。しかし、明示的な仮定と暗黙の仮定を分けて次のように書きます。

  • R1, ..., Rk/ P1, ..., Pn |- Q

R1, ..., Rk が暗黙の仮定(って、もはや暗黙じゃないけど)で、P1, ..., Pn が明示的仮定です。R1, ..., Rk をΓのようなギリシャ文字大文字で表すことにします。

  • Γ/ P1, ..., Pn |- Q

Γのことを予備知識、背景知識、文脈知識などと呼びます。単に背景(background)、文脈(context; コンテキスト)とも言います。スラッシュより右に書く明示的仮定は単に仮定と呼びましょう。そして、'|-'の左側全体を前提(premises)と呼ぶことにします。証明要求においても同じ用語法を使います。

文脈知識と仮定の区別は、便宜的・恣意的なもので、確たる根拠はありません。したがって、スラッシュの位置はどこに移動してもかまいません。区切り(スラッシュ)の位置を変えてもいいことは次のように表現できます。

   Γ, R/ P1, ..., Pn |- Q
 ----------------------------[文脈から仮定へ]
   Γ/ R, P1, ..., Pn |- Q


   Γ/ P1, P2, ..., Pn |- Q
 ----------------------------[仮定から文脈へ]
   Γ, P1/ P2, ..., Pn |- Q

この事情は証明要求(proof requirement)のときも同じです。

   Γ, R/ P1, ..., Pn |-? Q
 ----------------------------[文脈から仮定へ]
   Γ/ R, P1, ..., Pn |-? Q


   Γ/ P1, P2, ..., Pn |-? Q
 ----------------------------[仮定から文脈へ]
   Γ, P1/ P2, ..., Pn |-? Q

文脈知識と仮定の境界線を動かしてもいいことは、理論的にはたいした意味はないです。そもそもそんな区別はしないのが普通です。しかし、現実的にはけっこう意味があって、境界線とその移動に対して意識的・自覚的になったほうがいいと思います。文脈知識(=暗黙の仮定)がズレていてコミュニケーションがうまくいかない事態は頻繁に起きます。区切り(スラッシュ)位置の調整と合意がコミュニケーションでは重要なのです。

ターゲットからの論理記号の除去

証明要求において、'|-?'の右に書く命題(論理式)をターゲット(target)と呼ぶことにします。ゴールでも同義ですが、証明支援系における「ゴール」が甚だしく混乱しているので、「ゴール」という言葉は避けます。

さて、与えられた証明要求に対してお膳立て(事前処理)を施す主な動機は、証明要求のターゲットをより簡単にしたいことです。ターゲットに論理記号がたくさん含まれれば複雑な論理式ですから、論理記号を減らそうと試みるのです。

論理記号(慣用のもの)には、次があります。

  1. ¬

このなかで、∧, ⇒, ∀を除去するお膳立てルール(=バックワード・リーズニングのルール)は「証明の“お膳立て”のやり方」で述べました。念のために再掲します。Γは文脈、Δは(明示的)仮定です。

      Γ/ Δ |-? P∧Q
 ------------------------------[連言の分解]
  Γ/ Δ |-? P   Γ/ Δ |-? Q
  Γ/ Δ |-? P⇒Q
 ------------------[含意の変形]
  Γ/ Δ, P |-? Q
  Γ/ Δ |-? ∀x∈X.Q
 ----------------------[全称の変形]
  Γ/ Δ, x : X |-? Q

ターゲットに ∨, ¬, ∃ が含まれる場合はどうでしょうか? 次節以降で考えてみます。

背理法を使うとき

背理法を使うときは、事前に「背理法で証明します」のように断りを入れます。この断り書きは、お膳立ての一種です。お膳立てとは証明要求の変形ですが、背理法を使う直前に次の変形が行われるのです。

  Γ/ Δ |-? ¬Q
 -------------------[背理法]
  Γ/ Δ, Q |-? ⊥

ここで、'⊥'は矛盾を表す記号です。具体例として、「√2は有理数ではない」の証明要求で考えてみると:

  Γ/ |-? `¬(√2は有理数)`
 -----------------------------[背理法]
  Γ/ `√2は有理数` |-? 矛盾

もともとの証明要求は、諸々の予備知識Γから、`¬(√2は有理数)`を証明せよ、と要求しています。これを、予備知識Γと仮定`√2は有理数`から矛盾を証明せよ(矛盾を導き出せ)、と変形しています。

「お膳立てで論理記号を減らす」という動機から見ると、もともとはターゲットに否定'¬'が含まれていたのが、変形後に'¬'が消えているので、背理法のお膳立ては、否定記号を除去するお膳立てだと言えます。

証明における顧客と業者

メイヤー先生は、ソフトウェア仕様に関して、顧客(customer)と業者(provider, supplier)のあいだの契約(contract)という比喩を導入しました。この比喩的モデルは実に秀逸で、ソフトウェア仕様の基本概念を日常的な感覚で理解できるようになりました。興味がある方は、例えば次の記事を見てください。

証明においても、顧客・業者モデルを導入してみましょう。証明を請け負う“証明屋”という業者がいるとします。顧客は、業者“証明屋”に証明の作成を依頼します。業者は、顧客の依頼に応えて、成果物を納品します。依頼するときに契約が交わされ、納品時に契約が履行されたことが確認されます。

証明依頼のときの指示書・仕様書が、今話題にしている証明要求です。成果物=納品物が証明です。ここでいう証明は、形式的な証明オブジェクト/タクティク言語で書かれた証明スクリプト/自然言語で書かれた伝統的証明などで、顧客と業者のあいだで合意があるならフォーマットは自由に選べます。

顧客と業者のあいだの契約の条件は、全て証明要求に書き込まれています。したがって、納品物のチェックも証明要求を基準にします。証明要求が Γ/ Δ |-? Q だとして、次の事は契約違反になります。

  • ΓにもΔにも入ってない命題が仮定として使われた。
  • Qと異なる命題が結論になっている。

より大枠に関する契約違反としては:

  • 納品された証明のフォーマットが合意されたものではない。
  • 納品された証明のなかに、顧客が解釈できない部分/許容できない部分がある。

上記のような不備がなければ、納品チェックはパスして、契約は履行されたとみなされます。

今話題にしている“お膳立て=証明要求の書き換え”は、(世間によくある)元請け・下請けを考えれば理解できます。元請けが下請けに発注(再依頼)するとき、指示書・仕様書は書き換えられます。“丸投げ”ってヤツもありますが、ここでは丸投げは考えません

例えば、次の“お膳立て=証明要求の書き換え”を考えてみます。

      Γ/ Δ |-? P∧Q
 ------------------------------[連言の分解]
  Γ/ Δ |-? P   Γ/ Δ |-? Q

もとの証明要求を2つに分解し、2つの下請け業者に発注します。上がってきた下請け成果物をまとめれば、もとの証明要求を満たす成果物を顧客に納品できる、というわけです。

インテグレーターの憂鬱

ソフトウェア業界には、システムインテグレーターと呼ばれる業種があります。顧客と契約を交わす元請けと思えばいいでしょう。証明業界(架空の業界)にもインテグレーターがいるとしましょう。証明インテグレーターは、顧客からの証明要求を若干書き換えて下請け業者に発注します。下請けへの発注では、もとの証明要求よりは簡単な要求にします -- 良心的ですね*1

ターゲットに、∧(連言), ⇒(含意), ∀(全称), ¬(否定)を含む証明要求を、より簡単(論理記号が減っている)証明要求にして下請けに出すのは割とスンナリいきます。しかし、∨(選言)と∃(存在)の“お膳立て=証明要求の書き換え”はちょっと難しい。

Γ/ Δ |-? P∨Q の形の、ターゲットが選言'∨'を含む証明要求の場合も、2つの証明要求に分解はできます。

  1. Γ/ Δ |-? P
  2. Γ/ Δ |-? Q

しかし、連言の場合とは違います。下請けに出した後の納品待ちがまったく違うのです。連言'∧'の場合は、2つの下請け業者両方の納品を待ちますが、選言'∨'の場合は、どちらか一方から納品があれば(もう一方を待たずに)、ただちに顧客への納品を完了させます。

余談ですが、'∧'と'∨'に関する下請けへの出し方/待ち方は、並列プロセスの制御方法と類似しています。証明行為とプログラム実行に何らかの関係があることを示唆しています。

さて、残るはターゲットが'∃'を含む証明要求です。どのように“お膳立て=証明要求の書き換え”をして下請けに出せばいいのでしょうか?

存在'∃'が付く命題は、選言'∨'がイッパイある命題と思えます。例えば、`∃n∈N.P(n)`という自然数に関する命題は、P(0), P(1), P(2), ... を選言で繋いだ P(0)∨P(1)∨P(2)∨ ... と同じです。ということは、無限個の証明要求を作って無限の下請け業者に発注して、どれでもいいから納品があるのを待つことになります。

では、実数に関する命題`∃x∈R.P(x)`がターゲットならどうでしょうか。連続無限個の証明要求を作って連続無限の下請け業者に発注します。でも、連続無限個の証明要求って、具体的にどうやって書き上げるのでしょうか? お膳立ての段階で、神様の(超越的な)能力が要求されます。

という事情で、ターゲットが存在命題`∃x∈X.P(x)`であるときのお膳立ては困難です。無限個の証明要求に書き換えるよりは、存在命題を同値な命題に置き換えたり、Xの具体的要素を表す項tをなんとか探し出して、P(t)を証明することになるでしょう。

[追記]

証明要求 Γ/ Δ |-? P∨Q を2つに分解して、どちらかの(どっちでもいい)証明を要求することが悪いわけではありません。が、他の書き換えのほうが適切な場合もあります。例えば、ターゲットを二重否定してみます。≡はメタな意味の同値性を表す記号として:

  • P∨Q ≡ ¬¬(P∨Q) ≡ ¬(¬P∧¬Q)

背理法を使うことにすれば:

  Γ/ Δ |-? P∨Q
 -------------------------[同値]
  Γ/ Δ |-? ¬(¬P∧¬Q)
 -------------------------[背理法]
  Γ/ Δ, ¬P, ¬Q |-? ⊥

うまく矛盾が導き出せれば、もとの証明要求に応えたことになります。

[さらに追記]証明の“お膳立て”のやり方 4: 随伴による集合差の定義」でさらに詳しい話をしています。[/さらに追記]

[/追記]

定義と補題の利用

証明の“お膳立て”のやり方」の具体例で、次のような“お膳立て済みの証明要求”が登場しました。

  • Γ/ `f*:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `∃S, T∈Pow(B).(f*(S) = f*(T) ∧ S ≠ T)`

ターゲットが存在命題なので、実例を作るしかありません。Im(f)はfの像集合として、S = Im(f), T = B と置くと適切な実例になります。しかし、Im(f)の定義が文脈知識Γにないとしたら、Im(f)という記号を使うことは契約違反になります。思い出してください。

  • 納品された証明のなかに、顧客が解釈できない部分/許容できない部分があれば、契約違反となる。

未知の記号Imは、顧客が解釈できないものです。こんなときは、新しい記号(概念)の定義を、文脈知識か仮定に追加します。次のような命題を追加すればいいでしょう。

  • ∀y∈B.(y∈Im(f) ⇔ ∃x∈A.(y = f(x)))

Imに関連する次の命題も前提に入れたいですね。

これらを文脈知識に入れた証明要求は次のようになります。

  • Γ, `∀y∈B.(y∈Im(f) ⇔ ∃x∈A.(y = f(x)))`, `fは全射 ⇔ Im(f) = B`/ `f*:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `∃S, T∈Pow(B).(f*(S) = f*(T) ∧ S ≠ T)`

イヤッ、ちょっと待って下さい。契約履行の基準のなかに次があります。

  • ΓにもΔにも入ってない命題が仮定として使われたなら、契約違反となる。

`∀y∈B.(y∈Im(f) ⇔ ∃x∈A.(y = f(x)))`, `fは全射 ⇔ Im(f) = B` は、もとの前提(文脈または仮定)に入ってません。それを証明内で使えば、契約違反となるのではないでしょうか。

実は大丈夫です。契約違反として禁止されている行為は、無根拠に勝手に前提を増やしてしまうことです。すぐ上で行った行為は、証明作業の中間段階で定義や補題を利用してるだけです。もともと指定された前提を勝手に増やしてはいません。

この事情は、証明可能性判断と証明要求を一緒に使って説明できます。

  Γ/ Δ |-? Q   Γ/ Δ |- R
 -----------------------------[定義・補題の追加]
      Γ/ Δ, R |-? Q

顧客・元請け・下請けモデルで考えると分かりやすいです。上段左がもとの証明要求です。元請けが作業をして、Rの証明は出来上がっています(上段右)。元請けによる作業結果を前提に追加して、下請けに出す新しい証明要求を作ります。それが下段です。下段の証明要求に応える証明(=成果物=納品物)が下請けから上がってくれば、元請けは契約違反することなく顧客に納品できます。

つまり、前提が増えているのは元請けから下請けへの証明要求でのことで、増やした理由は Γ/ Δ |- R という証明が既にあるからです。勝手に増やしてはいません。定義の導入には特に前提を必要としないので、これももとの前提を勝手に増やしたことにはなりません。

ターゲットの取り替え

顧客と業者のあいだの契約上の禁止事項に次のものがありました。

  • 証明要求で指定されたターゲットとは異なる命題が結論になっていれば、契約違反となる。

これは当たり前で、要求と異なる事をやっても認められません。しかし、元請け・下請けのあいだでは証明要求のターゲットを書き換えることはあります。

  Γ/ Δ |-? Q   Γ/ Δ |- R⇒Q
 -------------------------------[ターゲットの取り替え]
      Γ/ Δ |-? R

分かりますよね。元請け側で`R⇒Q`の証明を済ましている(上段右)ので、下請けに出す証明要求(下段)ではRをターゲットにしているのです。下請けからRの証明が上がってくれば、元請けがQの証明を作って納品することは容易です。契約違反は犯してません。

まとめ

メイヤー先生にならい、証明も顧客・業者モデルで考えることにしました。“お膳立て=証明要求の書き換え”は、元請けが下請けに発注するときに新しい証明要求を作る作業に喩えることができます。

証明要求のターゲットが選言(∨)と存在(∃)を持つとき、それを取り除いて下請けに発注することは難しいです。それ以外の場合、∧, ⇒, ∀, ¬を取り除いて下請けに発注する方法、それと一部の証明を元請け側でやってから下請けに発注する方法を以下に並べます。

      Γ/ Δ |-? P∧Q
 ------------------------------[連言の分解]
  Γ/ Δ |-? P   Γ/ Δ |-? Q
  Γ/ Δ |-? P⇒Q
 ------------------[含意の変形]
  Γ/ Δ, P |-? Q
  Γ/ Δ |-? ∀x∈X.Q
 ----------------------[全称の変形]
  Γ/ Δ, x : X |-? Q
  Γ/ Δ |-? ¬Q
 -------------------[背理法]
  Γ/ Δ, Q |-? ⊥
  Γ/ Δ |-? Q   Γ/ Δ |- R
 -----------------------------[定義・補題の追加]
      Γ/ Δ, R |-? Q
  Γ/ Δ |-? Q   Γ/ Δ |- R⇒Q
 -------------------------------[ターゲットの取り替え]
       Γ/ Δ |-? R

元請けから下請けに回る段階で、もとの要求より易しい要求になっている点に注意してください。実に良心的な下請け構造なのです。

これは、元請けが“お膳立て=証明要求の書き換え”を適切に行えば、下請けの証明作業が必ず簡単になることを意味します。この比喩で、お膳立ての意義と重要性が分かるでしょう。

*1:現実世界では、無理難題を下請けに押し付けて、オイシイところだけは元請けで担当するなんてこともありそうです。

2017-09-25 (月)

証明の“お膳立て”のやり方

| 13:56 | 証明の“お膳立て”のやり方を含むブックマーク

N君が「こういうのは、どうやって証明したらいいのか… わかんないなー?」と困った顔をしてました。的確な処方箋を述べることは出来ないのですが、ヒントになりそうなことを記しておきます。

目的:

  1. 証明の“お膳立て”とは
  2. 例題
  3. 命題、証明可能性判断、証明要求
  4. 連言の分解
  5. 含意の変形
  6. 全称限量子を型宣言に
  7. お膳立てルールの繰り返し適用
  8. 同値な命題に置き換える
  9. お膳立てを完成させる

シリーズ目次:

  1. 証明の“お膳立て”のやり方
  2. 証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル
  3. 証明の“お膳立て”のやり方 3: さらに事例
  4. 証明の“お膳立て”のやり方 4: 随伴による集合差の定義
  5. 証明の“お膳立て”のやり方 5: 証明可能性判断と推論規則

証明の“お膳立て”とは

何らかの命題を証明するとき、状況を確認したり、仮定と結論を整理したり、命題をより扱いやすい形に変形したりします。こういうことも証明行為(リーズニング)の一部だといえますが、プリプロセス(前段階の処理)っぽい雰囲気があるので、ここでは“お膳立て”と呼んでおきましょう。

簡単な証明なら出来るけど、少し複雑になると「どこから手を付けていいか分からない」という人は、このお膳立てがうまくいってないことがあるように思えます。

とはいえ、お膳立てを正確に定義することも、体系的に手順・コツを提示することも出来ないので、具体的な例に沿って、その例のなかに出てくる幾つかの手法を説明します。

例題

f:A→B は写像とします。Pow(B)は、集合Bのベキ集合(powerset)です。つまり、S∈Pow(B) ⇔ S⊆B ですね。f*:Pow(B)→Pow(A) は、Bの部分集合に“fによる逆像”を対応させる写像です。詳しく言えば:

  • f*(S) = {x∈A | f(x)∈S}

f*はf-1と書かれることが多いですが、fの逆写像ではないので上付きアスタリスクにします。

さて、次の命題を例に使います。

  • f:A→B は全射 ⇔ f*:Pow(B)→Pow(A) は単射

この命題を普通の方法(集合と写像に関する議論)で証明することを考えます。

命題、証明可能性判断、証明要求

ある命題(形式的に扱う場合は論理式)Qに対して、それが証明可能であることを意味するメタ命題を次の形に書きます。

  • |- Q

この形のメタな主張を証明可能性判断(provability judgement)と呼びます。「Pが証明できる」ということを記号的に書いただけです。

P1, ..., Pn という幾つかの命題を仮定としてQを証明できることは、次のように書きます。

  • P1, ..., Pn |- Q

一般的には、Qを証明するために必要な仮定命題はイッパイあります。それを全部並べると大変なので、暗黙の予備知識のような命題までは書き並べません。ここでは、特に注目してない諸々の前提達をΓ(大文字ガンマ)で表します。Γは命題の集合だと思ってください。例えば、全射・単射の定義とか、x∈A ⇒ f(x)∈B のような当たり前な命題は全てΓに入っているとします。ここだけの用語法ですが、特に注目している仮定命題を単に「仮定」と呼び、暗黙の予備知識なども含めた全体を「前提」と呼びます。

扱っている命題が地の文と紛らわしいときは、命題をバッククォートで囲むことにします。例えば、`x∈A ⇒ f(x)∈B`のように。

命題Pが証明可能かどうかは分かってない状態で、「証明できるでしょうか?」という疑問文、あるいは「証明を試みてください」という問題文の記述として、次の形を使うことにします。

  • |-? Q

使ってよい仮定、あるいは暗黙の前提も指定した形は:

  • P1, ..., Pn |-? Q
  • Γ, P1, ..., Pn |-? Q

この形を証明要求(proof requirement)と呼ぶことにします。

前節で述べた例題を証明要求として書けば:

  • Γ |-? `f:A→B は全射 ⇔ f*:Pow(B)→Pow(A) は単射`

Γは使ってもよい諸々の前提だとします。`Aは集合`とか`∀S∈Pow(B).∀x∈A.(x∈f*(S) ⇔ f(x)∈S)`などもΓに入っているでしょう。暗黙の前提Γはけっこう膨大になったりします。

連言の分解

最初のお膳立ては、証明すべき命題(ゴール、ターゲット)が連言(論理AND)で書かれているとき、証明要求を2つ(以上)に分解することです。

`f:A→B は全射 ⇔ f*:Pow(B)→Pow(A) は単射`という命題には、連言が入っています。なぜなら、`P ⇔ Q`は、`(P⇒Q)∧(Q⇒P)`のことだからです。連言('∧')を明示的に書けば:

  • (f:A→B は全射 ⇒ f*:Pow(B)→Pow(A) は単射)∧(f*:Pow(B)→Pow(A) は単射 ⇒ f:A→B は全射)

もとの証明要求は、次の2つの証明要求になります。

  1. Γ |-? `f:A→B は全射 ⇒ f*:Pow(B)→Pow(A) は単射`
  2. Γ |-? `f*:Pow(B)→Pow(A) は単射 ⇒ f:A→B は全射`

一般的には、P∧Qがターゲットである証明要求は、Γ |-? P と Γ |-? Q に分解(decompose, resolve)できます。上段に分解前(before)、下段に分解後(after)を書く書式で表現すれば:

      Γ |-? P∧Q
 ----------------------[連言の分解]
  Γ |-? P   Γ |-? Q

含意の変形

しばらくは、2つに分解した片一方の証明要求に注目しましょう。

  • Γ |-? `f:A→B は全射 ⇒ f*:Pow(B)→Pow(A) は単射`

証明すべき命題に含意記号('⇒')が含まれます。このとき、含意の前件(antecedent, 左側)を、証明要求の仮定側に移してかまいません。つまり、証明要求を次の形に変形*1していいのです。

  • Γ, `f:A→B は全射` |-? `f*:Pow(B)→Pow(A) は単射`

一般的なお膳立てルールとしては:

  Γ |-? P⇒Q
 --------------[含意の変形]
  Γ, P |-? Q

これは、演繹定理(deduction theorem)と呼ばれる、論理の基本法則です。定理と呼んでいますが、これが成立するように証明系を設計するので、論理の指導原理(のひとつ)と言ってもいいでしょう。実際、証明のお膳立てには演繹定理が頻繁に使われます。

なお、演繹定理の圏論的解釈は、順序随伴性: ガロア接続の圏論に書いています。

全称限量子を型宣言に

証明すべき命題`f*:Pow(B)→Pow(A) は単射`が持つ情報のうちで、証明要求の前提側('|-?'の左側)に持っていけるものを移動すると:

  • Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)` |-? `f*は単射`

単射の定義を使って`f*は単射`を展開すると:

  • Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)` |-? `∀S, T∈Pow(B).(f*(S) = f*(T) ⇒ S = T)`

全称限量子'∀'が出てきました。全称限量子の束縛変数S, Tは、ベキ集合Pow(B)上を走る自由変数に置き換えることができます。自由変数の変域を変数の型と考えて、次の形式を使うことにします。

  • S, T : Pow(B)

意味はもちろん、「SとTは自由変数で、その型(変域)はPow(B)である」です。これは、`S : Pow(B)`, `T : Pow(B)` の略記である点にも注意してください。

全称限量子を取り払い、束縛変数を自由変数に置き換え、その変数の型宣言を前提側に置く、という証明要求の変形が許されます。

  • Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)` |-? `f*(S) = f*(T) ⇒ S = T`

一般的なお膳立てルールとしては:

  Γ |-? ∀x∈X.Q
 ------------------[全称の変形]
  Γ, x : X |-? Q

お膳立てルールの繰り返し適用

現時点での証明要求のターゲットに含意'⇒'が出現するので、もう一度、含意の変形ルールを適用します。すると:

  • Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `S = T`

これでターゲットは`S = T`になりました。SとTは集合なので、S = T ⇔ S⊆T ∧ T⊆S です。`S = T`を同値な命題で置き換えると:

  • Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `S⊆T ∧ T⊆S`

連言の分解ルールを適用すると:

  1. Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `S⊆T`
  2. Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `T⊆S`

ターゲットに含まれる包含('⊆')を定義により展開すれば:

  1. Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `∀y.(y∈S ⇒ y∈T)`
  2. Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `∀y.(y∈T ⇒ y∈S)`

さらに全称の変形と含意の変形を適用すると:

  1. Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)`, `y : Any`, `y∈S` |-? `y∈T`
  2. Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)`, `y : Any`, `y∈T` |-? `y∈S`

`y : Any`は、yが制約のない自由変数であることを表します。しかし、直後に`y∈S`があるので、まとめて`y : S`としても同じことです。

ここまで証明要求を変形すれば、使える仮定はだいぶ増えているし、証明すべき結論は簡単な形をしているので、証明が出来そうな気がします。

今までのお膳立ての手順を見てみると、これはバックワード・リーズニングによる証明行為を遂行していることになります。あえて“お膳立て”として証明本体と区別しているのは、証明は通常、フォワード・リーズニングとして書かれるからです。バックワード・リーズニングは、事前調査や予備作業の位置付けになることが多いでしょう。

ちなみに、人間はバックワード・リーズニングを補助的に使い、オフィシャルな証明記述にはフォワード・リーズニングを使いますが、コンピュータによる証明ではバックワード・リーズニングだけを使うほうが主流です。

同値な命題に置き換える

ここで話を戻して、保留にしておいた証明要求を再び取り上げます。

  • Γ |-? `f*:Pow(B)→Pow(A) は単射 ⇒ f:A→B は全射`

この命題は対偶にしたほうがやりやすい気がするので、結論を対偶に置き換えます。対偶に置き換えなきゃダメなわけじゃありませんが、わずかに証明が簡略化するし、置き換えの事例としてやってみます。あと、`f*:Pow(B)→Pow(A)`は前提側に移します。

  • Γ, `f*:Pow(B)→Pow(A)` |-? `f:A→B は全射ではない ⇒ f*は単射ではない`

一般的なお膳立てルールとしては:

  Γ |-? P ⇒ Q
 --------------------[対偶に置き換え]
  Γ |-? ¬Q ⇒ ¬P

対偶に限らず、証明要求の結論や前提に出てくる命題を同値な命題に置き換えることは許されます。既に、定義による置き換えなどは使っていますし。

お膳立てを完成させる

  • Γ, `f*:Pow(B)→Pow(A)` |-? `f:A→B は全射ではない ⇒ f*は単射ではない`

この証明要求の結論にも'⇒'が登場するので、前件を前提側に移します。

  • Γ, `f*:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `f*は単射ではない`

単射の定義を使って結論を同値な命題に置き換えれば:

  • Γ, `f*:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `¬(∀S, T∈Pow(B).(f*(S) = f*(T) ⇒ S = T))`

さらに、ドモルガンの法則を使って結論を同値な命題に置き換えます。

  • Γ, `f*:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `∃S, T∈Pow(B).(f*(S) = f*(T) ∧ S ≠ T)`

あっ、P⇒Q と ¬P∨Q が同値なことも使っています。

さて、今までの経緯をまとめましょう。最初の証明要求は次でした。

  • Γ |-? `f:A→B は全射 ⇔ f*:Pow(B)→Pow(A) は単射`

証明要求に対して許される幾つかの操作を適用することにより、次の3つの証明要求にたどり着きました。

  1. Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)`, `y : Any`, `y∈S` |-? `y∈T`
  2. Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)`, `y : Any`, `y∈T` |-? `y∈S`
  3. Γ, `f*:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `∃S, T∈Pow(B).(f*(S) = f*(T) ∧ S ≠ T)`

1番目と2番目はほとんど同じ形をしているので、どっちか一方を証明して「同様に」でいいと思います。3番目は、結論(ターゲット)が存在命題なので、当該条件を満たすS, Tを実際に構成する問題になります。

これら3つの証明要求は、もとの証明要求に比べれば、だいぶ取り扱いやすくなっています。やりやすい状況まで質問や問題設定(つまり証明要求)を書き換えることが、今回“お膳立て”と呼んだ作業です。お膳立ては済んだので、3つの証明要求に応える、つまり実際の証明を行ってみてください。

*1:分解と変形を区別して使っていますが、「分解」を"resolve"の訳語とするなら、すべて分解と呼んでしまってもいいかも知れません。