おはにゃあ(๑ŏ _ ŏ๑)
最近女装を始めたオカマプログラマーのゆみなです。ゆみにゃんって呼んでね～♥♥♥
Twitterは@pizyumiです！オカマの自撮りを見たい方は是非いらしてくださいね～！SNOW加工も無加工もあるよ！
この連載記事では形式化数学をJavaScriptで実装して遊んでみたいと思います。
形式化数学というのは聞き慣れない言葉かもしれませんが、要は形式化された数学のことです。
形式化された数学では数、多項式、集合など数学で登場する全てのもの（数学的物件）が形式的に定義されています。
数学的物件は全て記号列や（特にプログラムで数学的物件を取り扱う場合には）木構造として表されます。
そのような記号列や木構造の中で特定の特徴を有するものがその特徴によって数になったり、多項式になったり、集合になったりする訳です。
全ての数学的物件は曖昧さの全くない形で形式的に定義されるためそこに曖昧さはありません。ある数学的物件が別の数学的物件と混同されるということはありません。
このような考え方で、形式的な数学的物件を作り出すことはできそうです。
しかし、数学を行うのに必要なのは数学的物件だけではありません。
数学的物件に対して論理的な論考を行うのが数学というものです。
ですから、論理が必要です。
そして、形式化数学においては論理も曖昧さの全くない形で形式的に定義されている必要があります。
もし論理が曖昧さの全くない形で形式的に定義されていなかったとしたら、論考において曖昧さが混入する可能性があるということになり、数学的物件を曖昧さの全くない形で形式的に定義した意味がなくなってしまいます。
という訳で、形式化数学で遊ぶにはまず形式的な論理体系が必要ということになります。
そこで、今回から数回に亘って形式的な論理体系をJavaScriptで実装することを目指したいと思います。
なお、形式化数学については過去に形式化数学入門1という記事も書いたことがありますので参考にしてください。
どんな論理体系を作ろうか？
取り敢えず単純な論理体系を作って、それを徐々に拡張していきたいと思います。
では、その単純な論理体系って何がいい？ということですが、否定と含意から成る命題論理になるかと思います。
一応この記事は命題論理のような数学でよく使われる論理については既に知っていることを前提としたいのですが、ある程度は説明しておきましょう。
まず、数学とは数学的物件に対して論考を行う学問ですが、その結果は定理という形で現れます。
定理というのは最初は予想として誰かによって提起されます。そして、その予想が解かれたら、つまり、その予想が確かに成り立つという論考を示すことができたら、その予想は定理に変わります。
そして、その時の論考のことを証明と言います。
最近だと弱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を実装してみます。
function create_proposition (index) {
return {
type: 'prop',
subtype: 'atom',
index: index
};
}
ここでやっているのはtype、subtype、indexという3つのプロパティを有するオブジェクトを返すということだけです。
typeプロパティはオブジェクトの種類を表すものですが、propとしています。今後**propという値は主張を表す**ものとします。
subtypeプロパティはオブジェクトの更に細かい種類を表すものです。この値をatomとすることでオブジェクトが最小の主張であることを表すことにします。
indexプロパティは要は識別子です。異なる最小の主張が区別できるようにするために番号を振ります。その番号は関数の第1引数として受け取ることにします。
これで最小の主張を作る関数が出来上がりました。
早速使ってみましょう。
最小の主張を適当に作ってみる
最小の主張を適当に作ってみます。
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);
結果は下のようになります。
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を作りましょう。
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プロパティ）を付加したような形で表現することにします。
この関数を使って
console.log(tostring(p1));
console.log(tostring(p2));
console.log(tostring(p3));
console.log(tostring(p4));
とすると、結果は下のようになります。
P1
P2
P3
P4
それでは次に、コマンドプロンプトからコマンドを入力して自由に最小の主張を作れるようなプログラムを作ってみましょう。
最小の主張を自由に作ってみる
下のような感じのプログラムを書くだけです。
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関数を実装してみます。
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関数を実装してみます。
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関数を否定や含意の主張を表すオブジェクトにも対応させましょう。
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というプロパティを追加することにします。
var context = {
pindex: 0,
sindex: 0,
smap: new Map()
};
このプロパティの値はマップとし、プログラムの実行中に作成された全てのオブジェクトを格納するものとします。
このマップのキーは通し番号（sindexプロパティ）とすることにします。
そして、process_command関数は下のようになります。
ちょっと長いですが、注意深く読めば理解できるかと思います。
否定の主張を作るnegコマンドと含意の主張を作るimpコマンドが追加されており、negコマンドは1つの引数を取り、impコマンドは2つの引数を取ります。
それぞれの引数は新しく作られる主張の材料となる主張の通し番号です。
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
このように、否定や含意の主張は先に作っておいた主張を材料にして作成します。
これにより適切なコマンドを入力して様々な主張を作り出すことができるようになりました。
今回はここまで
今回はここまでとしたいと思います。
次回は主張を基にして証明を作る方法について考えたいと思います。