ライブラリはMathelで記述されており、FOLは他ソフトとの橋渡しとして使用されます。
まずはFOLに焦点をあてて作っていきます。（一般の一階言語については既知とします…）
a1
一般に言語は「単語の列」のうち文法を満たすもので構成されます。ここでは機械にとって処理しやすいprefix形の文法を採用します。\(\dagger\)
私たちの言語
記号列のうち一定の規則を満たすものをFormといいます。FOLでは、Formのうち通常使用されるものはs-Formとp-Formです。\(\dagger\)
Formはいくつかの形をとりますが、そのうちの一つにprefix形があります。
wordのgram
prefix Formで使用される記号はwordと呼ばれます。
wordはgramというデータを持ちます。gram は (gram0, gram1) という形になります。
FOLでは次の形になります。
・gram0 … s,p の列か vp
・gram1 … s,p のどれか
また、arity : gram0の長さ、ただし gram0がvp ⇒ arity : q とされます。
var
phpの正規表現に倣ったものを準備します。数字を[0-9]とします。
ローマ字の小文字を[a-z]、小文字と大文字を[a-zA-Z]とします。
ギリシャ字はローマ字にないもののみ用いられ [greek] とします。\(\dagger\)
0回以上の繰り返しを*、またはを|で表します。
prefix Form
Formは、wordの列で帰納的に作成されます。
・\({\tt w}\)がword[arity : \({\tt n}\)], \({\tt F}_1,\cdots,{\tt F}_{\tt n}\)がForm ⇒ \({\tt wF}_1\cdots{\tt F}_{\tt n}\)がForm
・\({\tt w}\)がword[arity : q], \({\tt x}\)がvar, \({\tt F}\)がForm ⇒ \({\tt wxF}\)がForm
s-Form, p-Form の細かい規則として、例えば
・\({\tt w}\)がword(s,p)，\({\tt S}\)がs-Form ⇒ \({\tt wS}\)がp-Form
a2
prefix形は人間には読みにくいので他の形を導入します。省略表現もできるようにします。
使用される記号が増えます。
wordの表記法
arityが0でないwordは表記法データも持ちます。それは次の2種類のどちらかになります。
F 結合性(LかR)およびprecedの組
結合性は通常は L です。precedは自然数ですが、大小関係に意味があります。
decent Form
{ } を含むForm
％ を ;; に変更すべし
( ) を補わない { } を含むForm
{ } は通常はFormとしての塊を作りますが、稀にその塊を崩すこともあります。
abbrを使用するときは ( ) を補いますが、補わないものは abbr* とされます。
a3
言語の取り扱いで注意すべきものを挙げます。
Formの同値、代入
表記上の注意
メタ自然数の利用
\n+1等も使えるように。xn は x\n に変更すべし。
a4
ここでMathelの正式な作成をします。
一階言語の拡張
Mathelでは使用されるFormにc-Formが加わります。\(\dagger\)wordのgramも次のように拡張されます。\(\dagger\)
・gram0 … s,c,p の列か vp
・gram1 … s,c,p のどれか
Formを作る規則～代入はFOLと同様です。
FOLとMathelのword
FOLのwordはすべてMathelのwordになります。
FOLのwordはMathelのwordになったとき、稀にgramが変化することがあります。