制約論理プログラミング
⟨ A ∪ a , C , S ⟩ → r ⟨ A ∪ B , C , S ∪ ( a = h ) ⟩ {\displaystyle \langle A\cup a,C,S\rangle \rightarrow _{r}\langle A\cup B,C,S\cup (a=h)\rangle }
A 内の原子論理式 a ( L ( t 1 , ... , t n ) {\displaystyle L(t_{1},\ldots ,t_{n})} )について、ルール h ← B {\displaystyle h\leftarrow B} があり、ヘッド部 h ( L ( t 1 ′ , ... , t n ′ ) {\displaystyle L(t_{1}',\ldots ,t_{n}')} )が変数の書き換えで同じにできる場合。この場合は原子論理式 a を書き換える。ここで ( a = h ) {\displaystyle \left(a=h\right)} は t 1 = t 1 ′ , ... , t n = t n ′ {\displaystyle t_{1}=t_{1}',\ldots ,t_{n}=t_{n}'} を表す。
⟨ A ∪ a , C , S ⟩ → r f a i l {\displaystyle \langle A\cup a,C,S\rangle \rightarrow _{r}fail}
原子論理式 a を書き換え可能なルール h ← B {\displaystyle h\leftarrow B} がない場合。
制約論理プログラミングを状態遷移システムとしてとらえた場合の操作的意味は状態 ⟨ A , C , S ⟩ {\displaystyle \langle A,C,S\rangle } の遷移として表現できる。 A は原子論理式や制約の多重集合、 C 、 S は制約の多重集合を表す。 C と S とは制約を格納する制約ストアを表し、システム内部の制約評価系の処理対象となる。 A はまだ見えていない原子論理式や制約の集まりを表し、Prologなどの論理プログラミング言語でのゴールの集合にあたる。 C は能動的な(利用可能な)制約の集まりで、 S はまだ利用できない受動的な制約の集まりである。例えば、制約評価系が線型連立方程式のみを扱える場合、 x*y=z のような非線型な式は利用できないため S に格納されるが、もし x=2 の制約が追加された場合は線型な式 2*y=z に変わるため能動的な制約の集まりである C に格納され、制約評価系で簡約化が行われる。 実行の最初のゴール G {\displaystyle G} は、システムの初期状態 ⟨ G , ∅ , ∅ ⟩ {\displaystyle \langle G,\emptyset ,\emptyset \rangle } で表される。導出が成功した場合、最後の状態は ⟨ ∅ , C , S ⟩ {\displaystyle \langle \emptyset ,C,S\rangle } であり、 C と S が実行結果となる。
状態遷移システムの遷移は以下のように表現できる。