エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

論理プログラミング(2)

Prologのプログラムでは否定を扱うことができないため、Prologのデータは分配的な束と考えることができます。これは可換な冪等半環で加法に関しても乗法に関しても分配的なものと考えることができます。

ここでは PLP のデータをまず半環として数学的に定義することをやっていきます。

PLP で定義できる形式の論理式の集合(PLP ではホーン節の集合)から導出によって得られるものと、その論理式の集合から一階述語論理の推論規則(たとえば自然演繹)によって得られるものが同じものになるということを見ていきます。

PLP の一回分の導出を微分を考えて、その極限を考えることにより無限に実行することができる論理プログラミングを考えます。この無限に実行することができる論理プログラミングを PLP+ と呼ぶことにします。