PLP のデータとなる項を定義します。
記号の有限集合 があってその元を定数と呼びます。定数は項となります。
記号の可算集合 があってその元を変数と呼びます。変数は項となります。
記号の有限集合 があってその元を関数と呼びます。関数 に対して という形の記号の列は項となります。ここで は項です。
以上で定義された最小のものが項となります。項全体の集合を とおきます。
関数は変数に依存した項を表すためのもので、「シークエント計算」のところでは説明していなかったのでこの後説明していくことにします。
次に PLP のプログラムを定義します。
記号の有限集合 があってその元を述語と呼びます。述語 に対して という形の記号の列はを述語式と呼ぶことにします。ここで は項です。述語式全体の集合を とおきます。
の形の列をホーン節と呼びます。ここで は述語式です。これは
という論理式を表しています。以下では論理式の意味で使うこともあります。 の場合もあり、これは
と書きます。
ホーン節の がない場合は が「偽」の場合を表し
という論理式を表します。これをゴール節と呼び Prolog では
と書きます。これはホーン節には含めないことにします(通常は含めるようですが)。
PLP のプログラムは有限個のホーン節と1個のゴール節からなります。ゴール節は1個の述語式からなるものを考えます。複数の場合
をゴール節に追加してゴール節は だけにすることができます。
次に PLP で使う論理式を定義します。
述語式全体の集合 によって自由生成される半環を とおきます。これは を含む最小の半環で の元と2項演算子 と で書くことができるものの全体になります。 は分配法則が成り立つので の元は
という形に書くことができます。この形を選言標準形と呼びます。
を連言節と呼ぶことにします。 の元は選言標準形で書かれていると考えることにして、 の元を正規化された論理式と呼ぶことにします。
次にシークエント計算のところで見た からまでの議論について見てみると、PLP のプログラムはある述語式に正規化された論理式と対応させる写像
と考えることができます。この写像を拡張して
と考えます。この写像を微分と呼ぶことにします。微分 と述語式 に対して可算個の列
を考えて、これを の による極限と呼び、 と書くことにします。
この極限を使って関数プログラミング、オブジェクト指向プログラミングを表すとどうなるかというのがここでの議論の目的となるので、後で考えていくことにします。
次に PLP のプログラムと証明の関係について考えていきます。
項の定義で変数を含まないように定義したものを変数を含まない項と呼びその全体の集合を とおきます。 から への写像を から への写像に拡張したものを代入と呼びます。 を代入全体の集合とし、 をその冪集合とします。
正規化された論理式 に対して
の という形の述語式以外の述語式を true で置き換えたものを 、
の という形の述語式以外の述語式を false で置き換えたものを
と書きます。 を を が true となる代入 全体の集合に写す写像とします。
となる が存在するときこのプログラムは失敗(証明できない)、
となる が存在するときこのプログラムは成功(証明可能)、
任意の に対して かつ のときこのプログラムは無限に実行されます(終了しない)。