問題タブ [successor-arithmetics]

私は楽しみのために (Java で) 統合アルゴリズムを使用するアプリケーションを開発しています。

私は、統合アルゴリズムが可能なすべての統合を返すことを選択しました。たとえば、私が解決しようとすると

add(X,Y) = succ(成功(0))

それは返す

{X = 成功 (成功 (0))、Y = 0}、{X = 成功 (0)、Y = 成功 (0)}、{X = 0、Y = 成功 (成功 (0))}

ただし、場合によっては、可能な統合が無数に存在する場合があります (たとえば、X > Y = true)。

無限の数の統合が発生する可能性があるかどうかを判断できるアルゴリズムを知っている人はいますか?

前もって感謝します

私は公理の解決がプロローグでどのように機能するかを理解しようとしています。

自然数に対して2つの基本的な操作を定義すると仮定しましょう。

• s（term）（後継者を表す）および

• add（term、anotherTerm）。

addのセマンティクスは次のように与えられます

• 追加（0、x1）-> x1

• 追加（x1、0）-> x1

• add（s（x1）、y1）-> s（add（x1、y1））

次に、方程式を解きたい

add（x、add（y、z））= s（0）

一つの戦略は

• 方程式の右辺（RHS）が左辺（LHS）と等しいかどうかをテストします

• 解決策が見つからない場合は、最も一般的なユニファイアを探してください

• そうでない場合は、この方程式で使用できる公理を見つけてください。この仕事をするための戦略は次のようになります（公理ごとに）：方程式のRHSが公理のRHSに等しいことを解こうとします。解がある場合は、方程式のLHSが公理のLHSに等しいことを解いてみてください。それが成功した場合、私たちは正しい公理を見つけました。

• 最終的に、解がなく、方程式のLHSとRHSが同じ操作（つまり、同じシグネチャであるが同じオペランドではない）の場合、各オペランドにアルゴリズムを適用し、各オペランドの解が見つかった場合に解が見つかります。

この（単純な）アルゴリズムはうまくいくと思います。しかし、このような問題を解決した経験のある人がいるかどうか知りたいのですが。より良いアルゴリズムに関するドキュメントがどこにあるか知っている人はいますか？

前もって感謝します

編集：解決しました。ソースファイルで言語拡張を有効にしても、GHCiで言語拡張が有効にならないことに気づいていませんでした。解決策は:set FlexibleContextsGHCiでした。

私は最近、Haskellのクラスとインスタンスの型宣言がホーン節であることを発見しました。そこで、 The ArtofPrologの第3章の算術演算をHaskellにエンコードしました。例えば：

Prologでは、値はプルーフの（論理）変数に対してインスタンス化されます。しかし、Haskellで型変数をインスタンス化する方法がわかりません。つまり、HaskellがPrologクエリに相当するものが何であるかがわかりません

は。私は

Haskellがインスタンス化する原因になりますxiが、これを有効Non type-variable argument in the constraintにしてもエラーが発生します。FlexibleContexts

自然数の次の手順は SWI-prolog です。

ここで、0 に到達すると停止する再帰呼び出しを実行したいと考えています。

私の自然数は -s(0)=0, s(s(0))=1, s(s(s(0)))=2, etc

だから私は定義します：

と呼び出します:3,5,s(0). しかし、それは私にエラーを与えます: out of local stack。

何が問題ですか？ありがとうございました。

ここに私が理解していないプラスコードがあります

与えられた間：

この再帰がわかりません。私が持っている場合、plus(s(0),s(s(s(0))),Z)どうすれば答えを得ることができ1+3=4ますか?

最初のコードについて説明が必要です。再帰を止めようとしplus(0,X,X)ますが、間違っていると思います。

次のルールがあります

クエリは次のとおりackermann (M,N,s(s(0)))です。

さて、私が理解したように、3番目の計算では、無限の検索（失敗ブランチ）が得られました。確認したところ、有限検索（失敗分岐）が出ました。

説明します：最初に、M = 0、N = s（0）の置換を取得しました（ルール1-成功！）。2番目では、M = s（0）、N = 0の置換を取得しました（ルール2-成功！）。しかし、今は何ですか？M = s（s（0））N = 0に一致させようとしましたが、有限検索-失敗ブランチが得られました。コンパイラが私に「失敗」と書かないのはなぜですか。

ありがとうございました。

私は、剰余の定理と整列原理を使用して、プロローグの分割を定義しようとしています。

私はこれまでに持っています：

しかし、の定義divはどういうわけか間違っています。誰かが私にヒントを教えてもらえますか？

PS：私は使うべきではありませんが、私は得ることも働くeqこともできませんでした。is=

数字の表現として、この非常に単純なコードがあります。問題は add2 関数を使用するときです。

例:正しくadd2(s(0)+s(s(0)), s(s(0)), Z).返されます。s(s(s(s(s(0)))))しかしadd2(0, s(0)+s(s(0)), Z).、常にreturns s(0)+s(s(0))。なぜこれが起こっているのか誰にもわかりますか？

私は Prolog を学ぼうとしてきましたが、述語 s() が何をするのか完全に困惑しています。私はそれが頻繁に使用されているのを目にしますが、インターネット上には Prolog に関するリソースがほとんどないため、答えを見つけることができません。

元。

チュートリアルで論理数のこの自然数評価に出くわしましたが、頭痛の種になっています。

このルールは大まかに次のように述べています:Nが自然数である場合、そうでない場合は、の内容が になるまで再帰的にルール0に送り返そうとします。そうでない場合は自然数ではありません。s/10

s(0)そこで、上記のロジックの実装をテストして、 as1およびs(s(0))asを表現したい場合はうまくいくと思いましたが、代わり2に に変換できるようにしたいと考えています。s(0)1

私は基本ルールを考えました：

ここに私の質問があります: s(0) を 1 に、s(s(0)) を 2 に変換するにはどうすればよいですか?

回答済み

編集：私が受け入れた答えが私に向けた実装の基本ルールを変更しました：

これで思い通りに使えるようになりました、ありがとうございます！