私は楽しみのために (Java で) 統合アルゴリズムを使用するアプリケーションを開発しています。
私は、統合アルゴリズムが可能なすべての統合を返すことを選択しました。たとえば、私が解決しようとすると
add(X,Y) = succ(成功(0))
それは返す
{X = 成功 (成功 (0))、Y = 0}、{X = 成功 (0)、Y = 成功 (0)}、{X = 0、Y = 成功 (成功 (0))}
ただし、場合によっては、可能な統合が無数に存在する場合があります (たとえば、X > Y = true)。
無限の数の統合が発生する可能性があるかどうかを判断できるアルゴリズムを知っている人はいますか?
前もって感謝します
Prologの文脈で、あなたが「統一」と言うとき、あなたは通常構文を意味します統一。したがって、add（X、Y）とsucc（succ（0））は、ファンクターとアリティが異なるため、（用語として）統合しません。いくつかの追加の方程式または述語が満たされていれば、add（X、Y）やsucc（succ（0））などの別個の用語を統一できる、統一モジュロ理論を参照しているようです。構文の統一は決定可能であり、最も一般的な統一を適用した後でも両方の項に変数がある場合、可能な統一の数は無限です。統一モジュロ理論は一般的に決定可能ではありません。すでに基本的な質問が難しい場合があることを確認するには、たとえば、整数に対する統一問題N> 2、X ^ N + Y ^ N = Z ^ Nを検討します。これは、解が存在するかどうかをアルゴリズムで簡単に判断できる場合（つまり、 、項が統合可能なモジュロ整数算術であるかどうか）、フェルマーの最終定理をすぐに解決するでしょう。マチャセビッチの定理と同様の決定不能性の結果も考慮してください。
特定の制約ロジック プログラミング システムでは、ソリューション セットが無限であるかどうかを簡単に確認できます。たとえば、一部の CLP(FD) 実装 (つまり、SWI-Prolog、Jekejeke Minlog、GNU Prolog や B-Prolog などの他の実装では、有限の上限/下限を想定しているため、そうではありません) では、無限の整数セットを使用したある程度の推論は次のようになります。したがってサポートされます。これは、(SWI-Prolog) のようなインターバル表記で見られます。
?- use_module(library(clpfd)).
true.
?- X #\= 2.
X in inf..1\/3..sup.
ただし、これらのセットには欠点があります。セットの要素が列挙され、インスタンス化された方程式を解こうとするさらなる試みが行われる CLP(FD) ラベル付けでは使用できません。また、CLP(FD) クエリを決定するために一般的に何かを行うことができれば、次の結果に反することになります。
「1900 年に、その深さを認識して、David Hilbert はすべてのディオファントス問題の可解性を彼の有名な問題の 10 番目として提案しました。1970 年に、マティヤセビッチの定理として知られる数学的論理の新しい結果が問題を否定的に解決しました。一般的に、ディオファントス問題は解けない。」(ウィキペディアのディオファントス方程式より)
通常、無限のソリューション セットも処理できる別の制約ロジック プログラミングは、CLP(R) です。そこでは、方程式間の推論が少し強くなります。たとえば、CLP(FD) は次の不一致を検出しません (システムによって異なります。これは SWI-Prolog の結果です。Jekejeke Minlog では、2 番目のクエリに対してすぐに No が表示され、GNU Prolog は約 4 秒間ループします)。いいえ):
?- X #> Y.
Y#=<X+ -1.
?- X #> Y, Y #> X.
X#=<Y+ -1,
Y#=<X+ -1.
一方、CLP(R) は次のことを見つけます。
?- use_module(library(clpr)).
?- {X > Y}.
{Y=X-_G5542, _G5542 > 0.0}.
?- {X > Y, Y > X}.
false.
制約システムは、数論、線形代数、解析などのアルゴリズムを実装することによって機能します。モデル化するドメイン、つまり、表記 CLP( * ) で * が何を示すかによって異なります。これらのアルゴリズムは、限量子の除去まで行うことができます。
さよなら