問題タブ [minikanren]

これは矛盾です：

同時にあるaqはtrueあり得ないからです。false

これも矛盾ではないでしょうか。

:-それが何を意味するのかわかりません。しかし、マップキーは一意である:kためtrue、false. 2 番目の目標が一致しないようにするにはどうすればよいですか?

もう一つの例

私はこれを次のように解釈しています。

• x:kは、 asを持つマップのようなものfalseです。
• qですtrue。
• qの値:kですx

私は正確に何をしようとしていますか?

私はfeaturec次のような目標を作成するために使用しようとしています:

それから私は言うことができるようにしたいです:

論理プログラミングについて読みたいとき、私はいつもそれを行うための 2 つの「主な」方法に出くわします。

• miniKanrenはThe Reasoned Schemer で導入されたミニ言語であり、 core.logicにより現在人気があります。
• Prolog、最初の「大きな」ロジック プログラミング言語。

私が今興味を持っていること: 2 つの主な技術的な違いは何ですか? それらはアプローチと実装が非常に似ていますか、それとも論理プログラミングに対してまったく異なるアプローチをとっていますか? それらは数学のどの分野から来ており、理論的基礎は何ですか?

最近は、Neo4j のようなグラフ データベースと、Prolog と miniKanren のロジック プログラミングについて調べています。私がこれまでに学んだことから、どちらも事実とそれらの間の関係を指定することができ、結果のシステムにいくつかの選択を照会することもできます。したがって、実際には、どちらもグラフの作成とクエリに使用できますが、異なる構文を使用するという点で、それらの間に大きな違いはありません。ただし、それらはまったく異なる種類のソフトウェアとして提示されます。

データベースがより時空間的に効果的なストレージ技術を提案する可能性があるという技術的なことと、miniKanren のような小さなロジック コアがよりシンプルで埋め込み可能であることを除いて、グラフ データベースとロジック プログラミング言語の実際の違いは何ですか。 + クエリ API?

演習 (またはエントリ?) 57 では、ロジックがどのように流れるかを理解していません。問題は、次のことです。

ここで、'=' は実際には三重棒の統合 (?) 演算子です。以下を実行します。

本は答えを与えます：

私は答えが次のようになると思っていたでしょう：

私の推論は、(teacupo x) の 'x' は、最初にすべてのソリューションを通過し、すべてのソリューションのリストに統合する必要があるということです。しかし、teacupo は一度に 1 つのソリューションしか放棄しないようです。conde の私の解釈では、それが与える規則を使用すると、conde の行を調べて、行が成功した後、失敗したふりをして、変数を更新し、成功する次の行を見つける必要があるため、混乱します。解決策が機能する方法を考えると、そのコードのコンデは成功した行に戻り、茶碗コンデを強制的に失敗させ、次の可能な値をあきらめるように見えます。繰り返しになりますが、teacupo ソリューションはリスト内のすべてのコンデ ソリューションを放棄し、外側のコンデ コールに進むと考えていました。

完全宣言型ホーン ロジック(または完全宣言型プロローグ)と呼ばれるもので、いくつかの知識を形式化し、クエリを実行したいと考えています。誰かがそれを実装する方法に関するガイドラインを提供できますか? 上記のリンクからの詳細な説明を簡単に要約します。

正式な言語は、Prolog (のコア) のものです。「プログラム」は、Prolog と同様に、規則と事実のセットです (関数と変数を含み、基本的にはユーザー定義の述語のみを含みます)。

ただし、Prolog とは対照的に、論理プログラムの標準的な宣言的セマンティクスに関して健全で完全な実装、つまり最小の Herbrand モデル (帰納的に定義された基本用語のセット) を探しています。論理プログラミングの理論的研究では、これは通常研究の対象であり、たとえば、次の条件:

• マッチング ルールの公平な検索 (たとえば、Prolog の深さ優先検索は公平ではありません)。
• "発生チェック" による統一 (変数が統一された項に出現しないことを確認する)。

車輪を発明するのではなく、既存の機能に基づいて構築される簡潔な実装を探しています。私が見ているより有望な方向性の 2 つは、Prolog のメタインタープリターとして、または何らかの定理証明の一部として実装することです。これらの分野で実際的な知識を持っている人は、それを実装する方法に関するガイドラインを提供できますか? miniKanrenで簡単に実装できますか?

私の意図は、一部の知識を完全に宣言的な方法で形式化することです。このような形式化の重要な特徴は、それが (単調な) 帰納法の数学的概念に正確に対応しているため、知識とその特性を帰納的な議論で簡単に推論できることです。

...どうすれば回避できますか?

戻り値

_0これは、マップには少なくとも:a 1キーと値のペアとキーと値のペアが含まれている必要があることを意味すると理解してい:a 2ます。MultiMaps を使用しない限り、と:aの両方にマップできないため、これは矛盾しているように見えます。指定した制約が結合であるため、ORとして読み取ることはできません。制約が矛盾しているため、結果は次のようになるはずだと想像したでしょう。これらの制約を満たすことができる値はありません。12:a 1:a 2()q

結果を間違って読んでいるに違いありません。