数学は楽しい楽しい記号ゲーム JavaScriptで実装した形式化数学で遊んでみよう1

おはにゃあ(๑ŏ _ ŏ๑)

最近女装を始めたオカマプログラマーのゆみなです。ゆみにゃんって呼んでね～♥♥♥

Twitterは[@pizyumi](https://twitter.com/pizyumi)です！オカマの自撮りを見たい方は是非いらしてくださいね～！SNOW加工も無加工もあるよ！

---

この連載記事では**形式化数学をJavaScriptで実装して遊んでみたい**と思います。

**形式化数学**というのは聞き慣れない言葉かもしれませんが、要は**形式化された数学**のことです。

形式化された数学では数、多項式、集合など数学で登場する全てのもの（数学的物件）が形式的に定義されています。

数学的物件は全て記号列や（特にプログラムで数学的物件を取り扱う場合には）木構造として表されます。

そのような記号列や木構造の中で特定の特徴を有するものがその特徴によって数になったり、多項式になったり、集合になったりする訳です。

全ての数学的物件は曖昧さの全くない形で形式的に定義されるためそこに曖昧さはありません。ある数学的物件が別の数学的物件と混同されるということはありません。

このような考え方で、**形式的な数学的物件を作り出すことはできそう**です。

しかし、**数学を行うのに必要なのは数学的物件だけではありません**。

数学的物件に対して論理的な論考を行うのが数学というものです。

ですから、**論理が必要**です。

そして、形式化数学においては論理も曖昧さの全くない形で形式的に定義されている必要があります。

もし論理が曖昧さの全くない形で形式的に定義されていなかったとしたら、論考において曖昧さが混入する可能性があるということになり、数学的物件を曖昧さの全くない形で形式的に定義した意味がなくなってしまいます。

という訳で、**形式化数学で遊ぶにはまず形式的な論理体系が必要**ということになります。

そこで、**今回から数回に亘って形式的な論理体系をJavaScriptで実装することを目指したい**と思います。

なお、形式化数学については過去に[形式化数学入門1](https://qiita.com/pizyumi/items/24e5ba843133059fd74a)という記事も書いたことがありますので参考にしてください。

### どんな論理体系を作ろうか？

取り敢えず**単純な論理体系を作って、それを徐々に拡張していきたい**と思います。

では、その単純な論理体系って何がいい？ということですが、**否定と含意から成る命題論理**になるかと思います。

一応この記事は命題論理のような数学でよく使われる論理については既に知っていることを前提としたいのですが、ある程度は説明しておきましょう。

まず、数学とは数学的物件に対して論考を行う学問ですが、その結果は**定理**という形で現れます。

定理というのは最初は**予想**として誰かによって提起されます。そして、その予想が解かれたら、つまり、その予想が確かに成り立つという論考を示すことができたら、その予想は定理に変わります。

そして、その時の論考のことを**証明**と言います。

最近だと弱abc予想が解かれて定理に変わりましたね。

さて、予想や定理というのは数学的物件に対して何らかのことを**主張**する形になっています。

そして、**主張は正しいか正しくないかのどちらか**です。

予想が解かれたとは予想の主張が正しいことが証明されたということです（稀に予想の反例が見付かった場合も解かれたと言われることがありますが。ちなみに、主張が正しいか正しくないかということと主張が正しいか正しくないかということを証明できるかということは別問題なので注意してください）。

数学では主張は正しいか正しくないかのどちらかしかないので、**数学において用いる論理では主張に関しては正しいか正しくないかだけが取り扱えれば十分**です。

さて、次に、数学において良くある論考の形とはどのようなものでしょうか？

たとえば、

* `A` ならば `B`
* `B` ならば `C`
* よって、`A` ならば `C`

とか、

* `A` ならば `B`
* `A` ならば 「`B` でない」
* よって、「`A` でない」

みたいなものかと思います。

ここで、具体的な論考において**`A`や`B`や`C`に入るのは正しいか正しくないかどちらかの主張**だということは分かるかと思います。

しかし、もう1つ重要なのは「ならば」や「でない」というものの存在です。

これらの言葉は2つの主張を繋ぎ合わせて1つの大きな主張にしたり、1つの主張を修飾して別の主張に変えたりしています。

このような言葉のことを**論理結合子**と言います。そして、「ならば」は**含意**と呼ばれ、「でない」は**否定**と呼ばれます。

**数学における全ての主張はそれ以上分解できない最小の主張と論理結合子から構成されます**。

そして、上で書いた**「否定と含意から成る命題論理」というのはそれ以上分解できない最小の主張と論理結合子として否定と含意がある論理**のことです。

ということで、**まずは最小の主張と否定と含意の論理結合子を使って色々な主張を作る機能を実装しましょう**。

### 最小の主張

最小の主張というのは上の箇条書きの`A`や`B`や`C`のことです。

実際に数学を実践する際には`A`や`B`や`C`の中身は何らかの数学的物件に対する何らかの主張になるはずですが、**今は論理を作る段階なので、`A`や`B`や`C`の具体的な中身がどうなるかは気にする必要がありません**。

そして、**JavaScript上では主張はオブジェクトという形で表す**ことにしましょう。

最小の主張をオブジェクトとして表すには

* **オブジェクトが最小の主張であることが分かる**
* **異なる最小の主張が識別できる**

ことができれば良いですね。

ということで、最小の主張を作る関数`create_proposition`を実装してみます。

```js
function create_proposition (index) {
	return {
		type: 'prop', 
		subtype: 'atom', 
		index: index
	};
}
```

ここでやっているのは`type`、`subtype`、`index`という3つのプロパティを有するオブジェクトを返すということだけです。

`type`プロパティは**オブジェクトの種類**を表すものですが、`prop`としています。今後**`prop`という値は主張を表す**ものとします。

`subtype`プロパティは**オブジェクトの更に細かい種類**を表すものです。**この値を`atom`とすることでオブジェクトが最小の主張であることを表す**ことにします。

`index`プロパティは要は**識別子**です。異なる最小の主張が区別できるようにするために番号を振ります。その番号は関数の第1引数として受け取ることにします。

これで最小の主張を作る関数が出来上がりました。

早速使ってみましょう。

### 最小の主張を適当に作ってみる

最小の主張を適当に作ってみます。

```js
var p1 = create_proposition(1);
var p2 = create_proposition(2);
var p3 = create_proposition(3);
var p4 = create_proposition(4);

console.log(p1);
console.log(p2);
console.log(p3);
console.log(p4);
```

結果は下のようになります。

```js
C:\work2017\project\fm>node mobject.js
{ type: 'prop', subtype: 'atom', index: 1 }
{ type: 'prop', subtype: 'atom', index: 2 }
{ type: 'prop', subtype: 'atom', index: 3 }
{ type: 'prop', subtype: 'atom', index: 4 }
```

特にコメントすることもない当たり前の結果ですね。

ちょっと見栄えが悪いので、オブジェクトを文字列に変換する関数`tostring`を作りましょう。

```js
function tostring (obj) {
	if (obj.type === 'prop') {
		if (obj.subtype === 'atom') {
			return 'P' + obj.index;
		}
		else {
			throw new Error('not supported subtype.');
		}
	}
	else {
		throw new Error('not supported type.');
	}
}
```

**最小の主張は`P`に番号（`index`プロパティ）を付加したような形で表現する**ことにします。

この関数を使って

```js
console.log(tostring(p1));
console.log(tostring(p2));
console.log(tostring(p3));
console.log(tostring(p4));
```

とすると、結果は下のようになります。

```
P1
P2
P3
P4
```

それでは次に、コマンドプロンプトからコマンドを入力して自由に最小の主張を作れるようなプログラムを作ってみましょう。

### 最小の主張を自由に作ってみる

下のような感じのプログラムを書くだけです。

```js
var readline = require('readline');
var colors = require('colors');

var rl = readline.createInterface({
    input: process.stdin,
    output: process.stdout
});

function read_command(context) {
    rl.question('', function (command) {
        if (process_command(context, command)) {
            read_command(context);
        }
        else {
            rl.close();
        }
    });
}

function process_command (context, command) {
    var cs = command.split(' ');

    if (cs[0] === 'prop') {
        context.pindex++;

        var p = create_proposition(context.pindex);

        context.sindex++;

        console.log(context.sindex + ': ' + tostring(p).yellow.bold);

        return true;
    }
    else if (cs[0] === 'exit') {
        return false;
    }
    else {
        return true;
    }
}

var context = {
    pindex: 0, 
    sindex: 0
};

read_command(context);
```

プログラムを実行し、**`prop`というコマンドを実行すると新しい最小の主張を作り出し、その主張をコマンドプロンプトに出力します**。

**出力には通し番号を付けるようにしました**。

また、`exit`コマンドを実行するとプログラムを終了します。

実行例は下のようになります。

```
C:\work2017\project\fm>node fm.js
prop
1: P1
prop
2: P2
prop
3: P3
exit
```

### 次は否定

次は「`A`でない」というような主張、つまり、主張を否定した主張を作れるようにしましょう。

否定の主張を作る関数は`create_negation`関数とします。

また、否定の主張は何らかの主張を材料として作られる主張です。

ですから、この関数は**引数として任意の主張を1つ受け取る**ようにしなければなりません。

また、否定の主張をオブジェクトとして表すには

* **オブジェクトが否定の主張であることが分かる**

必要がありますし、

* **否定の主張を作る材料となった主張はオブジェクトのプロパティとしてアクセスできるべき**

です。

ということで、`create_negation`関数を実装してみます。

```js
function create_negation (p) {
	if (p.type !== 'prop') {
		throw new Error('not prop.');
	}

	return {
		type: 'prop', 
		subtype: 'neg', 
		sub: p
	};
}
```

たったこれだけです。

`create_negation`関数は**第1引数として否定の主張を作る材料となる任意の主張を受け取る**ことにします。引数として変なものを受け取ったら例外を投げます。

そして、返り値のオブジェクトは3つのプロパティを有します。

`type`プロパティはオブジェクトの種類を表すものですが、この値は主張を表す`prop`としています。上の`create_proposition`関数の場合と同じです。

`subtype`プロパティはオブジェクトの更に細かい種類を表すものですが、**この値を`neg`とすることでオブジェクトが否定の主張であることを表す**ことにします。

`sub`プロパティは**否定の主張を作る材料となった主張**を表すことにします。

### 次は含意

次は「`A`ならば`B`」というような主張、つまり、含意と呼ばれる主張を作れるようにしましょう。

含意の主張を作る関数は`create_implication`関数とします。

また、含意の主張は2つの何らかの主張を材料として作られる主張です。

ですから、この関数は**引数として任意の主張を2つ受け取る**ようにしなければなりません。

また、含意の主張をオブジェクトとして表すには

* **オブジェクトが含意の主張であることが分かる**

必要がありますし、

* **含意の主張を作る材料となった2つの主張はそれぞれがオブジェクトのプロパティとしてアクセスできるべき**

です。

ということで、`create_implication`関数を実装してみます。

```js
function create_implication (p1, p2) {
	if (p1.type !== 'prop') {
		throw new Error('not prop.');
	}
	if (p2.type !== 'prop') {
		throw new Error('not prop.');
	}

	return {
		type: 'prop', 
		subtype: 'imp', 
		sub1: p1, 
		sub2: p2
	};
}
```

たったこれだけです。

`create_implication`関数は**第1引数と第2引数として含意の主張を作る材料となる任意の主張を受け取る**ことにします。**第1引数の主張が「ならば」の前に来る主張（前件と言います）を表す**ものとし、**第2引数の主張が「ならば」の後に来る主張（後件と言います）を表す**ものとします。引数として変なものを受け取ったら例外を投げます。

そして、返り値のオブジェクトは4つのプロパティを有します。

`type`プロパティはオブジェクトの種類を表すものですが、この値は主張を表す`prop`としています。上の`create_proposition`関数や`create_negation`関数の場合と同じです。

`subtype`プロパティはオブジェクトの更に細かい種類を表すものですが、**この値を`imp`とすることでオブジェクトが含意の主張であることを表す**ことにします。

`sub1`プロパティと`sub2`プロパティは**含意の主張を作る材料となった主張**を表すことにします。`sub1`プロパティが**前件**を表し、`sub2`プロパティが**後件**を表すものとします。

### tostring関数の改良

`tostring`関数を否定や含意の主張を表すオブジェクトにも対応させましょう。

```js
function tostring (obj) {
	if (obj.type === 'prop') {
		if (obj.subtype === 'atom') {
			return 'P' + obj.index;
		}
		else if (obj.subtype === 'neg') {
			return '( ' + '~' + tostring(obj.sub) + ' )';
		}
		else if (obj.subtype === 'imp') {
			return '( ' + tostring(obj.sub1) + ' -> ' + tostring(obj.sub2) + ' )';
		}
		else {
			throw new Error('not supported subtype.');
		}
	}
	else {
		throw new Error('not supported type.');
	}
}
```

**否定の主張は材料となった主張の頭に`~`を付けることで表す**ことにします。

**含意の主張は材料となった2つの主張を前件、後件の順番で`->`で繋げることによって表す**ことにします。

また、スコープが分かるように前後を`(`と`)`で囲みます。

### CLIの改良

CLIを否定や含意の主張にも対応させましょう。

変更が必要なのは`process_command`関数と`context`オブジェクトのみです。

まず`context`オブジェクトには`smap`というプロパティを追加することにします。

```js
var context = {
	pindex: 0, 
	sindex: 0, 
	smap: new Map()
};
```

このプロパティの値はマップとし、プログラムの実行中に作成された全てのオブジェクトを格納するものとします。

このマップのキーは通し番号（`sindex`プロパティ）とすることにします。

そして、`process_command`関数は下のようになります。

ちょっと長いですが、注意深く読めば理解できるかと思います。

**否定の主張を作る`neg`コマンドと含意の主張を作る`imp`コマンドが追加されており、`neg`コマンドは1つの引数を取り、`imp`コマンドは2つの引数を取ります**。

**それぞれの引数は新しく作られる主張の材料となる主張の通し番号です**。

```js
function process_command (context, command) {
	var cs = command.split(' ');

	if (cs[0] === 'prop') {
        context.pindex++;

        var p = create_proposition(context.pindex);

        add_object(context, p);

        return true;
	}
	else if (cs[0] === 'neg') {
		var objs = get_n_objects_from_args(context, 1, cs);
		if (objs == null) {
			return true;
		}
		var p = create_negation(objs[0]);

		add_object(context, p);

		return true;
	}
	else if (cs[0] === 'imp') {
		var objs = get_n_objects_from_args(context, 2, cs);
		if (objs == null) {
			return true;
		}
		var p = create_implication(objs[0], objs[1]);

		add_object(context, p);

		return true;
	}
	else if (cs[0] === 'exit') {
		return false;
	}
	else {
		return true;
	}
}

function get_n_objects_from_args (context, n, cs) {
	if (!check_num_arguments(cs, n)) {
		return null;
	}

	var objs = [];
	for (var i = 0; i < n; i++) {
		var idx = get_int_argument(cs[1 + i]);
		if (idx === null) {
			return null;
		}

		if (!check_in_range(idx, context.sindex)) {
			return null;
		}

		var obj = context.smap.get(idx);

		objs.push(obj);
	}

	return objs;
}

function add_object (context, obj) {
	context.sindex++;
	context.smap.set(context.sindex, obj);

	console.log(context.sindex + ': ' + tostring(obj).yellow.bold);
}

function check_num_arguments (cs, num) {
	if (cs.length < num + 1) {
		console.error('missing argument.'.red.bold);

		return false;
	}
	else {
		return true;
	}
}

function get_int_argument (arg) {
	var int = parseInt(arg);
	if (isNaN(int)) {
		console.error('not integer.'.red.bold);

		return null;
	}
	else {
		return int;
	}
}

function check_in_range (arg, max) {
	if (arg < 1 || arg > max) {
		console.error('out of range.'.red.bold);

		return false;
	}
	else {
		return true;
	}
}
```

実行例は下のようになります。

```
C:\work2017\project\fm>node fm.js
prop
1: P1
prop
2: P2
prop
3: P3
neg 1
4: ( ~P1 )
neg 3
5: ( ~P3 )
imp 1 2
6: ( P1 -> P2 )
imp 2 3
7: ( P2 -> P3 )
imp 3 1
8: ( P3 -> P1 )
imp 6 7
9: ( ( P1 -> P2 ) -> ( P2 -> P3 ) )
exit
```

このように、否定や含意の主張は先に作っておいた主張を材料にして作成します。

これにより適切なコマンドを入力して様々な主張を作り出すことができるようになりました。

### 今回はここまで

今回はここまでとしたいと思います。

次回は主張を基にして証明を作る方法について考えたいと思います。