Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
miniKanren
open-in-new
<p>miniKanren is a family of <a href="/facts/Programming_language/cWTYbgWa">programming languages</a> for <a href="/facts/Relational_programming/Xgh8lj3F">relational programming</a>. As <a href="/facts/Binary_relation/r9BwGgaK">relations are bidirectional</a>, if miniKanren is given an <a href="/facts/Expression_(computer_science)/eRlhoBeN">expression</a> and a desired output, miniKanren can run the expression "backward", finding all possible inputs to the expression that produce the desired output. This bidirectional behavior allows the user to constrain both the input to the program and the result of the program simultaneously. miniKanren performs an interleaved search which will eventually find any solution that exists, even if any one branch of the search tree is infinitely long and contains no solutions. If no solution exists, miniKanren may search forever if the search tree is infinite. </p><p>An example of miniKanren code is evalo, a relational goal that relates expressions to the values that they evaluate to. When evalo is called in miniKanren like so: (evalo q q), it will generate <a href="/facts/Quine_(computing)/noybHw3h">quines</a>, that is, expressions q that when run will evaluate to themselves. </p><p>The book <i>The Reasoned Schemer</i> uses miniKanren to demonstrate relational programming, and provides a complete implementation in <a href="/facts/Scheme_(programming_language)/0aGdf3SC">Scheme</a>. The core of the language fits on two printed pages. The Scheme implementation of miniKanren is designed to be easily understood, modified, and extended. </p><p>αleanTAP is a program written in αKanren, an extension of miniKanren for nominal logic. Given a theorem, it can find a proof, making it a <a href="/facts/Automated_theorem_proving/vKGvuKFI">theorem-prover</a>. Given a proof, it can find the theorem, making it a theorem-checker. Given part of a proof and part of a theorem, it will fill in the missing parts of the proof and the theorem, making it a theorem-explorer. </p><p>There are implementations of miniKanren in <a href="/facts/Haskell_(programming_language)/4Htv9WLu">Haskell</a>, <a href="/facts/Racket_(programming_language)/5n7LW08b">Racket</a>, <a href="/facts/Ruby_(programming_language)/BeYSaPSR">Ruby</a>, <a href="/facts/Clojure/3JRNxKXx">Clojure</a>, <a href="/facts/JavaScript/XhhIIEsl">JavaScript</a>, <a href="/facts/Scala_(programming_language)/ebL8o6AK">Scala</a>, <a href="/facts/Swift_(programming_language)/A7qHQC32">Swift</a>, <a href="/facts/Dart_(programming_language)/xJ8tE6Tl">Dart</a> and <a href="/facts/Python_(programming_language)/YbuGqofa">Python</a>. The canonical implementation is an embedded language in <a href="/facts/Scheme_(programming_language)/0aGdf3SC">Scheme</a>. The Clojure core.logic library was inspired by miniKanren. </p><p>The name <i>kanren</i> comes from a Japanese word (関連) meaning "relation". </p>