メタ論理
メタ論理とは何か。
ここでは、ラムダ計算のアイデアを使って、文や述語を項として扱えるようにします。
まずどんな意味を表せればよいのか明らかにしましょう。たとえば以下の論理式は P という述語の定義になっていますね。
∀x∀y. P(は:x, の:y)⇔食べる(が:x, を:y)
これをちょっと弄って、以下のような記法にします。
P = λ(は:x, の:y).食べる(が:x, を:y)
このようにした時、λ(は:x, の:y).食べる(が:x, を:y) の部分は、語形（名前）から切り離された述語の定義を表す個体になっています（発想は無名関数と同じです）。これは、格と内部で使う変数の対応（は:x, の:yの部分）と論理式（食べる(が:x, を:y)）のセットが表現できれば良いことが分かります。
Varhilには定数や等号がないのでλ(は:x, の:y).食べる(が:x, を:y)を表現できません。そこで、無標格（は）にPを渡すことで表現します（ほかの定数記号がもたぶん同様の表現をすることになります）。
(=λ(は:x, の:y).食べる(が:x, を:y))(は:P)
このとき、Pはただの変数と考えられるでしょう（Pのような変数と、そうでないxyのような変数を文法的に区別しないことで、Pを別の述語に渡すこともできるようになるので便利です）。すると、以下のような変数に引数を渡す表現が必要です。
P(は:x, の:y)
x()
では、これらに対応する表現を見ていきましょう。
抽象節
抽象節 は引数リストと論理式によって述語の定義を表現する節です。
文を 抽象開始 {ABS と 抽象終止 }ABSで挟むことで、 抽象節を作ることができます。単独抽象 /ABS は直後の述語句または名詞句をとって抽象節を作ります。このとき、抽象節の論理式は文または句の論理式がそのまま使われ、引数リストは空のものが作られます。
- {ABS fe://PREが a:DET0+ be://PREを a’a:DET1+ moku:食べる }ABS
- λ().食べる(が:x, を:y)
- /ABS fe://PREが a:DET0+ be://PREを a’a:DET1+ moku:食べる
- λ().食べる(が:x, を:y)
前置詞の直後に名詞句、その後ろに抽象節が来た場合、それは抽象節になります（一階述語論理での前置詞の使い方を拡張しています）。この場合、引数リストには前置詞のが表す格と名詞句が表す変数が追加され、論理式は名詞句の論理式ともとの抽象節の論理式の論理積になります。
- e://PREは a:DET0+ pe://PREの a’a:DET1+ /ABS fe://PREが u:DET0- be://PREを a’a:DET1+ moku:食べる
- λ(は:x, の:y).食べる(が:x, を:y)
抽象節に ラムダ /LAMを前置すると「eは{その抽象節が表す述語}である」のように、変数と述語の定義を結び付ける述語句になります。文中で抽象節がこれ以外の形で現れることはありません。
- e://PREは au:DET /LAM e://PREは a:DET0+ pe://PREの a’a:DET1+ /ABS fe://PREが u:DET0- be://PREを a’a:DET1+ moku:食べる
- (=λ(は:x, の:y).食べる(が:x, を:y))(は:z)
抽象節の内部のみで使われ、また引数リストにも含まれていない変数は、抽象節の内部で量化されます。
評価
評価 /EVA は、直後に名詞句を一つ取って述語句を作ります。評価は抽象節の逆の操作にあたり、変数を述語に還元します。
形式文法
ここまでの文法を形式文法にまとめると、以下のようになります。
<文>
<句>*
<句>
<述語句>
<名詞句>
<否定開始> <文> <否定終止>
<述語句>
<前置詞> <名詞句> <述語句>
<単独否定> <述語句>
<ラムダ> <抽象節>
<評価> <名詞句>
<述語>
<名詞句>
<関係詞> <述語句> <名詞句>
<単独否定> <名詞句>
<述語句>
<限定詞>
<抽象節>
<抽象開始> <文> <抽象終止>
<単独抽象> <句>
<前置詞> <名詞句> <抽象節>
<限定詞>
au
a('[aeiou])*
i('[aeiou])*
u('[aeiou])*
<述語>
(([^aeiou'][aeiou]){2,})
<前置詞>
([^aeiou]?)e
<関係詞>
([^aeiou]?)ei
<単独否定>
no
<否定開始>
nou
<否定終止>
noi
<単独抽象>
<抽象開始>
<抽象終止>
<ラムダ>
<評価>