ミニカンレン

miniKanren は、Will Byrd によって最初に開発された関係プログラミング用のプログラミング言語のファミリーです。 ^{[ 1 ]}関係は双方向であるため、miniKanren に式と目的の出力が与えられると、miniKanren は式を「逆方向」に実行して、目的の出力を生成する式へのすべての可能な入力を見つけることができます。この双方向の動作により、ユーザーはプログラムへの入力とプログラムの結果の両方を同時に制約できます。miniKanren はインターリーブ検索を実行し、検索ツリーのいずれかのブランチが無限に長く、解が含まれていない場合でも、存在するすべての解を最終的に見つけます。解が存在しない場合、検索ツリーが無限であれば miniKanren は永遠に検索する可能性があります。

miniKanren コードの例としてevalo、式をその評価結果の値に関連付ける関係目標があります。evalominiKanren で次のように が呼び出されると、 quines、つまり実行時にそれ自身に評価される式が(evalo q q)生成されます。^{[ 2 ]}q

書籍『The Reasoned Schemer』では、関係プログラミングを実演するために miniKanren を使用し、Schemeで完全な実装を提供しています。^{[ 3 ]}言語の中核は印刷された 2 ページに収まります。miniKanren の Scheme 実装は、理解しやすく、変更しやすく、拡張しやすいように設計されています。

microKanrenはminiKanrenファミリーの別の言語で、Schemeで40行未満という最小限の実装で知られています。^{[ 4 ]}

αleanTAP は、名目論理のための miniKanren の拡張である αKanren で書かれたプログラムです。定理が与えられると、証明を見つけることができるため、定理証明器となります。証明が与えられると、定理を見つけることができるため、定理チェッカーとなります。証明の一部と定理の一部が与えられると、証明と定理の欠落部分を補完するため、定理探索器となります。^{[ 1 ]}

miniKanrenは、 Clojure、Dart、Haskell、JavaScript、Python、Racket、Ruby、Scala、Swiftで実装されています。最も代表的な実装は、 Schemeに組み込まれた言語です。Clojureのcore.logicライブラリは、miniKanrenに触発されて開発されました。

kanrenという名前は、 「関係」を意味する日本語の「関連」に由来しています。

• 論理プログラミング
• ツリー走査

• 公式サイト