In logic programming, what is unnesting for?

Question

The question

The Reasoned Schemer describes how to use miniKanren, which resembles Prolog but is a library for Lisp-like languages. The book's "First Commandment" is this:

To transform a function whose value is a Boolean into a function whose value is a goal, replace cond with conde and unnest each question and answer. Unnest the answer #t (or #f) by replacing it with #s (or #u).

They don't really define unnesting, except through a few roughly equivalent example. The clearest is this: unnesting takes you from (list? (cdr l)) to

(fresh (d)
       (cdro l d)
       (listo d))

I don't understand why unnesting is needed. For instance, for the above goal, why is it not sufficient tp write (listo (cdr l))?

[1] My mini-kanren setup in Racket

As described here, I ran raco pkg install minikanren and then defined a few missing pieces.

[2] Some function definitions you may not need

Here are the definitions of listo and everything it uses it, except for things defined in the minikanren library or in Racket's prelude.

(define listo
  (lambda (l)
    (conde
     ((nullo l) #s)
     ((pairo l)
      (fresh (d)
             (cdro l d)
             (listo d)))
     (else #u))))

(define nullo
  (lambda (x)
    (== x '())))

(define pairo
  (lambda (p)
    (fresh (a d)
           (conso a d p))))

(define cdro
  (lambda (p d)
    (fresh (a)
           (== (cons a d) p))))

(define conso
  (lambda (head tail result)
    (== (cons head tail) result)))

Answer 1

Disclaimer, I don't know scheme and I'm about 1/5 into this book.

I think it's needed because the function you're replacing often has input parity (number of arguments taken) lower than the one you're replacing it with. You're kind of refactoring a function to put the output into a variable that you pass into it instead of returning it as output. Why do you need to replace each function with a logical equivalent? I'm not totally sure,

(Edit I read the context of your example more...) if we take the example you gave, the standard version would raise an error if passed a non-list I think, which is different from returning failure. So if you pass something that's not a list, instead of getting () from your run, you raise an exception which is different. There's another difference I realized, and a more important one. Your example comes from the definition of listo, and listo doesn't just check for whether something can be a list. it could be used to generate an infinite list if given an unbound variable. It does that because first the first element in the conde will succeed so you'll get (). After, pairo l will succeed by making the first element (reified_1) and the second element goes back to listo, this inner listo first returns () like the first result of the outer listo did, so you get (reified_1 . ()) and this can continue infinitely. This works because you have (cdro l d) with a fresh d, allowing d to be bound to a variable which is set by the recursive call to listo. You couldn't do that without creating the d variable by unnesting.

Explaining the parity point:

cdr(x) # get the rest elements of x
cdro(a x) # you "pass in" the equivalent to the output element of the first function into this logical version. 

That means that if you have b = cdr(cdr(x)) You need to create a variable to hold the intermediate value like:

fresh(a)
cdro(a, x)
fresh(b)
cdro(b, a)

See the difference/reason? You're passing in your outputs. So you can't "nest" where everything sits inside the nested expression, you need to break it into lines to have space to assign your new variables.

Why does it have to be this way? I was considering whether you could avoid a lot of unnesting by overloading the functions based on parity. Something like I've written below (in python, assume caro is already defined). The point is that I think it's useless because the variable you bind to the first element of the list is new, not referred to anywhere else, so can't possibly be useful for applying any other constraints. The point of goals is to return sets of bindings that satisfy them, but those bindings must be on variables that are already defined or they're useless.

class UNDEF:
    pass

def cdronew(a, b=UNDEF):
    if b is UNDEF:
        # assume that we need to fresh a variable and use that for our output
        b = fresh('b')
        # not a typo in order, we're assuming we wanted the first val of the list
        # here is the problem, we'll bind b but noone outside this function knows about it so that binding is useless!
        return cdro(b, a)
    else:
        return cdro(a, b)

Answer 2

the term un-nesting means to modify the hierarchy of the structure - or to remove brackets.

just found the book The Reasoned Schemer and the associated GitHub page, which also defines it:

Process of transforming (car (cdr l)) into (cdro l v) and (caro v r) is called unnesting… . Recognize the similarity between unnesting and [CPS].

Answer 3

"Unnesting" is for SSA transform, because that's how Prolog is, because it doesn't have evaluation and all state changing and passing must be done explicitly.

SSA form is what you get your code as after performing a limited form of CPS transform. Simply, each interim entity is made explicit and is given a name.

(let* ((c (+ (sqr x) (sqr y)) )
       (z (sqrt c)))
  ....

is transformed into

(let*  ((a (sqr x))
        (b (sqr y))
        (c (+ a b))
        (z (sqrt c)))
  ....

Similarly, as you write, the Lisp code (list? (cdr l)) is turned into a predicate

    ( L = [_ | D], 
      is_list( D ) )

in Prolog, which is the goal

    (fresh (d)
       (cdro l d)    ; a relation "cdro" holds between `l` and `d`
       (listo  d))   ; a predicate listo holds for `d`

in miniKanren. Why? Because (cdr l) is a Lisp function which returns a value. But in Prolog there is no evaluation, there are no values returned implicitly, but rather they are put into existence explicitly by a predicate, a relation, by "setting" a logical variable which is an argument to that predicate.