Not understanding The Reasoned Schemer Chapter 5 frame 62

316 views Asked by At

I am currently learning miniKanren by learning The Reasoned Schemer.

And I am stuck in an exercise in Chapter 5 frame 62: (run* (x) (flatten_o (a) x)), why there are three lists in output?

1

There are 1 answers

0
William E. Byrd On

Good question! Where do these extra lists come from???

The problem is in the else clause of the definition of flatteno. The else clause handles the case in which s is a symbol (the symbol a, here). However, the clause also allows s to be the empty list or a pair! This is why we see three lists instead of one---the extra two lists are produced by recursive calls that succeed due to the else clause accepting non-symbol values for s.

In later versions of miniKanren we have added special constraints such as symbolo and =/= to prevent such behavior. For example, here is the same query, and flatteno, written in faster-miniKanren (https://github.com/webyrd/faster-miniKanren):

(define flatteno
  (lambda (s out)
    (conde
      ((== '() s) (== '() out))
      ((fresh (a d res-a res-d)
         (== (cons a d) s)
         (flatteno a res-a)
         (flatteno d res-d)
         (appendo res-a res-d out)))
      ((symbolo s) (== (cons s '()) out)))))

(run* (x)
  (flatteno '(a) x))
=>
((a))

Note the use of the symbolo constraint in flatteno to ensure s is a symbol.

You can find a non-"Little Book" explanation of these constraints in this paper:

http://webyrd.net/quines/quines.pdf

We are trying to figure out how to include a description of these constraints in a Little Book format. The implementation of the constraints is a bit involved, which makes it hard to fit in a Little Book!

Hope this helps!

Cheers,

--Will