What is the name of this relation?

[Brett Schreiber]

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

[William Byrd]

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

--
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 minikanren+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/minikanren/ac5e6700-f7c6-4e1c-8915-d9db0907c715n%40googlegroups.com.

[Brett Schreiber]

Hi Will!

The `split` relation in the code you linked (llmr.scm)  is a very similar relation on the domain of multisets. Thank you for sharing!

Regarding another use of `riffleo`: I have been trying to transform an undirected graph into a sequence of nonoverlapping bicliques (complete bipartite subgraphs). This is always possible, since every graph has a maximum independent edge set (which can be thought of as (1, 1)-bicliques). This decomposition into bicliques has an application in graph coloring.

I have found `riffleo` useful for partitioning the vertices of the graph into 3 sets: `left`, `right`, and `rest-v`. Then I can check if there is an edge from every vertex in `left` to every vertex in `right`. Here is the code for that. Hopefully the implicit relations make sense.

(defrel (bicliqueso graph bicliques)
  (conde
    ((== bicliques '()) (empty-grapho graph))

    ((fresh (v e rest-v rest-e rest-g rest-bicliques left right*rest-v right)

      ;; A biclique is a pair of vertex sets
      (== bicliques `((,left . ,right) . ,rest-bicliques))

      (pairo left)

      (pairo right)
       

      ;; Assume an efficient undirected graph data structure
      (verticeso g v)

      (verticeso rest-g rest-v)
      (edgeso g e)

      (edgeso rest-g rest-e)

      ;; partition the vertices into nonempty `left`, nonempty `right`, and `rest-v`

      (riffleo left right*rest-v v)
      (riffleo right rest-v right*rest-v)

      ;; check that every vertex in `left` is connected to every vertex in `right`
      (is-bicliqueo left right g)

      ;; Keep only the edges which have both vertices in `rest-v`
      (filtero e rest-v rest-e)
           
      (bicliqueso rest-g rest-bicliques)))))

This ended up being unfeasible since I could not think of a good data structure for representing an undirected graph in miniKanren, and I found it difficult to write `is-bicliqueo`. I ended up porting `riffleo` into Python as `unriffle`.

def unriffle(o: List[T]) -> Iterator[Tuple[List[T], List[T]]:

    ...

I used that for a while in Python until I figured out a bottom-up way to find all bicliques by constructing a table all_bicliques_of_size[m][n].

TL;DR - `riffleo` can be used to partition a set into n disjoint subsets, which may be useful for detecting bicliques.

Brett

[Brett Schreiber]

I found this relation in two more places:

First was in the Wikipedia article on Logic programming, under "Concurrent logic programming". It is written in Prolog as shuffle/3. Here, the relation models the nondeterminism that occurs when two processes run at the same time. It was added in a 2014 revision, and it can still be found in the current version of the article:

https://en.wikipedia.org/w/index.php?title=Logic_programming&diff=prev&oldid=621458003

Second was in this StackOverflow question from 2018, which I found from Googling "prolog shuffle". The question asks how the relation works, and does not give any applications.

https://stackoverflow.com/questions/52211171/how-does-this-prolog-code-really-work-shuffle-two-lists

[Brett Schreiber]

Here is another use-case I found for riffleo: subsequenceo, a 3-relation between two lists and one of their common subsequences. It might also be possible to create a longest common subsequence relation by adding a disequality constraint somewhere.

#lang racket

(include "../../CodeFromTheReasonedSchemer2ndEd/trs2-impl.scm")

(require "riffleo.mk.rkt")

(defrel (subsequenceo l1 l2 s)
  (fresh (x1 x2)
         (riffleo s x1 l1)
         (riffleo s x2 l2)))

#;(run 10 (l1 l2 s) (subsequenceo l1 l2 s))
#;'((()
     ()
     ())

    (()
     (_0 . _1)
     ())
   
    ((_0 . _1)
     (_0 . _1)
     (_0 . _1))
   
    ((_0 . _1)
     ()
     ())

    ((_0 . _1)
     (_2 . _3)
     ())

    ((   _0 . _1)
     (_2 _0 . _1)
     (   _0 . _1))
   
    ((_0)
     (_0 _1 . _2)
     (_0))
   
    ((_0 _1 . _2)
     (   _1 . _2)
     (   _1 . _2))

    ((      _0 . _1)
     (_2 _3 _0 . _1)
     (      _0 . _1))
   
    ((_0    _1 . _2)
     (_0 _3 _1 . _2)
     (_0    _1 . _2)))


#;(run 10 (l1 l2) (subsequenceo l1 l2 '(a b c)))
#;'(((a b c)
     (a b c))
   
    ((   a b c)
     (_0 a b c))

    ((_0 a b c)
     (   a b c))
   
    ((a    b c)
     (a _0 b c))
   
    ((      a b c)
     (_0 _1 a b c))
   
    ((_0 a b c)
     (_1 a b c))
   
    ((a b c)
     (a b c _0 . _1))

    ((a b    c)
     (a b _0 c))
   
    ((a _0 b c)
     (a    b c))
   
    ((   a    b c)
     (_0 a _1 b c)))