【自由研究】数学DB設計-001～記号～

PK_RNX_ずんだもん博士(数物系)

みなさんこんにちは、ずんだもん博士なのだ。みなさんは、記号はありますか？たとえ小さな記号でも、いつかそれが…ってそりゃ電脳チャイナパトロールの「希望」回だろがい！！！！！！！！！

どうも、バーグハンバーグバーグ加藤亮さん大好(だいハオ)倶楽部です。ということでね、今回は記号を定義していきますけども、数学ではいろんな記号がありますね。日ごろよく使うのは

$$
\begin{align*}
0, 1, \pi, e, x, +, -, \times, \land, \forall, \exists,\text{ etc…}
\end{align*}
$$

などでしょうな。今回はこれらを分類して、テーブル化できる形までもっていこうと思います！数学DB設計000もみてね・・・！

今回のサンプルコードは以下になります：

そのほか、Const.csの「SymbolTypeEnum」「FormulaTypeEnum」も見てみてね。


定義

まずはガチッと定義を述べて、それに注釈をつけていく形でやっていきましょう。

記号

記号とは、以下の属性で定義される、ひとかたまりのデータである：

  • ID (データベースでの識別用)

  • 記号名称 (テキスト)

  • 記号種類 (後述の記号種類に紐づくカラム)

  • 引数の個数 (0以上の整数値)

  • 引数にとれる論理式の種類 (後述の)

  • 備考(テキスト。その記号の意味などを書いておく)

記号種類

記号種類とは、以下の属性で定義される、ひとかたまりのデータである：

  • ID (データベースでの識別用)

  • 記号種類名称 (テキスト)

  • 論理式種類 (後述の論理式種類に紐づくカラム)

  • 量化記号かどうか(true/false)

論理式種類

論理式種類とは、以下の属性で定義される、ひとかたまりのデータである：

  • ID (データベースでの識別用)

  • 論理式種類名称 (テキスト)

RDBの説明

もしかしたらデータベース触ったことないよっていう人もいるかもしれないので、要らんかもしれんけど、(リレーショナル)データベースの説明をまずしていこうと思います。

リレーショナルデータベース(以下RDB)は、基本的には「テーブル」と呼ばれるものの集まりです。テーブルは、みなさんExcel触ったことあるかもしれませんが、基本的に見た目はアレっぽいの認識でOKです。実際、DB設計なんぞするときはExcelを使うことが多いです。

例えば「論理式種類テーブル」を作りたいぜっていうときは、以下のような見た目になると思います：

論理式種類テーブルの設計

テーブルとカラムについて

テーブルというのは、いくつかのカラムが設定されていて、カラムひとつずつに数値やテキストなどのデータを入れて、一行のデータ(レコード)として溜め込むことができるようにしたものです。カラムに付与できる重要な概念は沢山あるのですが、とありあえず以下を押さえておけば大丈夫かなと思います：

  • カラムの値の型 (数値系(number, decimal, float等)、テキスト系(VARCHAR, TEXT等)、boolean系などなど…)

  • プライマリーキー (Primary Key)

  • 外部キー

「カラムの値の型」は問題ないでしょう。そのカラムに設定できる値を設定します。最近のDBはすごくて、画像や動画などもバイナリデータとして持っておけるものがあります。まあ、入出力に時間がかかっちゃうから、あんまりやらない方がいいですけどね。

プライマリーキーはそのテーブルに登録されているレコードの中で一意に定めるカラムです。つまり、もしプライマリーキーが重複するデータを登録しようとした場合、エラーではじかれます。これがプライマリーキーの最も重要な機能です。普通はIDという名前の、数値あるいは乱数生成した値を入れるカラムひとつだけが用いられるんですが、別に数値じゃなければいけないルールもなければ、複数のカラムをプライマリーキーに設定できます。例えば「IDと名前」をプライマリーキーに入れたら、IDと名前で一意であればいいので、名前さえ違えばIDは重複しても登録できます。まあ、複数プライマリーキーもあんまりやらないですけどね。

最後に外部キーは、他テーブルに登録されているデータのプライマリーキーと紐づけて、そのレコードが他のテーブルのデータとどのように紐づいているかを定義するものです。例えば

外部キー使用例

記号種類(symbol_type)テーブルの「formula_type_id」が、論理式種類(formula_type)のプライマリーキー「id」に紐づいています。

もしここに「論理式種類」に登録されていないid(3とか4とか)を登録しようとするとエラーになります。これが外部キーの重要な機能です。

僕の数学DB設計は、この外部キーを使い倒して、データ整合性で証明の正しさを保証することです。なんかできそうな気がしてきたでしょ？

ほいじゃ、本題に戻りますぞ。

記号種類

まずどんな種類の記号があるのか、つまり記号種類から解説する必要がありましょう。まずは想定している記号種類を列挙していきましょう：

  • 項型自由変数記号

  • 命題型自由変数記号

  • 束縛変数記号

  • 関数記号

  • 述語記号

  • 論理記号

  • 項型量化記号

  • 命題型量化記号

簡単な順に一つずつ見ていきましょうか。ただ、自由変数は難しいので最後にします。

関数記号

これはこの中では一番簡単な部類ですね。「$${+,-,/,\times}$$」などです。「項」というのはあとで定義するんですが、ザックリ言えば数学的な実体です。0とか1などの数字もあれば、円周$${S^1}$$、ベクトル空間$${\mathcal{H}=\{\psi:\mathbb{R}^4\rightarrow\mathbb{C}\mid\text{シュレーディンガー方程式}\}}$$なども項です。

関数記号というのは、そういう「項」を引数にとって、新たに「項」をつくる記号です。まあ、イメージはつかめましたかね？

重要なのは引数の個数です。引数の個数が1以上の関数記号はイメージしやすいと思いますが、引数の個数が0の関数記号も許容します。それは例えば$${0,1,2,\dots}$$や、$${\emptyset}$$とかもそうです。引数の個数が0の関数記号を定数記号と呼ぶ教科書もあります。僕も時々「定数記号」って言ってしまうことがあるかもしれませんが、システム内では引数の個数が0の関数記号の別名です。別名カラムを作った方がいいかな？

論理記号

$${\lor,\land,\neg,\Rightarrow}$$などです。「命題」っていうのも次回以降で定義するんですが、論理記号はいくつかの命題を引数にとって、新しい命題を作る記号です。

例えば$${P,Q}$$っていう二つの命題があったとき、$${P\land Q}$$っていうのは新しい命題です。ポーランド記法では$${\land PQ}$$って書きます。前回申し上げた通り、僕のデータベースではポーランド記法を採用します。

これにも引数の個数が0の論理記号もあります。たとえば「矛盾」を意味する$${\bot}$$です。まあ、これは次に説明する、引数の個数が0の述語記号とシステム上区別が付かないです。なので、どっちにするべきかは気分です。どっちかというと「矛盾である」っていうのは述語っぽく感じるので、もしかしたら$${\bot}$$は述語記号のほうがいいかもしれないです。

述語記号

述語記号は、いくつかの項を引数にとって、新しい命題を作る記号です。これは僕は相当使い倒すつもりです。たとえば

$$
\begin{align*}
{\rm IsSet},\;{\rm IsGroup},\;{\rm IsTopologicalSpace}
\end{align*}
$$

なんかを用意するつもりです。つまり、たとえば

$$
\begin{align*}
{\rm IsTopologicalSpace}\;X
\end{align*}
$$

などと書けば、「$${X}$$は位相空間です」と言ってることになります。これはよく定理の仮定に使う予定で、

Let $${X}$$ be a topological space

の代わりに使うつもりなのです。

命題型量化記号

$${\forall, \exists, \exists!}$$などです。わかりますね。

$$
\begin{align*}
\forall xP(x)
\end{align*}
$$

と書けば、任意の変数$${x}$$に対して$${P(x)}$$が成り立つと言っています。これは普段よく使っているでしょう。$${\epsilon\text{-}\delta}$$論法を知っていれば、それをイメージしてくれればいいです。

ただし重要なのは、この後説明する束縛変数との兼ね合いで、文字列$${\forall xP(x)}$$の中から自由変数$${x}$$は消滅させます。このことによって、数学基礎論最大の壁である「代入」という操作を少し楽にするつもりなのです。

項型量化記号

これは今のところ1種類しか想定していないです。つまり、前にも紹介した$${\{\mid\}}$$です。機能としては、一つの命題と、その中に含まれる一つの項型自由変数を束縛して新しい項を得るための記号です。例えば

$$
\begin{align*}
\{x\mid P(x)\}
\end{align*}
$$

というのは、$${x}$$を項型自由変数にもつ命題から、「集合」という数学的な実体(つまり項)を得る記号になります。こちらも次に説明する「束縛変数」によって、自由変数$${x}$$を消滅させます。

束縛変数

ブルバキ、あるいは今は亡き「数理科学のページ」に倣って、このシステムに許容する束縛変数の個数は1つのみとします。束縛変数というのは、さっき開設した「量化記号」が束縛する変数です。

つまり、普通の書き方をした時の、例えば$${\forall xP(x)}$$のような論理式の、$${x}$$のことです。これを、たった一つの記号$${\Box}$$であらわします。

ではその束縛変数の識別はどうやるのかというと、その変数を束縛している量化記号と、その束縛されている変数とを文字通り線で結んで表します。例えば

これは、ポーランド記法もほぐしてやって、普通に書けば

$$
\begin{align*}
\forall x [P(x)\lor Q(x)]\Rightarrow[[\forall y[P(y)]]\lor[\forall z[Q(z)]]]
\end{align*}
$$

という意味になります。

この記法はとても便利で、代入という操作に対して自由変数に関する束縛がかなり楽になります。例えば

$$
\begin{align*}
\forall x P(x,y)
\end{align*}
$$

という論理式の中に、$${y=T(x)}$$という項がぶち込まれることを考えてみてください：

$$
\begin{align*}
\forall x P(x,T(x))
\end{align*}
$$

本来$${y=T(x)}$$という項の代入に際して、$${\forall xP(x,y)}$$という命題で$${x}$$は再束縛されるべきでしょうか？いや、そうではありません。このような困難を、ブルバキ、あるいは今は亡き「数理科学のページ」では「束縛変数$${\Box}$$」および「量化記号と束縛変数を繋ぐ鎖」という概念を導入することによって解決しています。最初は受け入れるのが難しいと思いますが、いくつか計算してみると、なかなか効率がいいなーって感じると思います。

項型自由変数記号

自由変数記号は、$${x}$$とか$${y}$$とか、そういう方程式に使われる記号をイメージしてもらえれば大体あってます。ただ実数や複素数じゃなくて、これは行列かもしれないですし、位相空間かもしれないですし、集合かもしれないですし、集合の上位存在であるクラスかもしれません。本当に何を代入してもいいものです。

僕の数学基礎で一番頑張ろうとしているのは、実はここに「命題型の」自由変数を認めようというものです。理由を説明しましょう。

命題型自由変数

命題型の自由変数を認めないと言いつつ、命題を好きに代入して使う「命題もどき」を次の瞬間に使われる基礎論の教科書、多いです。例えば二重否定除去法則

$$
\begin{align*}
\neg\neg\varphi\iff\varphi
\end{align*}
$$

はいつも正しい、と仮定することがありますが、ここに含まれている記号$${\varphi}$$は明らかに「命題を代入する自由変数」ですよね。

もしこれを自由変数と認めない場合、取れる対応は一つしかありません。例えば二重否定除去法則なら、これを推論規則と考えるということです。つまり二重否定除去法則を、単なる命題ではなく、「$${\neg\neg\varphi}$$という形の命題から$${\varphi}$$という結論を導いても良い」という推論だと考えるのです。

これは一つの考え方としておそらく合っていて、僕も最初はその方針でコーディングを進めていました。ところがこの試みはプログラミングとしては、だんだん、だんだん難しくなっていきました。

まずこのタイプの推論規則は、他の推論規則から導かれるものがあります。例えば二重否定除去法則から、排中律を導くことができます。排中律から、背理法の基本原理を導くことができます。そうやって、推論規則から推論規則を導くことができるという状況が生まれます。なので、どこかの推論規則を基準において、別の推論規則を導くという「定理のような推論規則」を考える必要が発生しました。

これだけならまだよかったのですが、こうした「定理のような推論規則を別の定理の証明に適用する」というようなことを考えるとき、この「定理のような推論規則」と、例えば準同型定理のような「普通の定理」とを区別して扱う必要が出てきます。普通の定理は(項型)自由変数への代入で定理の適用とみなしうりますが、「定理のような推論規則」は「推論規則の適用」という、似たようで全く違うことをしないといけなくなります。これはコーディングに相当の負荷を感じました。

そもそも、「推論規則の適用」という行為自体が結構複雑です。また後日述べるのですが、推論規則には「どの変数にどの命題・項を適用し、どの未解消の仮定を打ち消すのか、あるいは追加するのか？また、代入に際して束縛されている自由変数が重複していないか？」などというバリデーションが必要になってきます。そういうとき、「定理の適用」が推論規則になってしまうと、例えば「その推論規則的な定理の何を命題型変数と思うべきなのか？」まで入力者が気にする必要があり、結果的にコーディングが絶望的に難しくなります (なった結果が1年以上のほったらかしにつながっています)。

じゃあいっそ、最初から命題型自由変数を認めて、定理の適用は「代入」という操作に一任させるだけにしたい、と、今はそう思っています。僕がこの記事を書いているということは、本気でそう思い始めたということです。

ただ前回気づいたように、命題型自由変数には項型自由変数を引数にもつことがあります。例えば

$$
\begin{align*}
{}^\forall X\;{}^\exists A\;{}^\forall x\;[x\in A\leftrightarrow [x\in A\land\psi(x)]]
\end{align*}
$$

とかね。ここの$${\psi(x)}$$に具体的な論理式を代入するときは、結構大変なことになりそう。まあ、その責任は「代入」に一任させましょうかね。

プログラミングの格言

今思い出したので有益情報として、プログラミングの格言を紹介しましょう。

単一責任の原則

クラスには持たせる責任は一つにすべし、という内容の、オブジェクト指向プログラミングにおける格言です。実際に業務でプログラミングしてると、一つのクラスにあれもこれも機能をぶち込んじゃうことがあります。「StorageInquiry(在庫照会)」ってクラスなのに、在庫の調整機能を付けちゃったりね。こういうのは大抵、保守性を極めて損なう危険な行為です。一つのクラスが万行単位になったりします。こんなん、初見で見た人は卒倒します。プログラムは、誰が見てもすぐにわかるように書きましょう。

さっきの在庫照会に在庫調整機能を付けちゃう例でいうと、もう「在庫調整」っていうクラスを新しく作って、在庫照会から「在庫調整」っていうモーダルを表示させる方がいいです。UI/UXとしても、そっちの方が間違えにくいでしょうしね。顧客が文句言ってきたら「じゃあ保守費用上げます」でお互いバチバチしましょう。

デメテルの法則

オブジェクト指向プログラミングでは、クラスが生成する「インスタンス」がユーザーの操作によってグニグニ変わっていきます。インスタンスの状態は、例えば

stock.name

みたいに書いて、今扱ってる stock インスタンスの名前(name)を得ます。でも例えば、その在庫の仕入れ時の、運送費用なんかを参照したいとき

stock.purchase.transportation.cost

みたいに、参照が連なることがあります。これはこれでいいとは思うんですが、「在庫の運送費をよく参照したい」っていう場合はあまり望ましくないです。もし後で「売上入力でも運送費を参照したいですー」って言われたとき、製造担当じゃなかった人がコーディングを担当するとき、どうすればいいでしょう？IDEが発達した今でさえ、上記のコードに行きつくのは至難です。こうなると保守担当者はもしかすると、新たに「在庫インスタンスから運送費を取得するSQL」を書いてしまいかねません。それは無駄です。

これを戒めるのが「デメテルの法則」です。僕も今回、記号種類に「量化記号かどうか」を持たせましたが、「記号」単体も「量化記号かどうか」が知りたいです。でも「量化記号かどうか」というデータが宿るべきテーブルは「記号種類」であるべきだと思っています。そういうとき、コーディング上ではgetのみのプロパティを用意することがあります。例えばSymbol.csには

public bool IsQuantifier
{
  get => Type?.IsQuantifier ?? throw new ArgumentException("Include SymbolType");
}

というコードを書かせてもらってます。こうすることで、あとで誰が見ても「お、Symbolが量化記号かどうかが分かるプロパティあるじゃん！」となって、保守効率が上がるというわけです。


いいなと思ったら応援しよう！