We will discuss here a kanren version that will modify just partial results and not redo the whole datastructure in order change an underlying value. This means that we are considering paralell executions of code that only modify the data relevant to their code section the solution is a combination of functional programming and using mutating datastructures. This code can be gotten from the logic directory in the guile-log distrubution (see the link on the right of the blog)
We are usign a guile-2.0 scheme. But you might be able to compile it on any scheme, what we need is:
(use-modules (ice-9 match))
(use-modules (ice-9 pretty-print))
In all data we will have atoms cons cells and fail thunks, letts pretty print all but the fail thunks that is procedures, so this is natural
(define (pretty x)
(pretty-print
(let lp ( (x x))
(match x
((x . l)
(if (procedure? x)
(lp l)
(cons (lp x) (lp l))))
(x x)))))
Let get into kanren basics. A predicate is constructed essentially as (predicate x ...) but will produce a lambda of the form (lambda (s p cc) code ...). Here s is the current bindings. p is a thunk that if executed e.g. prompt> (p), will backtrack to the previous junction point. cc is the continuation which will continue the analysis and typically you end your program in tail position to evaluate cc e.g. prompt> (cc s p) where the s should be the current bindings and p the current fail thunk at the tail call. No you can pass extra information to the next step of the logic program and we can do this by calling cc as prompt> (cc s p data) which assumes that the next step in the logic program can catch this. We will use this in this example code.
;; to link goals goal1, goal2, ... to execute after each other we use
;; (any goal1 goal2 ...) e.g.
(define (all . x)
(lambda (s p cc)
(match x
(() (cc s p))
((f) (f s p cc))
((f . l) (f s p (lambda (ss pp) ((apply all l) ss pp cc)))))))
Another possibility is to construct a junction point use
;; (any goal1 goal2 ...) will first try goal1, if that fails then goal2 etc.
(define (any . x)
(lambda (s p cc)
(match x
(() (p))
((f) (f s p cc))
((f . l) (f s (lambda () ((apply any l) s p cc)) cc)))))
We define som lower level utilities:
(define-syntax-rule (aif it p x y) (let ((it p)) (if it x y)))
(define (get-s x) (x))
(define (mk-v data)
(define vf
(case-lambda
(() data)
((x) (set! data x))))
(set-procedure-property! vf 'vf #t)
vf)
Now we are at the meat of our extra utilities. we will compute paralell branches of bindings, and we simply combine branches to one branch by making a vector of the different binding branches and start a new branch with that combination. When we lookup a variable and find such a branch we first see if we ben here before, If so we skip the state and continue with the rest of the search. Else we open up teh combining of branches and look in each of them in order depth wise. Here is the details:
(define (lookup state var)
(define bin (make-hash-table))
(define (bin-here? state)
(aif here? (hashq-ref bin state #f)
here?
(begin
(hashq-set! bin state #t)
#f)))
;; the last continuation returns var
(let lp ((state state) (cont (lambda () var)))
(match state
;;This is a combination of other branches
((and states #(y ...))
(if (bin-here? states)
(cont)
(let lp2 ((y y))
(match y
((s . sl)
(lp s (lambda () (lp2 sl))))
(()
(cont))))))
;; Normal lookup line
(((v . y) . l)
(if (eq? var v)
(if (var? y)
(lookup s y)
y)
(lp l cont)))
;; At end of the list we continue with a new branch or return 'var'
(()
(cont)))))
;; this generate fresh logical variables that can be bouded by values
;; and backtrack
(define-syntax-rule (fresh (v ...) f ...)
(let ((v (make-variable #f)) ...)
(all f ...)))
We need a few standard constructions as well in order to be able to generate somewhat interesting programs. It is a nice show how the functionality works the first one is interesting because it shows how to catch code that throws a value to the continuation (done by return below).
;; (values (((a ...) f) ...) fn ...)
;; executes f ... and catches the return value as is in (a ...)... the an
;; (all fn ...) is executed with those bindings in action.
(define-syntax values
(syntax-rules ()
((_ () code ...)
(all code ...))
((_ (((v ...) f) . l) code ...)
(lambda (s p cc)
(f s p (lambda (ss pp v ...)
((values l code ...) ss pp cc)))))))
;; bind variable x to value y, be careful (bind x x) will creat inf. loops
(define (bind x y) (lambda (s p cc) (cc (cons (cons x y) s) p)))
;; somtimes we want to mar truth, just execute the `cc`
(define true (lambda (s p cc) (cc s p)))
;; and false, probe the fail thunk `p` and execute it
(define false (lambda (s p cc) (p)))
;; And the pearl of logic programming. Unification. Lets do it
;; in the other primitives
(define (== x y)
(match (cons x y)
(((x1 . y1) . (x2 . y2))
(all
(== x1 x2)
(== y1 y2)))
((#(a ...) . #(b ...))
(== a b))
(_
(if (variable? x)
(bind x y)
(if (variable? y)
(bind y x)
(if (eqv? x y)
true
false))))))
;; succeeds when x is true
(define (k-when x)
(lambda (s p cc)
(if x (cc s p) (p))))
;; Avoid infinite recursion
(define (wrap f) (lambda x (apply f x)))
;; repeat f infinite many times
(define (repeat f)
(any f (wrap (repeat f))))
Now over to the new stuff with this code that deviates from normal kanren. We want to introduce mane paralell goals that will not interfere with the normal execution of kanren. These goals could, if expensive, be done in different threads, but for now we want to use it in paralell because they simply represent parts of code that we can backtrack to independently. E.g. if we backtrack to one branch we do not need to update any other branch. Here we go
;; (sv-value sv vv f) this will execute goal f that reurns one value this
;; is put in vv, which is a mutating container. The
;; resulting bindings will be captured and put in
;; container sv.
(define (sv-value sv vv f)
(lambda (s p cc)
(f s p (lambda (ss pp x)
(vv x)
(sv s)
(cc ss pp)))))
;; We will create a set of paralell bindings s ... and put them in the
;; container data-s for use to put on a new binding list,
;; the values v ... will be put in the container data uset for returning
;; a combined value then all code ... is executed in an (all code ...)
(define-syntax-rule (fresh-sv (data-s data : (s v) ...) code ...)
(let ((v (mk-v #f)) ...
(s (mk-v #f)) ...)
(let ((data-s (vector s ...))
(data (list 'data v ...)))
(all code ...))))
;; Implementation detail, wrap a single binding
(define (wrap-s s)
(list (vector (mk-v s))))
;; Modify the bindings s
(define (with-s ss)
(lambda (s p cc) (cc ss p)))
;; Return a value includeing the faili thunk
(define (return-p tag . l)
(lambda (s p cc)
(cc s p (cons* tag p l))))
;; (all-paralell s-data data code ...)
;; The intention is to execute all goals code ... in paralell.
;; s-data will be the resulting if any of the goals fail the whole
;; combined goal fails and backtracking is indecided whch means that
;; we will skip all the paralell goals in that case. The intentoin is
;; that in order to backtrack to a subgoal we need to capture their
;; fail thunk and execute that.
(define (all-paralell s-comb comb . l)
(lambda (s p cc)
(let ((ss (wrap-s s)))
(letrec ((cc2 (lambda (s p x)
((all
(with-s s-comb)
(apply return-p comb))
s p cc))))
((all-paralell0 cc2 l)
ss p cc2)))))
;; we will start all goals with the same s and the same p
;; also we will make sure that the second time we leave the
;; a subgoal we will enter the wrap up of the whole construct
;; in order to not enter another subgial again e.g. just backtrack
;; one single subgoal.
(define (all-paralell0 cend l)
(lambda (s p cc)
(match l
(() (cc s p))
((f) (f s p cc))
((f . l)
(letrec ((cc2 (lambda (s2 p2)
(set! cc2 cend)
((all-paralell0 cend l)
s p cc))))
(f s p cc2))))))
Presenting kanren data in readable form is done via repr and scm. In repr we represent the variables as v.1,v.2,..... n scm we simply leave the variable object as is.
(define (repr0 repr-var s data )
(match data
((x . l)
(cons (repr0 repr-var s x) (repr0 repr-var s l)))
(#(a ...)
(apply vector (repr0 repr-var s a)))
(a
(if (variable? a)
(lookup s a)
(if (procedure? a)
(if (procedure-property a 'vf)
(repr0 repr-var s (a))
a)
a)))))
(define (repr s data)
(define vmap (make-hash-table))
(define i 0)
(define (repr-var v)
(aif before? (hashq-ref vmap v #f)
before?
(let ((ret (string->symbol (format #f "v.~a" i))))
(set! i (+ i 1))
(hashq-set! vmap v ret)
ret)))
(repr0 repr-var s data))
(define (scm s data)
(repr0 (lambda (v) v) s data))
Finally we would like to return controll to the shell for data exploration. So wen we retrun control to the shell we put continuation information into the *env* variable and then we can use that to continue. Here is the API,
(define *env* #f)
;; Print format string with data ... and store data in the *env* as well
;; as continuation information
(define (ask string . data)
(repeat
(lambda (s p cc)
(apply format #t string (repr s data))
(set! *env* (list s p data cc)))))
;; show the daya again
(define show
(case-lambda
(()
(match *env*
((s p data . _)
(format #t "Returned Data:~%")
(pretty (repr s data))))
(if #f #f))
((data)
(match *env*
((s p . _)
(format #t "Returned Data:~%")
(pretty (repr s data))
(if #f #f))))))
;; get the data
(define (data)
(match *env*
((s p data . _)
data)))
;; continue a stall with data l ... to the continuation
(define (continue . l)
(match *env*
(( s p data cc)
(apply cc s p l))))
;; continue with the data but with f in stead
(define (continue-f f . l)
(match *env*
((s p data cc)
(apply f s p cc l))))
;; run a goal f
(define (run f) (f '() (lambda () #f)
(lambda (s p x)
(pretty (repr s x))
(set! *env* (list s p x))
(if #f #f))))
;; backtrack the stall point
(define (next)
(match *env*
((s p . _)
(p))))
;; get the path l ... = i1,i2,.... tree lookup in datastructure
;; ignoring the tag id and fail thunk, starting with index 1
(define (get . l)
(match *env*
((_ _ data . _)
(let lp ((data data) (l l))
(match l
((i . l)
(lp ((list-ref data (+ 1 i))) l))
(()
data))))))
;; bcktrack fail thunk at path l = i1 i2 i3 ...
(define (back . l)
((list-ref (apply get l) 1)))
Now over to a little geometric example. It's kind of stupid in that no prolog variables is defined and hence this logic can be generated with less fuss e.g. no need of variable bindings at all. Any way enjoy
;;;; EXAMPLE A LITTLE GEOMTRY CONSTRUCTOR
;; note that ask will return a value via the continuation cc from the user
(define (make-value x)
(any
(return-p 'value x)
(values (((x) (ask "continue with new value x=~a~%" x)))
(make-value x))))
;; Note how we define the paralell construct and use backtracking
;; and recursion
(define (make-point x y)
(any
(fresh-sv (s-point point : (sx vx) (sy vy))
(all-paralell s-point point
(sv-value sx vx (make-value x))
(sv-value sy vy (make-value y))))
(values (((x y) (ask "continue with new point '(x=~a y=~a)~%" x y)))
(make-point x y))))
;; the rest is repetition of what we learned
(define (make-link x1 y1 x2 y2)
(all
(k-when (or (not (= x1 x2)) (not (= y1 y2))))
(any
(fresh-sv (s-link link : (s-vp1 vp1) (s-vp2 vp2))
(all-paralell s-link link
(sv-value s-vp1 vp1 (make-point x1 y1))
(sv-value s-vp2 vp2 (make-point x2 y2))))
(values (((x1 y1 x2 y2)
(ask "continue with new link '(x1=~a y1=~a x2=~a y2=~a)~%"
x1 y1 x2 y2)))
(make-link x1 y1 x2 y2)))))
(define (make-rectangle xmin ymin xmax ymax)
(all
(k-when (and (< xmin xmax) (< ymin ymax)))
(any
(fresh-sv (s-rectangle rectangle : (s-vp1 vp1) (s-vp2 vp2))
(all-paralell s-rectangle rectangle
(sv-value s-vp1 vp1 (make-point xmin ymin))
(sv-value s-vp2 vp2 (make-point xmax ymax))))
(values (((xmin ymin xmax ymax)
(ask "continue with new rectangle '(xmin=~a ymin=~a xmax=~a ymax=~a)~%" xmin ymin xmax ymax)))
(make-rectangle xmin ymin xmax ymax)))))
And a session can look like
scheme@(guile-user)> (run (make-rectangle 1 2 3 4))
(rectangle
(point (value 1) (value 2))
(point (value 3) (value 4)))
scheme@(guile-user)> (back 2)
continue with new point '(x=3 y=4)
scheme@(guile-user)> (continue 2 3)
(rectangle
(point (value 1) (value 2))
(point (value 2) (value 3)))
scheme@(guile-user)> (back 2 2)
continue with new value x=2
scheme@(guile-user)> (continue 5)
(rectangle
(point (value 1) (value 2))
(point (value 2) (value 5)))
scheme@(guile-user)>