論理プログラミングの構文と意味論

論理プログラミングは、 DatalogやPrologなどの形式論理に基づく言語を含むプログラミング パラダイムです。この記事では、これらの言語の純粋に宣言的なサブセットの構文とセマンティクスについて説明します。紛らわしいことに、「論理プログラミング」という名前は、Prolog の宣言的なサブセットにほぼ対応する特定のプログラミング言語も指します。残念ながら、この記事ではこの用語を両方の意味で使用する必要があります。

宣言的論理プログラムは、次のような形式の ルールのみで構成される。

H  :-  B1 、 ...、 BN 。

それぞれの規則は、次のような含意として解釈することができます。

${\displaystyle B_{1}\land \ldots \land B_{n}\rightarrow H}$

「それぞれが真であれば、 も真です」という意味です。論理プログラムは、そのルールによって暗示される事実の集合を計算します。 ${\displaystyle B_{i}}$${\displaystyle H}$

Datalog、Prolog、および関連言語の多くの実装では、Prolog のカット演算子などの手続き型機能や、外部関数インターフェイスなどの論理外機能が追加されています。このような拡張機能の形式的な意味論は、この記事の範囲外です。

Datalog は、最も広く研究されている最も単純な論理プログラミング言語です。Datalog のセマンティクスには 3 つの主要な定義があり、それらはすべて同等です。他の論理プログラミング言語の構文とセマンティクスは、Datalog の構文とセマンティクスの拡張および一般化です。

Datalogプログラムはルールのリスト（ホーン節）で構成されています。^[1] constantとvariableがそれぞれ定数と変数の2つの可算なセットであり、 relationが述語記号の可算なセットである場合、次のBNF文法はDatalogプログラムの構造を表します。

<プログラム>  ::=  <ルール>  <プログラム> | ""
 <ルール>  ::=  <アトム> ":-" <アトムリスト> "."
 <アトム>  ::=  <関係> "(" <用語リスト> ")"
 <アトムリスト>  ::=  <アトム> | <アトム> "," <アトムリスト> | ""
 <用語>  ::=  <定数> | <変数> 
<用語リスト>  ::=  <用語> | <用語> "," <用語リスト> | ""

アトムはリテラルとも呼ばれます。シンボルの左側のアトムはルールのヘッド:-と呼ばれ、右側のアトムはボディと呼ばれます。すべてのDatalogプログラムは、ルールのヘッドに現れるすべての変数がボディにも現れるという条件を満たす必要があります（この条件は範囲制限と呼ばれることもあります）。^{[1] [2]}

本体が空のルールはファクトと呼ばれます。たとえば、次のルールはファクトです。

r ( x )  :-  .

論理プログラミングの多くの実装では、上記の文法を拡張して、:-次のように なしで事実を記述できるようにします。

r ( x ) です。

多くの場合、次のように括弧なしで 0 項関係を記述することもできます。

p  :-  q .

これらは単なる略語 (構文糖) であり、プログラムの意味には影響しません。

次のプログラムは、関係 の推移閉包pathである関係 を計算します。 edge

エッジ( x 、 y )。
エッジ( y 、 z )。
パス( A 、 B )  :- 
  エッジ( A 、 B )。
パス( A 、 C )  :- 
  パス( A 、 B )、 
  エッジ( B 、 C )。

Datalogプログラムのセマンティクスには、モデル理論的、固定小数点的、証明理論的の3つのアプローチが広く使用されています。これら3つのアプローチは同等であることが証明されています。^[3]

アトムは、そのサブタームのいずれも変数でない場合、グラウンドと呼ばれます。直感的に、各セマンティクスは、プログラムの意味を、事実から始めて、プログラムのルールから推測できるすべてのグラウンド アトムの集合として定義します。

ルールのすべてのアトム (ヘッドとボディ) がグラウンドである場合、そのルールはグラウンドと呼ばれます。グラウンド ルールR ₁は、別のルールR _2のグラウンド インスタンスである場合、つまり、 R _{1 が}R ₂のすべての変数を定数に置き換えた結果である場合です。

Datalog プログラムのHerbrand基底は、プログラムに現れる定数で作成できるすべての基底アトムの集合です。解釈(データベース インスタンスとも呼ばれる) は Herbrand 基底のサブセットです。基底アトムは、解釈Iの要素である場合に、解釈Iで真となります。規則は、その規則の各基底インスタンスについて、本体のすべての節が I で真である場合、規則のヘッドも I で真である場合に、 解釈 I で真となります。

DatalogプログラムPのモデルは、 Pの解釈Iであり、 Pのすべての基本事実を含み、IにおいてPのすべての規則が真となる。モデル理論的意味論によれば、Datalogプログラムの意味はその最小モデル（つまり、すべてのモデルの共通部分）である。^[4]

たとえば、このプログラム:

エッジ( x 、 y )。
エッジ( y 、 z )。
パス( A 、 B )  :- 
  エッジ( A 、 B )。
パス( A 、 C )  :- 
  パス( A 、 B )、 
  エッジ( B 、 C )。

エルブラン宇宙にはx、、、yz

そしてこのエルブラン基底: edge(x, x)、、edge(x, y)... edge(z, z)、、、path(x, x)...、path(z, z)

そしてこの最小限のエルブランモデル: edge(x, y)、、、、、edge(y, z)path(x, y)path(y, z)path(x, z)

I をDatalog プログラムPの解釈の集合、すなわちI = P ( H )とする。ここでHはPのエルブラン基底、P はべき集合演算子である。Pの即時結果演算子は、 IからIへの次の写像Tである。 Pの各ルールの各基底インスタンスについて、本体のすべての節が入力解釈に含まれる場合、基底インスタンスのヘッドを出力解釈に追加する。この写像T は、 T上の部分集合包含によって与えられる半順序に関して単調である。Knaster–Tarski 定理により、この写像には最小の不動点がある。Kleeneの不動点定理により、不動点は連鎖の上限である。 Mの最小の不動点は、プログラムの最小エルブランモデルと一致する。^[5]${\displaystyle T(\emptyset ),T(T(\emptyset )),\ldots ,T^{n}(\emptyset ),\ldots }$

固定点セマンティクスは、最小のエルブラン モデルを計算するためのアルゴリズムを提案します。プログラムの基本事実のセットから始めて、固定点に到達するまでルールの結果を繰り返し追加します。このアルゴリズムは、ナイーブ評価と呼ばれます。

プログラムPが与えられたとき、基底原子Aの証明木は、 Aでラベル付けされた根、 P内の事実の頭部からの基底原子でラベル付けされた葉、基底原子Gでラベル付けされた子を持つ枝を持つ木であり、基底インスタンスが存在する。 ${\displaystyle A_{1},\ldots ,A_{n}}$

G :- A1, ..., An.

Pの規則の証明理論的意味論では、Datalogプログラムの意味は、そのような木から定義できる基底原子の集合であると定義される。この集合は、最小のエルブランモデルと一致する。^[6]

モデルの残りの部分についてはあまり気にせず、特定の基底原子が Datalog プログラムの最小 Herbrand モデルに現れるかどうかを知ることに興味があるかもしれません。上記の証明ツリーをトップダウンで読み取ると、そのようなクエリの結果を計算するアルゴリズムが示唆され、そのような読み取りはSLD 解決アルゴリズムに情報を提供し、これがPrologの評価の基礎となります。

Datalogの意味論は、より一般的な半環上の不動点の文脈でも研究されてきた。^[7]

「論理プログラミング」という名前は、Datalog や Prolog を含むプログラミング言語のパラダイム全体を指すために使用されますが、形式意味論について議論する場合、通常は関数シンボルを使用した Datalog の拡張を指します。論理プログラムは、ホーン節プログラムとも呼ばれます。この記事で説明する論理プログラミングは、 Prologの「純粋な」または宣言的なサブセットに密接に関連しています。

論理プログラミングの構文は、関数シンボルを使用してDatalogの構文を拡張します。論理プログラミングでは範囲制限がなくなり、ルール本体には現れない変数がルールの先頭に現れるようになります。^[8]

関数記号の存在により、論理プログラムのエルブランモデルは無限になる可能性がある。しかし、論理プログラムの意味論は依然としてその最小エルブランモデルとして定義される。関連して、即時結果演算子の不動点は有限数のステップ（または有限集合）で収束しない可能性がある。しかし、最小エルブランモデルのどの基底原子も有限の証明木を持つ。これが、Prologがトップダウンで評価される理由である。^[8] Datalogと同様に、3つの意味論は同等であることが証明できる。

論理プログラミングには、論理プログラムの意味論の 3 つの主要な定義がすべて一致するという望ましい特性があります。対照的に、否定を含む論理プログラムの意味論については、相反する提案が多数あります。不一致の原因は、論理プログラムには固有の最小エルブラン モデルがあるのに、一般に、否定を含む論理プログラミング プログラム (または Datalog プログラム) にはそれがないことです。

否定は と記述されnot、ルール本体の任意のアトムの前に出現できます。

<アトムリスト>  ::=  <アトム> | "not" <アトム> | <アトム> "," <アトムリスト> | ""

否定を含む論理プログラムは、各関係を何らかの層に割り当てることができるときに階層化されているとみなされます。つまり、関係R が関係Sの本体で否定されて現れる場合、RはSよりも低い層にあります。^[9] Datalogのモデル理論的および固定小数点意味論は、階層化された否定を処理するように拡張することができ、そのような拡張は同等であることが証明できます。

Datalog の多くの実装では、固定小数点セマンティクスにヒントを得たボトムアップ評価モデルを使用します。このセマンティクスは層別否定を処理できるため、Datalog のいくつかの実装では層別否定を実装しています。

層別否定はDatalogの一般的な拡張であるが、層別化できない合理的なプログラムもある。次のプログラムは、対戦相手が何も動かなかった場合にプレイヤーが勝つ2人用ゲームを記述している。^[10]

move ( a ,  b ). 
win ( X )  :-  move ( X ,  Y ) であり、 win ( Y )ではありません 。

このプログラムは階層化されていませんが、aゲームに勝つと考えるのが妥当と思われます。

安定モデルの意味論は、プログラムの特定のエルブランモデルを安定と呼ぶための条件を定義します。直感的に、安定モデルとは、「[プログラム]を前提として、合理的なエージェントが持つ可能性のある信念の集合」です。^[11]

否定を含むプログラムには、安定モデルが多数存在する場合もあれば、全く存在しない場合もある。例えば、次のプログラム

p  :- は qではありません 。q :- はpではありません。
   

には2つの安定したモデルがあります。1ルールプログラム ${\displaystyle \{p\}}$${\displaystyle \{q\}}$

p  :- ではなく pです。

安定したモデルはありません。

すべての安定モデルは、最小エルブラン モデルです。否定のない Datalog プログラムには、単一の安定モデルがあり、これはまさにその最小エルブラン モデルです。安定モデル セマンティクスは、否定のあるロジック プログラムが、その安定モデル (1 つだけ存在する場合) である意味を定義します。ただし、プログラムの安定モデルをすべて(または少なくともいくつか) 調査すると便利な場合があります。これが、アンサー セット プログラミングの目標です。

Datalogの他の拡張としては、整数定数と関数（DatalogZを含む）をサポートする変種、 ^{[12] [13]} ルール本体の不等式制約、集約関数などが提案され研究されている。

制約ロジック プログラミングでは、実数や整数などのドメインに対する制約をルールの本体に表示できます。

• エルブラン構造
• 論理プログラミング
• 失敗としての否定
• Prologの構文と意味論

• Ceri, S.; Gottlob, G.; Tanca, L. (1989 年 3 月) 。「Datalog についていつも知りたかったこと (そして聞く勇気がなかったこと)」( PDF )。IEEE Transactions on Knowledge and Data Engineering。1 ( 1): 146–166。CiteSeerX 10.1.1.210.1118。doi : 10.1109 /69.43410。ISSN 1041-4347  。