Prolog でわかる TAPL 2日目 - 一階述語論理とProlog、MBNF

セレーネー

セレーネー（古希: Σελήνη, Selēnē）は、ギリシア神話の月の女神である。長母音を省略してセレネ、セレーネとも表記される。聖獣は馬、驢馬、白い牡牛。ローマ神話のルーナと同一視される。

Wikipedia セレーネー より

ここでは、TAPLをPrologで実装するための基礎的な仕組みを構築します。
わけわからなくなったらすっ飛ばして構いません。

木文法検査

PrologではXMLやJSON、S式の木構造データに対する検査プログラムを再帰的に定義することができます。

m(I) :- integer(I).
m(M1+M2) :- m(M1),m(M2).
m(M1-M2) :- m(M1),m(M2).
m(M1*M2) :- m(M1),m(M2).
m(M1/M2) :- m(M1),m(M2).

この構文を検査する述語は、以下のように使うことができます:

:- m(1).
:- m(1+2).
:- m('+'(1,2)).
:- m(1+2*3).
:- m('+'(1,'*'(2,3))).
:- halt.

２章で、アリティ2の述語が二項演算子と書けるというようなことが書いてありますが、述語だけではなく、述語内部の項についてもありティ2の項は2高演算子で書くことができます。

MBNF (Math BNF)

BNF はバッカスによって Algol60 のレポートを書くために導入された文法を記述する言語です。
BNF はチョムスキーの文脈自由文法より簡略なため多くの人々に利用されています。
構文解析の分野では EBNF のような拡張や、評価の順番を決定的にした PEG が提案されています。
一方で計算機科学の分野では形式的に構文を定義するために BNF スタイルの記法が開発されました。
数学的な BNF は構文解析と区別するためにフェラーらは What Does This Notation Mean Anyway? ﾆ追いて Math BNF または MBNF と呼びました。[1] TODO:ちゃんと参照する。

MBNF は XML Schema や JSON Schema のような木文法の定義と考えることも出来ます。
以下に Prolog を使った MBNF を用いた構文検査器を示します:

e ::= i | e+e | e-e | e*e | e/e.
:- bnf(e,1+2*3+4).
:- not(bnf(e,x+y)).

MBNF の評価文脈を用いたスモールステップ評価器は以下のようになります:

a::=[]|a+[]|[]+a|a-[]|[]-a|a*[]|[]*a|a/[]|[]/a.
f(A+B,I):-i(A),i(B),I is A+B.
f(A-B,I):-i(A),i(B),I is A-B.
f(A*B,I):-i(A),i(B),I is A*B.
f(A/B,I):-i(A),i(B),I is A div B.
:- run(1+2*3+4*5,R),writeln(R).

int 型しかありませんが型検査器は以下のように記述可能です:

t(I:int):-i(I).
t(A+B:int):-t(A:int),t(B:int).
t(A-B:int):-t(A:int),t(B:int).
t(A*B:int):-t(A:int),t(B:int).
t(A/B:int):-t(A:int),t(B:int).
:- t(1+2*3+4/5:int).

このように Prolog を使うと BNF を用いたプログラミング言語を簡潔に作ることが出来ます。

Prolog の述語を用いた構文規則は表記が若干冗長なので、BNFのように記述できればより便利です。そこで次のような述語 bnf/2 を定義して構文をBNFスタイルの記法で定義できるようにします。TAPLや多くの論文で用いられるこのような BNF スタイルの記法は MBNF と呼びます。[1]

:- op(1200,xfx,::=).
:- op(650,xfx,∈).
:- op(250,yf,*).
G∈{G}. G∈(G|_). G∈(_|G1):-G∈G1. G∈G.
bnf(S/[S2],AEs) :- compound_name_arguments(AEs,A,Es),bnf(S,A),bnf(S2,Es).
bnf(G,E):-G=..[O|Gs],E=..[O|Es],maplist(bnf,Gs,Es),!.
bnf(G,E):-(G::=Gs),!,G1∈Gs,bnf(G1,E),!.
bnf(i,I):-integer(I),!.
bnf(x,I):- atom(I),!.
bnf(E*,Ls) :- maplist(bnf(E),Ls).

この述語は以下のように用いることができます:

m ::= i | m + m | m - m | m * m | m / m.

:- begin_tests(bnf).
  test(i) :- bnf(i,0),bnf(i,-10),\+bnf(i,abc).
  test(m_i) :- bnf(m,0),bnf(m,-10),\+bnf(m,abc).
  test(add) :- bnf(m,1+2+3),bnf(m,1+(2+3)).
  test(sub) :- bnf(m,1-2-3),bnf(m,1-(2-3)).
  test(mul) :- bnf(m,1*2*3),bnf(m,1*(2*3)).
  test(div) :- bnf(m,1/2/3),bnf(m,1/(2/3)).
  test(mix) :- bnf(m,1+2/3*(4-5)).
:- end_tests(bnf).
:- run_tests.
:- halt.

評価規則

i(I) :- bnf(i,I).
I1+I2 → I3 :- i(I1),i(I2),I3 is I1+I2.
I1-I2 → I3 :- i(I1),i(I2),I3 is I1-I2.
I1*I2 → I3 :- i(I1),i(I2),I3 is I1*I2.
I1/I2 → I3 :- i(I1),i(I2),I3 is I1 div I2.
M1+M2 → M1_+M2 :- M1 → M1_.
I1+M2 → I1+M2_ :- i(I1),M2 → M2_.
M1-M2 → M1_-M2 :- M1 → M1_.
I1-M2 → I1-M2_ :- i(I1),M2 → M2_.
M1*M2 → M1_*M2 :- M1 → M1_.
I1*M2 → I1*M2_ :- i(I1),M2 → M2_.
M1/M2 → M1_/M2 :- M1 → M1_.
I1/M2 → I1/M2_ :- i(I1),M2 → M2_.

M ↠ M_                           :- M → M1, M1 ↠ M_.
M ↠ M.

term_expansion

Prolog のマクロ機構のような項を展開する述語 term_expansion/2 を使うことでより評価規則に近い形での評価規則が記述可能です:

i3 is i1+i2
----------------------- (E-Add)
i1+i2 → i3

このような規則は以下のように記述できます:

i(I1),i(I2),I3 is I1+I2
--%-------------------- (E-Add)
I1+I2 → I3.

この Prolog コードは以下のコードに置き換えられます:

I1+I2 → I3 :- i(I1),i(I2),I3 is I1+I2. % (E-Add)

評価規則のプログラムの全体はここをクリック

bnf(i,I)
--%-------------------- (E-Int)
i(I).

i(I1),i(I2),I3 is I1+I2
--%-------------------- (E-Add)
I1+I2 → I3.

i(I1),i(I2),I3 is I1-I2
--%-------------------- (E-Sub)
I1-I2 → I3.

i(I1),i(I2),I3 is I1*I2
--%-------------------- (E-Mul)
I1*I2 → I3.

i(I1),i(I2),I3 is I1 div I2
--%-------------------- (E-Div)
I1/I2 → I3.

M1 → M1_
--%-------------------- (E-Add1)
M1+M2 → M1_+M2.

i(I1),M2 → M2_
--%-------------------- (E-Add2)
I1+M2 → I1+M2_.

M1 → M1_
--%-------------------- (E-Sub1)
M1-M2 → M1_-M2.

i(I1),M2 → M2_
--%-------------------- (E-Sub2)
I1-M2 → I1-M2_.

M1 → M1_
--%-------------------- (E-Mul1)
M1*M2 → M1_*M2.

i(I1),M2 → M2_
--%-------------------- (E-Mul2)
I1*M2 → I1*M2_.

M1 → M1_
--%-------------------- (E-Div1)
M1/M2 → M1_/M2.

i(I1),M2 → M2_
--%-------------------- (E-Div2)
I1/M2 → I1/M2_.

M → M1, M1 ↠ M_
--%-------------------- (E-All1)
M ↠ M_.

!
--%-------------------- (E-All2)
M ↠ M.

これらの規則は述語 →/2 と ↠/2 の定義に過ぎません。

評価文脈と穴

TAPL の部分型付けあたりで説明されている TODO:調べる アレをコレします。

% 構文

m::= i|m+m|m-m|m*m|m/m.

% 評価文脈

a::=[]|a+[]|[]+a|a-[]|[]-a|a*[]|[]*a|a/[]|[]/a.

% 評価規則

A+B → I :- i(A),i(B),I is A+B.
A-B → I :- i(A),i(B),I is A-B.
A*B → I :- i(A),i(B),I is A*B.
A/B → I :- i(A),i(B),I is A div B.

たったこれだけで言語実装できちゃうのすごくないすか？っていう話です。
[] の箇所が評価文脈の穴であり、穴の中に入った先に評価規則があればそこを評価して穴の箇所を書き換えるという意味合いになります。
ついにリリカル★Lisp の上を我々が行く事ができました事をご報告差し上げる次第であります。

評価文脈と穴のプログラムの全体はここをクリック

calc_hole.pl

:- op(1200,xfx,::=),op(600,xfx,∈).
:- op(250,yf,*).
:- op(920, xfx, ['→', '↠']).
G∈G. G∈(G|_). G∈(_|G2):-G∈G2.
bnf(S/[S2],AEs) :- compound_name_arguments(AEs,A,Es),bnf(S,A),bnf(S2,Es).
bnf(G,E):-G=..[O|Gs],E=..[O|Es],maplist(bnf,Gs,Es),!.
bnf(G,E):-(G::=Gs),!,G1∈Gs,bnf(G1,E),!.
bnf(i,I):-integer(I),!.
bnf(x,I):- atom(I),!.
bnf(m*,Ls) :- maplist(bnf(m),Ls).
n([G|_]/G,[E|Es]/E,[H|Es]/H).
n([_|Gs]/G,[E|Es]/E1,[E|Es_]/H):-n(Gs/G,Es/E1,Es_/H).
h([],E,E,H/H).
h(G,E,V,E_/H):-G=..[O|Gs],E=..[O|Es],n(Gs/G1,Es/E1,Es_/H_),h(G1,E1,V,H_/H),E_=..[O|Es_].
h(G,E,V,E_/H):-(G::=Gs),G1∈Gs,h(G1,E,V,E_/H).
small(F,G,E,E_):-h(G,E,V,E_/H),call(F,V,H),writeln(E_).
all(F)-->call(F),all(F).
all(_)-->!.
i(I):-integer(I).

m::= i|m+m|m-m|m*m|m/m.
a::=[]|a+[]|[]+a|a-[]|[]-a|a*[]|[]*a|a/[]|[]/a.

A+B → I :- i(A),i(B),I is A+B.
A-B → I :- i(A),i(B),I is A-B.
A*B → I :- i(A),i(B),I is A*B.
A/B → I :- i(A),i(B),I is A div B.

run(M) :- bnf(m,M),all(small(→,a),M,_).
:- run((1+2*3)+4*5).
:- halt.

DCG と字句解析

今回の TAPL の解説では使いませんが、 Prolog でも通常のプログラミング言語を作成する場合と同様に字句解析を作ることも可能です。

DCG とは

a(X1,Xn) :- p1(X1,X2),p2(X2,X3),...,pn-1(Xn-1,Xn).

のような述語を

a --> p1,p2,...,pn-1.

と後ろのパラメータ２つを省略して書くことができる Prolog の機能です。

こんな感じ:

digit --> ['0']|['1']|['2']|['3']|['4']|['5']|['6']|['7']|['8']|['9'].

値を返す場合はたしかこんな感じ:

digit(I) --> [I],{member(I,['0','1','2','3','4','5','6','7','8','9'])}.

{}はパラーメータ引き渡しなしです。いいかげんだな。

DCG と構文解析

今回の TAPL の解説では使いませんが、Prolog でも字句リストから構文解析することができます。 DCG を使うことでより宣言的に記述可能となります。

e --> ['('], e, [')'].
e --> digit.
e --> digit,['+'],e.
e --> digit,['*'],e.

関数型言語のパーサコンビネータをモナドのような文脈で隠すような形で DCG を使うと構文解析が書けるわけです。
述語の定義は、BNFのような形でも書けますし、分けて書くこともできるわけです。

e --> ['('], e, [')'] ; digit ; digit,['+'],e ; digit,['*'],e.

のようにも書けるし、たしか、以下のようにも書けたはず:

e --> ['('], e, [')'] | digit | digit,['+'],e | digit,['*'],e.

TODO: 試してないので興味がある人は試してみてください。
構文解析が値を返したい場合は述語のパラメータとして返せば良いので特に悩むことはないです。＜いや悩むだろｗ

論理型言語のパラダイムでのパーサコンビネータのような存在である DCG は述語の拡張でしかないので自由度が高く、構文解析以外にも利用できるのもモナドがパーサコンビネータだけではなく一般的に用いることができる仕組みであるように、一般的に用いることができます。

まとめ

Prolog を使うと関数型言語よりも TAPL の図に近い形でその一部分は簡潔に実装することができます。

構文は XML Schema や JSON Schema と同様の木文法をBNFのようなBNFスタイルで書くことができ、最終的な呼び名がどうなるかはわかりませんが、 MBNF と読んではどうかという話し合いがされています。今回紹介した手法は構文検査しかできません。
しかし、将来的に MBNF は代数的データ型のような型定義も可能となるでしょう。

今日は、簡潔に記述するにはそれなりのテクニックが必要になるので説明しました。
TAPL の2章でも何やら数学的な準備がされており、初心者にとっては難しいと感じるかもしれません。
しかしながら、Prologの様々な技術を理解してしまえば簡単と思えるような事柄が書いてあるだけです。
手書きの字句解析、構文解析、構文を表す BNF や、パーサコンビネータ PEG モナドなどは難しいですが、分かってしまえば簡単になります。
TAPL の２章で説明されている集合論、一階述語論理の推移則などの数学的な記述はより詳細な練習問題や証明するための道具となるので必要になるため書いてあるわけですが、すぐにすべてを理解する必要はありません。
しかし、全体を理解するには必要になる知識なので、#include <stdio.h> というおまじないの中身が紹介されているわけです。

参考文献

[1] What Does This Notation Mean Anyway? David Feller, Joe B. Wells, Fairouz Kamareddine (ULTRA), Sebastien Carlier
https://arxiv.org/abs/1806.08771

Donkey From Wikipedia, the free encyclopedia

The donkey or ass (Equus africanus asinus)[1][2] is a domesticated member of the horse family, Equidae. The wild ancestor of the donkey is the African wild ass, E. africanus. The donkey has been used as a working animal for at least 5000 years. There are more than 40 million donkeys in the world, mostly in underdeveloped countries, where they are used principally as draught or pack animals. Working donkeys are often associated with those living at or below subsistence levels. Small numbers of donkeys are kept for breeding or as pets in developed countries.

どうでもいい筆者のつぶやき

ドンキーコングはロバコングなのかｗ びっくりドンキーはびっくりロバか！

Pāṇini From Wikipedia, the free encyclopedia

This article is about an ancient Sanskrit scholar from the Indian subcontinent. For other uses, see Panini (disambiguation).

Pāṇini (Sanskrit: पाणिनि) (pronounced [paːɳɪnɪ], variously dated between fl. 4th century BCE;[1][2][3][4] and "6th to 5th century BCE"[5][6][web 1][note 1]) was an ancient Sanskrit philologist, grammarian, and a revered scholar in ancient India.[7][9][10] Considered "the father of linguistics",[11] after the discovery and publication of Pāṇini's work by European scholars in the nineteenth century,[12][13] his influence on aspects of the development of modern linguists is widely recognized in the profession; his grammar was influential on foundational scholars such as Ferdinand de Saussure and Leonard Bloomfield.[14] Pāṇini likely lived in Shalatula in ancient Gandhara in the northwest Indian subcontinent, during the Mahajanapada era.[15][4]