Illustrations of logic programming ideoms
Disclaimer. I'm self educated when it comes to logic programming so I might be out on the water a bit, still I prefere to have a nice cool bath then just making sand castles
Ok, step 1 in this discussion is to note a need. I would like to try a logical branch and if it succeeds I want to use the result without the cruft needed to be used to calculate the result. E.g. store the result and backtrack to the beginning. Now if I later conclude that the results was not useful I would like to backtrack and redo the logical branch, back track that branch and calculate a new value. - sounds complex doesn't it.
Why would you like to do this. 1 in the process of calculating a value some other variables gets a binding as a result you would like to undo those settings and only use the conclusion. Also forcing this kind of call to only succeed once means that you can save stack storage.
Let's go to the meat,
(define (call s p cc lam x l)
(let ((s (gp-newframe s)))
((gp-lookup Lam s)
s p (lambda (ss pp)
(let ((state (gp-store-state ss)))
(let ((xx (gp-cp x)))
(let ((ppp (lambda ()
(%with-guile-log% (s ppp cc)
(%=% xx l)))))))))
This shows how this call mechanism is coded in guile-log.
use-logical means that redoing state is fast e.g. it's using the kanren approach to bind values with a translation table in the form of an assoc list, also variables is allocated on the heap. The drawback is that unification can be slow and if there is a lot of variable bindings going on then the assoc can be huge and we can get inferior performance. Because the only needed feature is the allocation of the variables on the heap, there is plenty of options to target this function towards different use-cases. note the argument list. All functions have the first three, s = state and assoc list, p is the failure and cc is the continuation. lam is the logic x is the result probe and l is the output variable where the result (x) should be unified to. As we continue in the function we make a newframe e.q. a point to backtrack to. Lam is a lambda e.g. a function with only the s p and cc argument here we code a special cc. It basically set the state after the calculation of the logic in Lam in the local variable state, then copy the result probe x to xx unwind to the beginning, leave the logical setup and unify xx with the output l and we go to the continuation! Note here how the ppp e.g. the failure lambda send to the continuation just restore the state and issue a backtrack
gp-cp is mapping x by looking up values and put them in the list or leave a variable at the place. Because variables are allocated from the heap they will be ok to use after all links have been backtracked and not be overrun when the continuation kicks in. Note here a quite huge issue. Assume that you have a variable that was alive at the beginning and inside the Lam you do a unification with a newly created variable, as it now is, what points to what is random and no rule is used so the function above is not really sound at the moment you can get a hook onto an old variable or not randomly. What you would like to do is to have a creation number on the variable and when you unify two variables you take the convention to point the newer to the older if not stated directly via a gp-set a form. But lets think away this problem for now and continue to the next step
For this step I would like to take a logic Lam, then a probe X and an output L then I would like to collect all possible answers X in the list L and L should be the result. Here is the code in guile-log
(%define% (collect Lam X L)
(%letg% ((l '()))
(%code% (set! l (cons (gp-cp X S) l)))
(%=% l L)))))
I use % in stead of guile-log's markers and work in a small sub language where I do not keep track of s p cc all the time plus some other feature. So again with logical++ we make sure to use variables on the heap. We create a letg variable l, that will contain the list we build up. the g stands for ... ! well i don't remember. but the semantic is that with it. you can store and retrieve states at will e.g. stop a calculation do something store the state run it again, at another point in time restore the state and run it another time perhaps with some other parameters. It also makes the algorithm slower so if one needs the speed just nuke the g in letg. Anyway we call the logic inside Lam and again make a copy of the probe X and cons it onto the list. When there is no more solutions left the next field in the or is run turning of the kanren (logic--) feature if it was not on from the beginning and unify the the result list to L. You might want to do a reverse of the list here as well.
For step 3 we mold the evaluation by forcing a probe to vary form result to result. We try this with perhaps,
(%define% (%uniq% Lam Y)
(%letg% ((l '()))
(%not% (%member% Y l))
(%code% (set! l (cons (gp-cp YY S) l)))))
We just make sure to keep a list of older probe values and the function will success only when there is a new value that does not unify to any of the elements in the list. note again the use of letg.The last step is to combine all the other steps and do that with,
(%define% (%collect-2% Lam X Y L)
(%call% ((Y YY))
(%uniq% (%/.% (%funcall% Lam X Y)) Y))
(%collect% (%/.% (%funcall% Lam X YY)) X L)))
Here Lam takes two values a probe value X and a by variable Y. %call% is a macro ovwe call above in step 1, where YY is the result and Y is the probe and the %uniq% etc is the Lam. %/.% is just making a closure e.g. a lambda with no arguments apart from standard ones. %var% makes a fresh new variable. The code should produce a list for each unique Y (the by variable) and when backtracking the next list with a new different Y will be made. This semantic is nice but can of cause be optimize for speed.