Next: minikanren, Previous: inheritance, Up: Top [Index]

Almost all of the kanren interface is implemented ontop of guile-log to use it import `logic guile-log kanren`

. One could say that the kanren interface is the functional sister to guile-log which is more a macro framework as such guile-log is about 2x faster the kanren, but kanren has more beutifull semantics.
E.g. the kanren operation maps function arguments to functions. The kanren interface is divided into two categories of functionals, facts and relations. One combine facts into relations. The main difference is that fact functions have standardized arguments and relations have customized arguments. Also conversely evaluating the relation will return back a fact.

`succed`

, This functional item repressents a term that always succeeds.

`fail,sfail`

, Both of these will always fail.

`(all f ...)`

, `all`

will produce a functional item representing success if all `f ...`

will success.

`(all! f ...)`

, `all!`

will produce only one success where all `f ...`

successes.

`(all!! f ...)`

, `all!!`

sucesses where all `f ...`

successes only one time.

`(all-interleave f ...)`

, As with `all`

, this construct sucesses if all of the parts sucesses, but the backtracking is designed so that it backtracks evenly and hence avoids problems due to some of the constructs can backtrack an infinite amount of times berfore the success is found. To note is also that this construct has exponential memory complexity with the depth of the search.

`(any f ...)`

, this will success if any of `f ...`

sucesses.

`(any-interleave f ...)`

, as `any`

, but one at a time will be tried cyclically and hence will find a solution in finite time if there exists one, else it could risk getting stuck in an infinite bacltracking sequence.

`(any-union f ...)`

This is similar to `any-interleave`

, but it will
skipp multiples of similar sucesses e.g. if `(all f1 f2)`

is a success, it will skipp the f1 and continue trying with the `f2`

which will success. Esentially this capture the case when all `f ...`

bind the same variable to a value and we do not backtrack to the same value multiple times.

`(if-only pred x), (if-only pred x y)`

, The first form is equivalent to `(all (all! pred) x)`

. For the second form if `pred`

successes then the form will fail if `x`

fails. If `pred`

first fails, then `y`

is executed.

`(if-some p x), (if-some p x y)`

, The first form is equivalent to `(all p x)`

and in the second form `y`

is executed if `p`

fails.

`(succeeds f ...)`

, is similar to `(all f ...)`

but if this success it will backtrack and undo any bindings and continue.

`(fails f ...)`

, if `(all f ...)`

fails then this form will backtrack and undo any bindings and continue with a success.

`(== a b)`

, unifies the terms.

`(*equal? a b)`

, this will try to unify without any variable binding.

`(let-lv (id ...) code)`

, this will bind `id ...`

to new fresh variables inside `code`

.

`(project (var ...) gl)`

, This will take a specification of a functional item represeting a fact, gl and use the lookuped values of `var ...`

inside the `gl`

spec. This logic is captured in a new functinal fact. If the lookup results in a variable an error will be produced.

`(project/no-check (var ...) gl)`

, As with project, but there is no error reported if the lookup results in a variable.

`(predicate scheme-expr code)`

, Succeeds if `scheme-expr`

is true.

`(var? x)`

, true if x is a logical variable.

`(reify x)`

, will produce a scheme representation of `x`

.

`_`

, produces a fress new logical variable in it’s place.

This is documentation derived from the kanren sources.

`(relation (VAR ...) (to-show TERM ...) [GL]`

, Defines a relation of arity `(length '(TERM ...))`

with an optional body `GL. VAR ...`

are logical variables that are local to the relation, i.e., appear in `TERM ...`

or `GL`

. It’s better to list as `VAR ...`

only logical variables that appear in `TERM ...`

. Variables that appear only in `GL`

should be introduced with exists. That makes their existential quantification clearer. Variables that appear in `TERM ...`

are universally quantified.

`(relation (head-let TERM ...) [GL])`

A simpler, and more efficient kind of relation. The simplicity comes from a simpler pattern at the head of the relation. The pattern must be linear and shallow with respect to introduced variables. The gl is optional (although omitting it doesn’t make much sense in practice) There are two kinds of head-terms. One kind is an identifier. This identifier is taken to be a logical identifier, to be unified with the corresponding actual argument. Each logical identifier must occur exactly once. Another kind of a head-terms is anything else. That anything else may be a constant, a scheme variable, or a complex term that may even include logical variables such as `_`

– but not logical variables defined in the same head-let pattern. To make the task of distinguishing logical identifiers
from anything else easier, we require that anything else of a sort of a manifest constant be explicitly quoted or quasiquoted. It would be OK to add ‘, to each ’anything else’ term.

Examples:

`(relation-head-let (x y z) (foo x y z))`

Here `x`

`y`

and `z`

are logical variables.

`(relation-head-let (x y '7) (foo x y))`

Here we used a manifest constant that must be quoted

`(relation-head-let (x y `(1 2 . ,_)) (foo x y))`

We used a quasi-quoted constant with an anonymous variable.

`relation (ANNOT-VAR ...) (to-show TERM ...) [GL]`

where `ANNOT-VAR`

is either a simple `VAR`

or `(once VAR)`

where ’once’ is a distingushed symbol. The latter form introduces a once-var, aka linear variable. A linear variable appears only once in `TERM ...`

and only at the top level (that is, one and only one `TERM`

in the to-show pattern contains `ONCE-VAR`

, and that term is `ONCE-VAR`

itself). In addition, `ONCE-VAR`

must appear at most once in the body `GL`

. (Of course, then `ONCE-VAR`

could be _, instead.) If these conditions are satisfied, we can replace a logical variable `ONCE-VAR`

with a regular Scheme variable.

`(fact (VAR ...) TERM ...)`

, this is syntactic sugar for `(relation (VAR ...) (to-show TERM ...) succeed)`

.

`(extend-relation (id ...) rel ...)`

, this relation will simply try each
sub relation `rel`

one at a time acording to `any`

calling them with arguments (id ...) which is the arguments of the resulting relation.

Example:

(extend-relation (a1 a2) (fact () 'sam 'rob) (fact () 'roz 'sue) (fact () 'rob 'sal))

Here `a1`

and `a2`

will be tried with one fact after the other until a match is found. At backtracking this process will continue untill another match is found.

`(extend-relation-with-recur-limit limit (id ...) rel ...)`

, this is the same as the previous term, but the resulting relation cannot be called recursively more then `limit`

times.

`(lift-to-relations (id ...) (g rel ...))`

, This will generate a
combination of the relation `rel ...`

according to `g`

and with the argument
variables `id ...`

. E.g.

Example:

(lift-to-relations (a1 b1) (any (fact () 'sam 'rob) (fact () 'roz 'sue) (fact () 'rob 'sal)))

Is equivalent to the previous example in the section for `extend-relation`

.

`(intersect-relation (id ...) rel ...)`

, This is the same as extend-relation, but it will use `all`

in stead of `any`

.

`(let-gls (id ...) ((name rel) ...) code)`

, this will create a new realation with arguments `id ...`

and in that create a set af relations names `name ...`

representing `rel ...`

and the names are used in `code`

.

`query (redo-k subst id ...) A SE ...) -> result or '()`

, The low level macro ’query’ runs the goal `A`

in the empty initial substitution, and reifies the resulting answer: the substitution and the redo-continuation bound to fresh variables with the names supplied by the user e.g. `redo-k`

and `subst`

. The substitution and the redo continuation can then be used by Scheme expressions `SE ...`

Before running the goal, the macro creates logical variables `id ...`

for use in `A`

and `SE ...`

If the goal fails, ’() is returned and `SE ...`

are not evaluated. Note the similarity with shift/reset-based programming where the immediate return signifies "failure" and the invocation of the continuation a "success" Returning ’() on failure makes it easy to create the list of answers.

`(solve n (v ...) g ...)`

, This will create fresh new variables `v ...`

and solve `(all g ...)`

. It will output a list of solution which depends on the value of `n`

. If this is equal to `*`

then all solutions will be included. Else if n is a number at must that number of solutions will be publishied in the list.

`(solution (v ...) g ...`

, This is the same as `(solve 1 (v ...) g ...)`

.

`(trace-vars title (var ...))`

, Will print out a trace expression for `var ...`

.

`partially-eval-sgl`

, not implemented, because guile-log is also directed towards stacks and assq lists and hence usually uses another kind of implementation for the interleaving constructs.

Example 1, any-union, (let* ((fact1 (fact () 'x1 'y1)) (fact2 (fact () 'x2 'y2)) (fact3 (fact () 'x3 'y3)) (fact4 (fact () 'x4 'y4)) ; R1 and R2 are overlapping (R1 (extend-relation (a1 a2) fact1 fact2)) (R2 (extend-relation (a1 a2) fact1 fact3)) ; R1 will first try fact1 then fact2 ; R2 will first try fact1 then fact3, hence overlapping ) (solve 10 (x y) (any-union (R1 x y) (R2 x y)))) => '((x1 y1) (x2 y2) (x3 y3))) Note how R1 and R2 first both bind x and y to the same values in their first match and how any-union avoid duplicate the results. This works independent of the orders of fact1 and fact2 etc in the definitions of R1 and R2.

Next: minikanren, Previous: inheritance, Up: Top [Index]