はじめに
前回の投稿で、Montague文法がニューロシンボリックAIに応用可能であることが見えてきました。Montague文法は自然言語(英語など)をラムダ式に変換する仕組みを持っています。もしこのラムダ式をProlog上で評価できれば、Montague文法で得た構文的意味を直接実行できるようになります。
今回、Prologでラムダ計算の簡約機構を実装しました。
ラムダ計算とは?
ラムダ計算は計算機科学のもっとも基本的な理論体系のひとつです。Lispを設計したジョン・マッカーシー博士も、この理論を参考にしたとされています。提唱者はアロンゾ・チャーチで、Turingと並び計算可能性理論の祖として知られています。
記法の工夫(Prolog向け)
チャーチの記法(λx.x)はPrologで直接扱うにはやや不便なので、述語論理風の構文に変換して扱います。
ラムダ記法 Prolog記法
λx.x l(x, x)
(λx.x) a [l(x,x), a]
このように、ラムダ抽象は l(変数, 本体)、適用はリスト [関数, 引数] の形式で表現します。
ベータ簡約
ラムダ計算では、関数適用はすべて「変数への置換(β変換)」によって処理されます。
たとえば:
?- reduce([l(x, x), a], Y).
Y = a.
このように、l(x,x) に a を適用すると、変数 x が a に置き換えられて a に簡約されます。
アルファ変換
変数名の衝突を避けるために、変数名を変更する処理が必要になる場合があります。
たとえば:
l(x, l(x, x)) → l(x, l(x0, x0))
内側のラムダ式の x は別の引数として束縛されているため、外側と名前が重なると意味が曖昧になります。そのため、名前を変更して区別を明確化します。これを α変換 と呼びます。
実行例(Prolog)
Prologで定義した述語 reduce/2 を使うことで、ラムダ式の簡約が可能になります。
以下に代表的な例を示します:
% 恒等関数の適用
?- reduce([l(x, x), a], Y).
Y = a.
% 定数関数の適用
?- reduce([l(x, y), a], Y).
Y = y.
% ラムダ式の返り値に変数が含まれる場合
?- reduce([l(x, l(y, x)), a], Y).
Y = l(y1, a).
% ネストされた適用
?- reduce([[l(x, l(y, x)), a], b], Y).
Y = a.
% 定数
?- reduce(a, a).
% λ式そのもの(簡約されない)
?- reduce(l(x, x), Y).
Y = l(x, x).
% 引数に関数を含む例
?- reduce([l(x, [x, z]), [l(y, y), a]], Y).
Y = [[l(y, y), a], z].
おわりに
Montague文法で生成されたラムダ式をPrologで実行することが可能になれば、意味論処理と論理推論を統一的に扱うことができます。これは、ニューロシンボリック統合における一つの実践的アプローチでもあり、Prologの表現力の高さを活かした応用例として注目に値します。
全コード
https://github.com/sasagawa888/nprolog/blob/master/library/lambda.pl