7

次の Clojure コードはcore.logic、2 つの異なる順序で同じ目標を持つ同じ論理問題を解決するために使用します。このような順序の選択により、一方はすぐに終了し、もう一方はハングします。 

(use `clojure.core.logic)

;; Runs quickly.  Prints (1 2 3).
(clojure.pprint/pprint (run* [q] (fresh [x] (== x [1,2,3]) 
                                            (membero q x))))

;; Hangs
(clojure.pprint/pprint (run* [q] (fresh [x] (membero q x) 
                                            (== x [1,2,3]))))

この問題を回避するための一般的な解決策または一般的な方法はありますか?

4

2 に答える 2

8

ここに私の理解があります：

ではcore.logic、検索スペースをできるだけ早く削減したいと考えています。制約を最初に置くmemberoと、実行はスペースを検索することから開始memberoされ、制約によって生成された失敗でバックトラックし==ます。しかし、どちらも統一されていないか、少なくとも制限されていないため、memberoスペースは巨大です。qx

しかし、制約を最初に置くと、 と==直接統合され、現時点での探索空間は明らかに の要素に限定されます。x[1 2 3]memberox

于 2013-01-13T21:01:56.123 に答える
3

を使用する場合membero、この問題に対する一般的な解決策はありません。新鮮な vars で呼び出すmemberoと、メンバーである可能性のあるすべての (読み取り、無限) リストが生成されますq。もちろん、3 より大きいリストは適用されません - しかし、あなたが使用run*したので、それぞれが失敗しても、カウント 3 より大きいリストをやみくもに試行し続けます。

制約インフラストラクチャを使用してより新しいバージョンの core.logic のより良いバージョンを作成することmemberoは可能ですが、これを行う方法の詳細は今後数か月で変更される可能性があります。制約を定義するための堅実なパブリック API が存在するまでは、Prolog を悩ませる微妙な順序付けや非終了の問題に悩まされます。

于 2013-01-13T23:50:44.937 に答える