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


14 Kanren

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.

14.1 The fact building blocks

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.

14.2 relations

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.

14.3 Queries

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 ...).

14.4 Misc

(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.

14.5 Examples

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: , Previous: , Up: Top   [Index]