Hi Brett! I don't recall if I've used `riffleo` before, but I agree that it looks useful!
We may have used something similar in this code: https://github.com/webyrd/linear-logic-multiset-rewriting What are other examples of uses of `riffleo` that you have encountered? Cheers, --Will On Mon, Oct 24, 2022 at 12:35 PM Brett Schreiber <[email protected]> wrote: > Hello all, > I have become very interested in relational programming, and I have > enjoyed trying to a variety of search problems in miniKanren. I have found > a relation that has been useful to many of these problems. > > Consider the relation a * b = o where: > > 1. a is a list > 2. b is another list, and > 3. o is the result of nondeterministically merging the lists, i.e., (a > * b) > > It reminds me of the "riffle" step when shuffling a deck of cards. > Here is an example: > > a = '( a b c d e f) > b = '(1 2 3 4 5 6 7 8 ) > o = '(1 2 a 3 b c 4 5 d 6 e 7 8 f) > > Some properties: > > - a * (b * c) = (a * b) * c > - |a * b| = |a| + |b| > - (a * b) contains a and b as subsequences > - which implies if (a * b) is sorted, then a is sorted and b is > sorted > - a * b = b * a > > Notice that appendo shares all of these properties except the last one. > So this is some sort of generalization of appendo. > > Here is the relation's definition in miniKanren, where a * b = o is > written (riffleo a b o) > > (defrel (riffleo a b o) > (fresh (car-a cdr-a car-b cdr-b car-o cdr-o) > (conde > ;; If `a` and `b` are both empty, then the output is empty. > ((== a '()) (== b '()) (== o '())) > > ;; If `a` is non-empty and `b` is empty, > ;; then the output is equal to `a`. > ((== a `(,car-a . ,cdr-a)) (== b '()) (== o a)) > > ;; If `a` is empty and `b` is non-empty, > ;; then the output is equal to `b`. > ((== a '()) (== b `(,car-b . ,cdr-b)) (== o b)) > > ;; When both `a` and `b` are non-empty > ((== a `(,car-a . ,cdr-a)) (== b `(,car-b . ,cdr-b)) (== o > `(,car-o . ,cdr-o)) > (conde > ((== car-o car-a) (riffleo cdr-a b cdr-o)) > ((== car-o car-b) (riffleo a cdr-b cdr-o))))))) > > And after applying a correctness-preserving transformation: > > (defrel (riffleo a b o) > (fresh (car-a cdr-a car-b cdr-b car-o cdr-o *z0 z1*) > (conde > ;; If `a` and `b` are both empty, > ;; then the output is empty. > ((== a '()) (== b '()) (== o '())) > > ;; If `a` is non-empty and `b` is empty, > ;; then the output is equal to `a`. > ((== a `(,car-a . ,cdr-a)) (== b '()) (== o a)) > > ;; If `a` is empty and `b` is non-empty, then the output is > equal to `b`. > ((== a '()) (== b `(,car-b . ,cdr-b)) (== o b)) > > ;; When both `a` and `b` are non-empty > ((== a `(,car-a . ,cdr-a)) (== b `(,car-b . ,cdr-b)) (== o > `(,car-o . ,cdr-o)) > > > > > *(conde ((== car-o car-a) (== z0 cdr-a) (== z1 b)) > ((== car-o car-b) (== z0 a) (== z1 cdr-b))) > (riffleo z0 z1 cdr-o)*)))) > > I have found riffleo to be useful as a "choose" function when the > arguments are considered multisets rather than lists. For example, it makes > it easy to write the NP-complete 3-partition problem > <https://en.wikipedia.org/wiki/3-partition_problem> as a relation. > > (defrel (three-partitiono l partitions sum) > (fresh (e0 e1 e2 rest-l e0+e1 rest-partitions) > (conde > ;; Base case > ((== l '()) > (== partitions '()))) > > ;; Recursive case > ((== partitions `((,e0 ,e1 ,e2) . ,rest-partitions)) > (riffleo `(,e0 ,e1 ,e2) rest-l l) > (+o e0 e1 e0+e1) > (+o e0+e1 e2 sum) > (three-partitiono rest-l rest-partitions sum)))) > > > Has anyone else encountered this riffle relation? > > Best, > Brett Schreiber > > -- > You received this message because you are subscribed to the Google Groups > "minikanren" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/minikanren/ac5e6700-f7c6-4e1c-8915-d9db0907c715n%40googlegroups.com > <https://groups.google.com/d/msgid/minikanren/ac5e6700-f7c6-4e1c-8915-d9db0907c715n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/minikanren/CACJoNKFVP3AcEaHFGh%3DGdz3VQ0oStyUrWF1JYuZ80A15CGMENA%40mail.gmail.com.
