操作的意味
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2020/10/15 19:56 UTC 版)
「制約論理プログラミング」の記事における「操作的意味」の解説
制約論理プログラミングを状態遷移システムとしてとらえた場合の操作的意味は状態 ⟨ 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 が実行結果となる。 状態遷移システムの遷移は以下のように表現できる。 ⟨ 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} がない場合。失敗（fail）する。 ⟨ A ∪ c , C , S ⟩ → c ⟨ A , C , S ∪ c ⟩ {\displaystyle \langle A\cup c,C,S\rangle \rightarrow _{c}\langle A,C,S\cup c\rangle } A 内に制約 c があれば制約ストアに移動する。 ⟨ A , C , S ⟩ → i ⟨ A , C ′ , S ′ ⟩ {\displaystyle \langle A,C,S\rangle \rightarrow _{i}\langle A,C',S'\rangle } 制約ストア内の制約を制約評価系で簡約化する（ ( C ′ , S ′ ) = i n f e r ( C , S ) {\displaystyle \left(C',S'\right)=infer\left(C,S\right)} ）。まだ利用できない受動的な制約の集まり S で利用可能なものがあれば C に移し、利用可能な制約の集まり C はより単純な制約に簡約化する。 ⟨ A , C , S ⟩ → s ⟨ A , C , S ⟩ {\displaystyle \langle A,C,S\rangle \rightarrow _{s}\langle A,C,S\rangle } 能動的な制約の集まり C の一貫性チェック c o n s i s t e n t ( C ) {\displaystyle consistent\left(C\right)} に問題がない場合。そのまま遷移を続ける。 ⟨ A , C , S ⟩ → s f a i l {\displaystyle \langle A,C,S\rangle \rightarrow _{s}fail} 能動的な制約の集まり C の一貫性チェックが成立しない場合（ ¬ c o n s i s t e n t ( C ) {\displaystyle \neg consistent(C)} ）。失敗（fail）する。 ここで i n f e r ( C , S ) {\displaystyle infer\left(C,S\right)} は制約評価の関数、 c o n s i s t e n t ( C ) {\displaystyle consistent\left(C\right)} は制約の一貫性チェック述語を表し、制約の領域ごとに異なる。多くの制約論理プログラミングシステムの操作的意味は → r → i → s {\displaystyle \rightarrow _{r}\rightarrow _{i}\rightarrow _{s}} と → c → i → s {\displaystyle \rightarrow _{c}\rightarrow _{i}\rightarrow _{s}} の遷移の組み合わせで表される。 また、 A からの原子論理式や制約の取り出しと追加はLIFOの順番に行われることが多い。この場合はPrologと同様の深さ優先探索の動作になり、途中で失敗（fail）した場合はバックトラックが行われる。
※この「操作的意味」の解説は、「制約論理プログラミング」の解説の一部です。
「操作的意味」を含む「制約論理プログラミング」の記事については、「制約論理プログラミング」の概要を参照ください。
- 操作的意味のページへのリンク
