問題タブ [unification]

OCaml での型推論の実装を詳しく見てみたいと思います。私の OCaml は にインストールされているようですが、内部には型推論のためのコードが含まれて/usr/local/lib/ocamlいないようです....ml

誰でも助けてもらえますか？

PROLOG で最初の簡単なコードを書きました。

is_beginning の最初の引数が 2 番目の引数と等しいかどうかを調べるように設計されています。まあ、私見は質問にかなりうまく答えることができますが、定義された2番目の引数に対して可能なすべての答えを得る可能性があるかどうか疑問に思っています。例えば。為に

[]、[a]、[a、b]、[a、b、c]を回答の統合として取得したいのですが、[]しか取得できません(最も簡単な回答)。

私が欲しいものを手に入れる可能性はありますか？多分私の定義に何か問題がありますか？私はすでにfindallとforallを使用しようとしましたが、うまくいきません:(

すべての回答に感謝します。

プロローグで：

B は [_G1091] として表示され、インスタンス化されていない変数であることを示しています。でも、ちょっと変えると・・・

突然、 B がインスタンス化されていないことを私に示すことに興味がありませんが、それでも何かと統合する準備ができている変数です..どうしてですか? （私は時々奇妙な詳細に焦点を当てるのが好きです:)）

これは、Prolog での統合に関する過去の試験の問題です。それらが統合されたかどうか、そしてインスタンス化されたかどうかを言うことになっていました。

これはかなり a = X, g(b,a) = g(Y,X) を統一し、非常に簡単です

h(c,d) は h(W,d) と統合しますが、g(Y) =/ X のためにこれが統合するとは思いません。大文字の X は解決策が見つかるまで検索するため、X = g(Y) である可能性はありますか?

候補句を解決するときに空のセットを取得しようとする解決アルゴリズムを実装したいと考えています。

候補の親句を幅優先の順序で解決するアルゴリズムが必要です。しかし、私はある時点で混乱しました：

S を知識ベースのすべての節とゴール節の否定の結合とする

S の候補句を S の候補句で解決しようとすると、S' が得られます。

アルゴリズムの 2 番目のステップとして、S と S' または S' を S' 自体で解決しようとする必要がありますか? そしてそれはどのように進めるべきですか？

例えば;

知識ベース + 否定を仮定します。ゴールセットの

p(a,b) ^ q(z),~p(z,b) ^ ~q(y) ((この集合を S としましょう)

セット S で解決アルゴリズムを実行すると、次のような節が得られます。

q(a) ^ ~p(z,b) (この集合を S' としましょう)

さて、BFS 戦略を採用しなければならない場合、最初の親が S にあり、2 番目の親が S' にあるリゾルベントを最初に見つける必要がありますか? または、両親が両方ともS'出身の解決者を確認してみてください。

いくつかの例では、最初に S' と S' で解決策を確認すると、解決策が得られます。ただし、セットのペア (S, S') (S, (S, S')) のチェックを続行すると、空の句につながる別の方法が得られます。では、BFS に対応するのはどの順序でしょうか?

前もって感謝します

与えられた Haskell 関数は次のとおりです。

問題は、手で「手動で」タイプを見つける方法です。Haskell にタイプを教えてもらうと、次のようになります。

しかし、次のように定義されている使用済み関数のシグネチャのみを使用して、これがどのように機能するかを理解したいと思います。

編集：非常に多くの非常に優れた説明...最適なものを選択するのは簡単ではありません!

私はすべてのクエリを実行するためにプロローグスクリプトを使用しています、コードは次のようになります：

問題は、queryAll次のような統合結果を見たいときに、「はい」または「いいえ」しか出力されないことです。

プロローグでこれを行う方法は？前もって感謝します。

型付けされていない言語でカスタム型推論言語を使用するプロジェクトの実現可能性を調査しようとしています。(言語自体は重要ではありませんが、たまたま PHP です)。私の最初のアイデアは、これで型の統一を実行することです。私は Haskell で少しプログラミングしたことがあるので、エンドユーザーの観点から型の統一がどのように機能するかは知っていますが、アルゴリズムの詳細を深く掘り下げたことはありません。

この時点で、PHP コード ファイルを解析し、対応する一連のルールを作成して、それらのルールに対して統合アルゴリズムの実行を開始したいと考えています。車輪を再発明するのではなく、既存の統合アルゴリズムを使用することにしました。AFIAK の Prolog は、最も堅牢な統合アルゴリズムの 1 つです。

検証可能な正しい入力を渡すと、Prolog は "true" を返します。正しくないものを渡すと、"false" が返されます。このシナリオで本当に必要なのは、型が統合されなかった理由を示すエラー メッセージを取得することです。SWI-Prolog で「トレース」モードをオンにすると、多かれ少なかれ探しているもの、型が統合されなかった理由の段階的な説明が得られます。私の中心的な質問は、この情報をプログラムで取得することは可能ですか? 私は C 拡張機能を書き、それが必要であれば Prolog コンパイラに直接リンクするつもりです。また、私は SWI-Prolog とは何の関係もありません。Google で最初に見つけたものです。

また、余談ですが、ウェブ形式または実際の本として、プロローグの優れたチュートリアルを知っている人はいますか?

Prologを使用する必要がある学校のプロジェクトがあります。これは私にとってすべて新しいことなので、いくつかの問題があります。

次のようなリストがあります。

作成しなければならないいくつかの述語を通じて、各メンバーに関する入力情報を受け取ることになっています。

そのうちの 1 つは次のタイプです。

また、M1 は M2 または M3 のいずれかであり、両方ではないことが示されています。例えば、

「a」を持つメンバーは、最初のフィールドに 2 または 3 があることを示します。

私は一晩中試してみましたが、解決策が思いつきません。統合を使用する必要があると思いますが、その方法がわかりません。

私はこれを試しました：

これはばかげているように見えるかもしれませんが、私が言ったように、Prolog は私にとってまったく新しいものであり、その機能を完全に把握することはできません。

どんなヒントでも大歓迎です。ありがとう！

編集：

例：

これで、アインシュタインが最初の 3 人のリストができました。

これらは、述語を適用した後に受け入れられる 2 つのリストです。

それは簡単な問題のはずですが、私には理解できません。

ありがとう！

pair/2フォームと述語の一連の定義がありますpropagate/3。

もし私が持っていてList = [pair(1, 2), pair(2, 3), pair(3, 4), pair(4, 5)]、私がするなら

目的の出力が得られますResult = [1, 3]。つまり、 とペアを形成するすべての数値のリストです2。

しかし、私が持っている場合、私が持っているList = [pair(N1, N2), pair(N2, N3), pair(N3, N4), pair(N4, N5)]場合

出力は

代わりに、出力を にしたいと思いますResult = [N1, N3]。どうやってやるの？