準決定的 (semidet)

これまで定義した述語は，決定性にdetを指定しており，必ず1つだけ結果を返し，失敗することのない述語でした．ここでは，成功すれば1つ値を返すが，失敗する可能性もあるということを表す semidetを決定性に持った述語を使ってみます．

例: リストの先頭要素を返す述語

以下はリストの先頭要素を返す述語です．

:- pred myhead(list(T)::in, T::out) is semidet.
myhead([X | _], X).

リストが空の場合は，先頭要素を取り出すことができないので失敗します．決定性をsemidetからdetに書き換えると，コンパイル時にエラーとして検出されます．

プログラム

実行結果

1
fail

結果を複数返す可能性のある述語は，非決定的であるといいます．非決定的な述語には，決定性にnondetかmultiを指定します． nondetは失敗する可能性がある述語，multiは失敗しない述語を指定するのに使います．

以下の述語onetwo/1は引数が1か2のとき成功して，それ以外の時に失敗する，決定性がsemidetな述語です．

:- pred onetwo(int::in) is semidet.
onetwo(1).
onetwo(2).

別の書き方では，

:- pred onetwo(int::in) is semidet.
onetwo(N) :- N = 1; N = 2.

です．

上の述語の引数を以下のように，モードをoutに変えて，決定性をmultiにすると，結果として，1と2を返し，失敗することのない非決定的な述語ができます．

:- pred onetwo(int::out) is multi.
onetwo(1).
onetwo(2).

このonetwo/1を使った例を書いてみたいと思います．標準ライブラリのsolutionsモジュールには，非決定的に値を返す述語を受け取って，そのすべての結果をリストにして返してくれるsolutions/2という述語があるので，それを活用したいと思います．

プログラム

実行結果

[1, 2]

リストに追加される順番は不定で，順番はコンパイラの都合で変更される可能性があります．上のプログラムで使っている述語print/3は，任意の値を画面に出力する述語です．

これまでのやり方では，宣言は型とモードの宣言をまとめて，

:- pred onetwo(int::in) is semidet.

のように書いていましたが，じつはこれは，

:- pred onetwo(int).
:- mode onetwo(in) is semidet.

の略記です．述語に対して，型の宣言はひとつしか書けませんが，モードの宣言は複数持たせることができます． onetwo/1は，同じ定義を複数のモードで利用できる述語です．これを表現するには宣言を，

:- pred onetwo(int).
:- mode onetwo(in) is semidet.
:- mode onetwo(out) is multi.

もしくは

:- pred onetwo(int::in) is semidet.
:- mode onetwo(out) is multi.

のように書きます．

探索問題などで，複数の結果を返す可能性があるが，どれか一つ得られればいいという場合，述語solutions/2で複数の結果をすべて求めるのは得策ではありません．そのようなときは，述語の決定性をcc_multiにすることで解決できます．

cc_multiは，その述語の定義は非決定的であるが，そのうちの一つだけを返し，決定的に定義されたかのように振る舞うことを指定します．ここでccは committed choice の略です．

プログラム

実行結果

結果はコンパイラの都合で変わる可能性があります． cc_multiと似た決定生で，cc_nondetというものもあります．これは，nondetな定義で，semidetな動作をさせる時に使います．