(index ("run*" 0) ("run" 888) ("succeed" 1248) ("fail" 1371) ("fresh" 1480) ("conde" 1875) ("conda" 2648) ("ifa" 3006) ("condu" 3232) ("ifu" 3569) ("==" 3795) ("=/=" 4168) ("var?" 4404) ("project" 4555) ("onceo" 5933) ("make-tag-A" 6062) ("symbolo" 7138) ("numbero" 7292) ("booleano" 7446) ("charo" 7712) ("atomo" 7865) ("nullo" 8014) ("pairo" 8252) ("listo" 8473) ("build-num" 8701) ("little-endian->number" 8945) ("zeroo" 9152) ("poso" 9446) ("pluso" 9761) ("+o" 9761) ("minuso" 10274) ("-o" 10274) ("*o" 10596) ("/o" 10878) ("<o" 11105) ("<=o" 11105) ("logo" 11305) ("expo" 11532) ("caro" 11796) ("cdro" 11958) ("conso" 12120) ("membero" 12346) ("rembero" 12478) ("appendo" 12641) ("flatteno" 12838) ("lengtho" 13118) ("anyo" 13258) ("nevero" 13360) ("alwayso" 13472) ("distincto" 13551) ("permuteo" 13728))
(def (sig (syntax "(run* (x) goal0 goal ...)" (id run*))) (p "Primary interface operator for miniKanren. " (tt "run*") " instantiates a fresh variable " (tt "x") ", and runs through each subsequent goal provided. It returns a list of all possible unifications of " (tt "x") " where goals " (tt "goal0") ", " (tt "goal") ", and so on succeed.") (p (b "Note") ": As long as there are a finite number of possible values that can be unified with " (tt "x") ", then " (tt "run*") " is guaranteed to terminate. However, this importantly doesn't make two guarantees:") (ol (li "The speed at which the answers will be found. The runtime is generally fast, but miniKanren, and more generally relational and logic programming necessarily requires one to think about the best way to prune the search space of possible answers.") (li "The order of answers in " (tt "x") " that satisfy the goals.")))
(def (sig (syntax "(run n (x) goal0 goal ...)" (id run))) (p "Interface operator for miniKanren. Behaves like " (tt "run*") ", except that it will only provide up to " (tt "n") " possible unifications of " (tt "x") ". This is useful if there are a finite number of solutions and one wants to merely " (i "take") " the first " (tt "n") " possible solutions."))
(def (sig (constant "succeed" (id succeed))) (p "A goal that is always successful. Equivalent to " (tt "(== #f #f)") "."))
(def (sig (constant "fail" (id fail))) (p "A goal that always fails. Equivalent to " (tt "(== #t #f)") "."))
(def (sig (syntax "(fresh (a ...) goal0 goal ...)" (id fresh))) (p "Creates a logic variable bound to each of the symbol(s) " (tt "(a ...)") ". These logic variables are then lexically scoped within this macro, whereupon each of the subsequent goals can be evaluated.") (p "Example:") (highlight scheme "(run* (q)\n  (fresh (a d)\n    (== a 1)\n    (nullo d)\n    (conso a d q)))\n; => ((1))"))
(def (sig (syntax "(conde (goal0 goal ...) (goal0^ goal^ ...) ...)" (id conde))) (p "Conditional performing logical disjunction over each set of " (tt "(goal0 goal ...)") " clauses. The first goal in each clause (i.e. " (tt "goal0") " or " (tt "goal0^") ") is considered the head of that clause. Behaves similarly to " (tt "cond") " in regular Scheme, except that each clause provides one possible path to unification through the subsequent goals.") (p "In the first edition of miniKanren, " (tt "conde") " was separate from " (tt "condi") ", which is no longer provided as part of the language. " (tt "conde") " now interleaves each of the possible clauses on recursive calls, so " (tt "condi") " (which used to stand for interleaving-conditional) is no longer needed."))
(def (sig (syntax "(conda (goal0 goal ...) (goal0^ goal^ ...) ...)" (id conda))) (p "Conditional behaving much like " (tt "conde") ", except that " (tt "conda") " does a soft-cut over the remaining goals. That is to say, if any of the heads of the clauses succeed, then the remaining clauses will all be " (i "cut") " (i.e. ignored) from future searches."))
(def (sig (syntax "(ifa (goal0 goal ...) b ...)" (id ifa))) (p "Single-branch version of " (tt "conda") ". " (tt "ifa") " relates to " (tt "conda") " the way that " (tt "if") " relates to " (tt "cond") " in regular Scheme."))
(def (sig (syntax "(condu (goal0 goal ...) (goal0^ goal^ ...) ...)" (id condu))) (p "Conditional behaving much like " (tt "conde") ", except that " (tt "condu") " performs a " (i "committed choice") ". What that means is that if the head of any goal succeeds, then the remaining goals of that clause will only be run once thereafter."))
(def (sig (syntax "(ifu (goal0 goal ...) b ...)" (id ifu))) (p "Single-branch version of " (tt "condu") ". " (tt "ifu") " relates to " (tt "condu") " the way that " (tt "if") " relates to " (tt "cond") " in regular Scheme."))
(def (sig (procedure "(== u v)" (id ==))) (p "Primary unification goal. " (tt "u") " and " (tt "v") " are either logic variables or values. If the two can be unified (i.e. if the two logic variables hold the same value, or if two values are the same) then this goal succeeds. When used on fresh variables, guarantees that the two logic variables will always be unified."))
(def (sig (procedure "(=/= u v)" (id =/=))) (p "Disequality goal. This goal succeeds if-and-only-if " (tt "u") " and " (tt "v") " are not unified. When used on fresh variables, ensures that " (tt "u") " and " (tt "v") " never unify."))
(def (sig (procedure "(var? v)" (id var?))) (p "Predicate procedure (not a goal) that returns true if-and-only-if " (tt "v") " is a logic variable."))
(def (sig (syntax "(project (x ...) goal0 goal ...)" (id project))) (p "Extracts the value of zero or more logic variables into lexical variables of the same name, and executes the goals within the body of the " (tt "project") " call.") (p "Example:") (highlight scheme ";; The following code will fail because `+` is not relational.\n(run 1 (q)\n  (fresh (a b)\n    (== a 1)\n    (== b 2)\n    (== q (+ a b))))\n\n; => Error: (+) bad argument type - not a number: #(a)\n\n\n;; However, if we use project to get the values of the logic variables,\n;; we can use those directly.\n(run 1 (q)\n  (fresh (a b)\n    (== a 1)\n    (== b 1)\n    (project (a b)\n      (== q (+ a b)))))\n\n; => (3)") (p (tt "project") " can be though of as an escape hatch to break out of miniKanren. It will give you the values of the variables, but it only works if the variables are grounded. In the above example, if the logic variable " (tt "b") " is not ground, then the " (tt "b") " inside the body of " (tt "project") " will not be lexically bound to anything, and will still be a fresh logic variable.") (p "In most cases it is advised to avoid " (tt "project") " when you can. It can be a powerful tool for debugging the values of logic variables when writing miniKanren code; however, excessive use will lead to extremely non-relational code that will be hard to work with in miniKanren."))
(def (sig (procedure "(onceo goal)" (id onceo))) (p "A procedure that ensures that " (tt "goal") " executes exactly one time."))
(def (sig (procedure "(make-tag-A tag pred)" (id make-tag-A))) (p "Constructs a goal that succeeds whenever " (tt "pred") " returns " (tt "#t") " for a single value, and fails if " (tt "pred") " returns " (tt "#f") " for that value. This creates a predicate-goal that tags the logic variable with the tag name " (tt "tag") ".") (p (b "Note") ": This is primarily useful for atomic-type predicates, i.e. predicates for atomic types that do not have explicit constructors. This is what is used to implement " (tt "symbolo") ", for example:") (highlight scheme "(define symbolo (make-tag-A 'sym symbol?))") (p "One should avoid using this for types that have constructors (e.g. pairs have " (tt "cons") ", lists have " (tt "list") "), and should instead prefer creating relational constructors for such types. This egg provides " (tt "symbolo") ", " (tt "numbero") ", " (tt "booleano") ", " (tt "charo") ", and " (tt "atomo") " using this method. However, " (tt "make-tag-A") " is highlighted here in case users have new atomic types that they wish to extend miniKanren with."))
(def (sig (procedure "(symbolo s)" (id symbolo))) (p "A tagged constraint goal that succeeds if-and-only-if " (tt "s") " can be unified with a symbol."))
(def (sig (procedure "(numbero n)" (id numbero))) (p "A tagged constraint goal that succeeds if-and-only-if " (tt "n") " can be unified with a number."))
(def (sig (procedure "(booleano b)" (id booleano))) (p "Predicate goal that succeeds if-and-only-if " (tt "b") " can be unified with a boolean. When " (tt "b") " is fresh, this guarantees that " (tt "b") " can only be unified with " (tt "#t") " or " (tt "#f") "."))
(def (sig (procedure "(charo c)" (id charo))) (p "A tagged constraint goal that succeeds if-and-only-if " (tt "c") " can be unified with a character."))
(def (sig (procedure "(atomo a)" (id atomo))) (p "A tagged constraint goal that succeeds if-and-only-if " (tt "a") " can be unified with an atom."))
(def (sig (procedure "(nullo p)" (id nullo))) (p "Predicate goal that succeeds if-and-only-if " (tt "p") " is the null list. When " (tt "p") " is fresh, it guarantees that " (tt "p") " can only unify with the null list " (tt "'()") "."))
(def (sig (procedure "(pairo p)" (id pairo))) (p "Predicate goal that succeeds if-and-only-if " (tt "p") " unifies with any pair. When " (tt "p") " is fresh, it guarantees that " (tt "p") " can only unify with a pair."))
(def (sig (procedure "(listo l)" (id listo))) (p "Predicate goal that succeeds if-and-only-if " (tt "l") " unifies with any list. When " (tt "l") " is fresh, it guarantees that " (tt "l") " can only unify with a proper list."))
(def (sig (procedure "(build-num n)" (id build-num))) (p "Constructs a bit-list to represent a number given a positive exact number.") (p "Example:") (highlight scheme "(build-num 0) ; => ()\n(build-num 1) ; => (1)\n(build-num 2) ; => (0 1)"))
(def (sig (procedure "(little-endian->number b)" (id little-endian->number))) (p "Procedure that converts a bit-list in little-endian form back into a Scheme number. The opposite of " (tt "build-num") "."))
(def (sig (procedure "(zeroo n)" (id zeroo))) (p "A goal that succeeds if-and-only-if the logic variable " (tt "n") " is zero (i.e. null bit list). When " (tt "n") " is fresh, this guarantees that it can only ever be bound to the null list. This makes it equivalent to " (tt "(nullo n)") "."))
(def (sig (procedure "(poso n)" (id poso))) (p "A goal that succeeds if-and-only-if the logic variable " (tt "n") " is a positive number (i.e. non-null bit list). When " (tt "n") " is fresh, this guarantees that it can only ever be bound to a non-null bit list. This makes it equivalent to " (tt "(listo n)") "."))
(def (sig (procedure "(pluso n m k)" (id pluso)) (procedure "(+o n m k)" (id +o))) (p "A goal that unifies two logic variables " (tt "n") " and " (tt "m") " such that the bit-lists they represent sum to " (tt "k") " when added. Think of this as if you were doing " (tt "(define k (+ n m))") ", except that it is relational.") (p "Example:") (highlight scheme "(run 1 (q)\n  (let ((a (build-num 4))\n        (b (build-num 3)))\n    (fresh (n k)\n      (== k a)\n      (== n b)\n      (pluso n q k))))\n; => (1)"))
(def (sig (procedure "(minuso n m k)" (id minuso)) (procedure "(-o n m k)" (id -o))) (p "A goal that unifies two logic variables " (tt "n") " and " (tt "m") " such that the bit-lists they represent subtract to " (tt "k") ". Think of this as if you were doing " (tt "define k (- n m))") ", except that it is relational."))
(def (sig (procedure "(*o n m p)" (id *o))) (p "A goal that unifies two logic variables " (tt "n") " and " (tt "m") " such that the bit-lists they represent multiply to " (tt "k") ". Think of this as if you were doing " (tt "(define k (* n m))") ", except that it is relational."))
(def (sig (procedure "(/o n m q r)" (id /o))) (p "A goal that unifies two logic variables " (tt "n") " and " (tt "m") " such that the bit-lists they represent divide to the quotient " (tt "q") " with remainder " (tt "r") "."))
(def (sig (procedure "(<o n m)" (id <o)) (procedure "(<=o n m)" (id <=o))) (p "Predicate goals that succeed if-and-only-if " (tt "n") " is less than (or equal to, in the latter case) " (tt "m") "."))
(def (sig (procedure "(logo n b q r)" (id logo))) (p "Goal that unifies two logic variables " (tt "n") " (number) and " (tt "b") " (base) such that they form the logarithm with power " (tt "q") " and remainder " (tt "r") "."))
(def (sig (procedure "(expo b q n)" (id expo))) (p "Goal that unifies the two logic variables " (tt "b") " and " (tt "q") " such that they form the exponential " (tt "n") ". Think of this as doing " (tt "(define n (expt b q))") ", except that it is relational."))
(def (sig (procedure "(caro p a)" (id caro))) (p "Goal that unifies a logic variable representing a pair " (tt "p") " with the car of that pair, " (tt "a") "."))
(def (sig (procedure "(cdro p d)" (id cdro))) (p "Goal that unifies a logic variable representing a pair " (tt "p") " with the cdr of that pair, " (tt "d") "."))
(def (sig (procedure "(conso a d p)" (id conso))) (p "Goal that unifies two logic variables " (tt "a") " and " (tt "d") ", representing the car and cdr of a pair, with the logic variable representing the pair " (tt "p") "."))
(def (sig (procedure "(membero x l)" (id membero))) (p "Goal that unifies " (tt "x") " with any member of the list " (tt "l") "."))
(def (sig (procedure "(rembero x l out)" (id rembero))) (p "Goal that unifies " (tt "out") " with a list where " (tt "x") " has been removed from " (tt "l") "."))
(def (sig (procedure "(appendo l s out)" (id appendo))) (p "Goal that unifies two lists " (tt "l") " and " (tt "s") " with a list " (tt "out") ", which is the two lists appended to one another."))
(def (sig (procedure "(flatteno s out)" (id flatteno))) (p "Goal that unifies a list " (tt "s") " with " (tt "out") ", where " (tt "out") " represents a list with the same elements of " (tt "s") ", except that " (tt "out") " is flattened (i.e. only contains atoms, not pairs)."))
(def (sig (procedure "(lengtho s n)" (id lengtho))) (p "Goal that unifies a list " (tt "s") " with the length of that list " (tt "k") "."))
(def (sig (procedure "(anyo goal)" (id anyo))) (p "Goal that succeeds if " (tt "goal") " succeeds."))
(def (sig (constant "nevero" (id nevero))) (p "Goal that always fails. Equivalent to " (tt "(anyo fail)") "."))
(def (sig (constant "alwayso" (id alwayso))) (p "Goal that always succeeds."))
(def (sig (procedure "(distincto s)" (id distincto))) (p "Goal that guarantees that no element of the list " (tt "s") " will ever unify with another element of " (tt "s") "."))
(def (sig (procedure "(permuteo xl yl)" (id permuteo))) (p "Goal that permutes " (tt "xl") " into " (tt "yl") ". It may not terminate if " (tt "xl") " is not ground.") (p "Example:") (highlight scheme ";; Get 5-permute-2, i.e. all 2 permutations of the numbers 1 through 5.\n(run* (q)\n  (lengtho q (build-num 2))\n  (permuteo '(1 2 3 4 5) q))\n\n; => (1 2) (2 1) (2 3) (1 3) (3 1) (3 2) (3 4) (2 4) (1 4) (4 1) (4 2)\n;    (4 3) (3 5) (4 5) (2 5) (1 5) (5 1) (5 2) (5 3) (5 4))"))
