math.pl

/*
このプログラムはswi-prologで実行することができます。
swiproogのインストールは以下のようにしてインストールできます:
$ brew install swi-prolog
$ apt install swi-prolog
このプログラムを実行するには以下のようにコマンドラインから実行します:
$ swipl math.pl

現代数学は一階述語論理を道具としてペアノ数などを定義していくことで構築されています。
http://www.f.waseda.jp/moriya/PUBLIC_HTML/social/natural_numbers.pdf
Prologは一階述語論理を深さ優先探索で自動証明するプログラミング言語です。
Prologを用いればペアノ数を素直に定義して用いることができます。
人によってはペアノ数なんてなんでそんなめんどくさい数を定義しても実用的ではないから意味がないのではないかと考えるかもしれません。
確かにスピード的には速くありません。しかし、神やコンピュータと言った存在なしに論理だけがある世界に自然数の計算が定義できることを理解することは重要です。
Prologによる一階述語論理を用いた動く数学の定義を作る実験は論理さえあれば数学が定義できることを理解する上で有用なのです。
より実用的なコンピューターは２真数を用いた論理回路によって構築され様々な最適化が行われているためより高速に動作します。
その最も基本的な考え方がペアノ数を用いた数の定義なのです。
*/

/*
数値は一切使えない状況で数値を認識するには、0から9までの文字のみで構成された Prolg の atom を数値として認識できれば良いでしょう。
そのためには atom を 1文字のリストに変換する述語 atom_chars/2 があればこの述語を用いて様々な述語を定義できます。
そこでまず、組込み述語のatom_charsが使えることを確認します。
*/

% atom_chars/2 は atom (Lispのシンボルのようなもの。文字列の代わりで使ってます) を文字のリストに変換する、またはその逆変換をする述語。
:- atom_chars(abc,[a,b,c]).
% atom から リスト へのテスト
:- atom_chars('123',R),!,R=['1','2','3'].
% リスト から atom へのテスト
:- atom_chars(R,['1','2','3']),!,R='123'.

/*
atom_chars が使えることを確認できたので、次は数値を表す atom を判定する述語 i/1 を作ります。

member/2 は以下のようなリスト内の1つの値を取り出す述語です:
member(A,[A|_]).
member(A,[_|As]):- member(A,As).

member/2 は非決定的な述語です。
1行目のルールの判定に失敗すれば、2行目のルールを実行し再帰的にmember/2を呼び出します。
このように定義することでリスト内の値をリストの先頭から順番に取り出す非決定的な述語になります。
*/

% i1/1 は atom が '0' から '9'　の文字であることを調べる
i1(I):-member(I,['0','1','2','3','4','5','6','7','8','9']),!.
% i2/1 はリスト内の全ての値が '0' - '9' の文字であることをチェック
i2([]).
i2([A|As]):-i1(A),i2(As).
% i/1 は 数値であるatomかどうかを調べる
i(A):-atom(A),atom_chars(A,As),i2(As).

% i/1 のテスト
:- i('0').
:- i('9').
:- i('10').
:- i('11').
:- not(i(abc)).
:- not(i([abc])).

/*
ペアノ数の構文を決めます。
これはXML SchemaやJSON Schema のように構造的なデータを再帰的に検査する述語を定義することで構文検査ができます。
(Prologの場合は値が束縛されていない変数を設定して呼び出す事で、生成文法としても機能します。もしよかったら実験してみてください。)
*/
% n/1 は ペアノ数であるかどうかを調べる。
n(z).
n(s(N)) :- n(N).

% n/1 をテスト
:- n(z).
:- n(s(z)).
:- n(s(s(z))).
:- n(s(s(s(z)))).
:- not(n(s)).

/*
ペアノ数の四則演算を定義します。
*/
% ペアノ数での足し算の定義
plus(z,N,N).
plus(s(N1),N2,s(N3)):- plus(N1,N2,N3).

% ペアノ数の掛け算
times(z,_,z).
times(s(N1),N2,N4):- times(N1,N2,N3),plus(N2,N3,N4).

% ペアノ数の引き算
minus(N,z,N):-!.
minus(z,_,z):-!.
minus(s(N1),s(N2),N3):- minus(N1,N2,N3).

% ペアノ数の比較
little_equals(_,z).
little_equals(s(N1),s(N2)):- little_equals(N1,N2).

% ペアノ数の割り算
division(_,z,_):- !,fail.
division(N1,N2,s(V)):- little_equals(N1,N2),!,minus(N1,N2,N1_),division(N1_,N2,V).
division(_,_,z).

% ペアノ数の割り算の余り
modulo(_,z,_):- !,fail.
modulo(N1,N2,V):- little_equals(N1,N2),!,minus(N1,N2,N1_),modulo(N1_,N2,V).
modulo(N,_,N).

% 足し算のテスト
:- plus(z,z,z).
:- plus(s(s(z)),s(z),s(s(s(z)))).
:- plus(s(s(z)),s(s(z)),s(s(s(s(z))))).
% 掛け算のテスト
:- times(z,z,z).
:- times(s(s(z)),s(z),s(s(z))).
:- times(s(s(z)),s(s(z)),s(s(s(s(z))))).
% 引き算のテスト
:- minus(s(s(z)),s(s(z)),z).
:- minus(s(s(z)),z,s(s(z))).
:- minus(s(s(z)),s(z),s(z)).
% 割り算のテスト
:- not(division(s(s(z)),z,_)).
:- division(s(s(z)),s(s(z)),s(z)).
:- division(s(s(z)),s(z),s(s(z))).
:- division(s(s(s(s(z)))),s(s(z)),s(s(z))).
% 割り算の余りのテスト
:- not(modulo(s(s(z)),z,_)).
:- modulo(s(s(z)),s(s(z)),z).
:- modulo(s(s(z)),s(z),z).
:- modulo(s(s(s(s(z)))),s(s(z)),z).
:- modulo(s(s(s(s(s(z))))),s(s(z)),s(z)).

/*
ペアノ数を生で扱うのは人間には優しくないので、123と言った表現を使った計算ができるようにします。
ペアノ数s(s(s(0)))を3と相互変換できる述語をまず定義します。
*/

% n2i1 はペアノ数0-9までと1文字のatomの変換を行う述語
n2i1(z,'0').
n2i1(s(z),'1'). 
n2i1(s(s(z)),'2').
n2i1(s(s(s(z))),'3').
n2i1(s(s(s(s(z)))),'4').
n2i1(s(s(s(s(s(z))))),'5').
n2i1(s(s(s(s(s(s(z)))))),'6').
n2i1(s(s(s(s(s(s(s(z))))))),'7').
n2i1(s(s(s(s(s(s(s(s(z)))))))),'8').
n2i1(s(s(s(s(s(s(s(s(s(z))))))))),'9').
% var/1 は未束縛な変数かどうかを検査する述語であるテスト
:- var(_).
:- not(var('123')).
% n2is/2 はペアノ数からアトムのリストに変換する述語
n2is(N,[I]):-n2i1(N,I),!.
n2is(N,[M_|Is]):- var(N),!,n2i1(M,M_),n2is(N1,Is),times(s(s(s(s(s(s(s(s(s(s(z)))))))))),N1,N1_),plus(N1_,M,N).
n2is(N,[M_|Is]):- modulo(N,s(s(s(s(s(s(s(s(s(s(z)))))))))),M),
                 n2i1(M,M_),
                 division(N,s(s(s(s(s(s(s(s(s(s(z)))))))))),V),
                 n2is(V,Is).
% n2i/2 は全てのペアノ数からアトムに変換する述語
n2i(N,I):- var(N),!,atom_chars(I,Is),reverse(Is,Is_),n2is(N,Is_).
n2i(N,I):- n2is(N,Is),reverse(Is,Is_),atom_chars(I,Is_).
% n2i1/2のテスト
:- n2i1(s(s(s(s(s(s(s(s(s(z))))))))),'9').
% n2i/2のテスト
:- n2i(s(s(s(s(s(s(s(s(s(z))))))))),'9').
:- n2i(s(s(s(s(s(s(s(s(s(s(z)))))))))),'10').
:- n2i(R,'29'),!,R=s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(z))))))))))))))))))))))))))))).
:- n2i(R,'10'),!,R=s(s(s(s(s(s(s(s(s(s(z)))))))))).
:- n2i(R,'11'),!,R=s(s(s(s(s(s(s(s(s(s(s(z))))))))))).

/*
自然な表現ができるようになったので、自然な表現での四則演算を定義します。
*/
% atom同士の加算
add(A,B,C):- n2i(A_,A),n2i(B_,B),plus(A_,B_,C_),n2i(C_,C),!.
% atom同士の引き算
sub(A,B,C):- n2i(A_,A),n2i(B_,B),minus(A_,B_,C_),n2i(C_,C),!.
% atom同士の掛け算
mul(A,B,C):- n2i(A_,A),n2i(B_,B),times(A_,B_,C_),n2i(C_,C),!.
% atom同士の割り算
div(A,B,C):- n2i(A_,A),n2i(B_,B),division(A_,B_,C_),n2i(C_,C),!.
% atom同士の割り算の余り
mod(A,B,C):- n2i(A_,A),n2i(B_,B),modulo(A_,B_,C_),n2i(C_,C),!.
% atom同士の比較
le(A,B,true):- n2i(A_,A),n2i(B_,B),little_equals(A_,B_),!.
le(_,_,false).
% 否定
not(true,false).
not(false,true).
% 比較
gt(A,B,R):- le(A,B,R1),not(R1,R).
% アトム同士の演算のテスト
:- add('15','23','38').
:- sub('38','15','23').
:- mul('8','8','64').
:- div('33','2','16').
:- mod('33','2','1').
:- le('13','11',true).

/*
四則演算は定義できましたが1*2+3*4と言ったネストした数式を計算することはまだできません。
そこで1*2+3*4をadd(mul(1,2),mul(3,4))のような表現を使った数式で計算できるようにします。
*/

% 数式の大ステップ評価器
% 構文木のインタプリタ
eval(I,I):- i(I). % 整数
eval(add(E1,E2),I):- eval(E1,I1),eval(E2,I2),add(I1,I2,I). % 足し算
eval(sub(E1,E2),I):- eval(E1,I1),eval(E2,I2),sub(I1,I2,I). % 引き算
eval(mul(E1,E2),I):- eval(E1,I1),eval(E2,I2),mul(I1,I2,I). % 掛け算
eval(div(E1,E2),I):- eval(E1,I1),eval(E2,I2),div(I1,I2,I). % 割り算

% 数式計算のテスト
:- eval(add('15','23'),'38').
:- eval(sub('38','15'),'23').
:- eval(mul('8','8'),'64').
:- eval(div('33','2'),'16').
:- eval(add(mul('1','2'),mul('3','4')),R),writeln(R),R='14'.

/*
中値演算子を定義して用いることで1*2+3*4を 1 mul 2 add 3 mul 4 のような形で計算できるようにします。
また boolの値と比較式、if 式を加えた数式が計算できるようにします。
*/
% 中地演算子の定義
:- op(600,xfy,add).
:- op(500,xfy,mul).
:- op(500,xfy,gt).

% bool値のある数式の計算の定義
eval2(I,I):- i(I).
eval2(add(E1,E2),I):- eval2(E1,I1),eval2(E2,I2),add(I1,I2,I).
eval2(sub(E1,E2),I):- eval2(E1,I1),eval2(E2,I2),sub(I1,I2,I).
eval2(mul(E1,E2),I):- eval2(E1,I1),eval2(E2,I2),mul(I1,I2,I).
eval2(div(E1,E2),I):- eval2(E1,I1),eval2(E2,I2),div(I1,I2,I).
eval2(true,true). % boolのtrue
eval2(false,false). % boolのfalse
eval2(not(E),B):- eval2(E,B1),not(B1,B). % boolの否定
eval2(if(E1,E2,E3),V):- eval2(E1,true)->eval2(E2,V);eval2(E3,V). % if式
eval2(gt(E1,E2),B):- eval2(E1,I1),eval2(E2,I2),gt(I1,I2,B). % 数値の比較
eval2(le(E1,E2),B):- eval2(E1,I1),eval2(E2,I2),le(I1,I2,B). % 数値の比較

% 数式のテスト
:- eval2('1' mul '2' add '3' mul '4',R),writeln(R),R='14'.
% boolのある式のテスト
:- eval2(if('11' gt '22', '1' mul '2' add '3' mul '4',false),R),writeln(R),R='14'.

/*
実はISO-Prologの定義には + - * / などの演算子が含まれているので、数式をそのまま扱えるようにします。
*/
% bool値のある数式の計算の定義
eval3(I,I):- i(I).
eval3(E1+E2,I):- eval3(E1,I1),eval3(E2,I2),add(I1,I2,I).
eval3(E1-E2,I):- eval3(E1,I1),eval3(E2,I2),sub(I1,I2,I).
eval3(E1*E2,I):- eval3(E1,I1),eval3(E2,I2),mul(I1,I2,I).
eval3(E1/E2,I):- eval3(E1,I1),eval3(E2,I2),div(I1,I2,I).
eval3(true,true). % boolのtrue
eval3(false,false). % boolのfalse
eval3(not(E),B):- eval3(E,B1),not(B1,B). % boolの否定
eval3(if(E1,E2,E3),V):- eval3(E1,true)->eval3(E2,V);eval3(E3,V). % if式
eval3(E1<E2,B):- eval3(E1,I1),eval3(E2,I2),gt(I1,I2,B). % 数値の比較
eval3(E1>E2,B):- eval3(E1,I1),eval3(E2,I2),le(I1,I2,B). % 数値の比較

% 数式のテスト
:- eval3('1' * '2' + '3' * '4',R),writeln(R),R='14'.
% boolのある式のテスト
:- eval3(if('11' < '22', '1' * '2' + '3' * '4',false),R),writeln(R),R='14'.

% プログラムの終わり
:- halt.

/*
このようにProlog を用いて段階的に数式を論理の力のみで構築して実行してみることができます。
より数学的には、足し算の前後を書き換えても結果が変わらない交換法則などの証明をしていくと良いのです。
しかしながらPrologには残念ながら定理証明を支援する機能は標準で付いていません。
さらに詳しい証明を行いたいのであれば Coq や Isabelle などの定理証明系のシステムを用いて証明を書いてみることをお勧めします。


*/