schemeracketlogic-programmingminikanrenreasoned-schemer# Clarify search algorithms in different minikanren implementation

## 1. Concept clarification

## 2. Explain the different versions of the

### 2.1

### 2.2

### 2.3

## 3. Explain these experiments in the question.

### 1st experiment

### 2nd experiment

### 3rd experiment

## 4. Conclusion

## 5. References

I am currently learning miniKanren by The Reasoned Schemer and Racket.

I have three versions of minikanren implementation:

The Reasoned Schemer, First Edition (MIT Press, 2005). I called it

`TRS1`

https://github.com/miniKanren/TheReasonedSchemer

PS. It says that

`condi`

has been replaced by an improved version of`conde`

which performs interleaving.The Reasoned Schemer, Second Edition (MIT Press, 2018). I called it

`TRS2`

https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd

The Reasoned Schemer, First Edition (MIT Press, 2005). I called it

`TRS1*`

I have did some experiments about the three implementations above:

1st experiment:

`TRS1`

```
(run* (r)
(fresh (x y)
(conde
((== 'a x) (conde
((== 'c y) )
((== 'd y))))
((== 'b x) (conde
((== 'e y) )
((== 'f y)))))
(== `(,x ,y) r)))
;; => '((a c) (a d) (b e) (b f))
```

`TRS2`

```
(run* (x y)
(conde
((== 'a x) (conde
((== 'c y) )
((== 'd y))))
((== 'b x) (conde
((== 'e y) )
((== 'f y))))))
;; => '((a c) (a d) (b e) (b f))
```

`TRS1*`

```
(run* (r)
(fresh (x y)
(conde
((== 'a x) (conde
((== 'c y) )
((== 'd y))))
((== 'b x) (conde
((== 'e y) )
((== 'f y)))))
(== `(,x ,y) r)))
;; => '((a c) (b e) (a d) (b f))
```

Notice that, in the 1st experiment, `TRS1`

and `TRS2`

produced the same result, but `TRS1*`

produced a different result.

It seems that the `conde`

in `TRS1`

and `TRS2`

use the same search algorithm, but `TRS1*`

use a different algorithm.

2nd experiment:

`TRS1`

```
(define listo
(lambda (l)
(conde
((nullo l) succeed)
((pairo l)
(fresh (d)
(cdro l d)
(listo d)))
(else fail))))
(define lolo
(lambda (l)
(conde
((nullo l) succeed)
((fresh (a)
(caro l a)
(listo a))
(fresh (d)
(cdro l d)
(lolo d)))
(else fail))))
(run 5 (x)
(lolo x))
;; => '(() (()) (() ()) (() () ()) (() () () ()))
```

`TRS2`

```
(defrel (listo l)
(conde
((nullo l))
((fresh (d)
(cdro l d)
(listo d)))))
(defrel (lolo l)
(conde
((nullo l))
((fresh (a)
(caro l a)
(listo a))
(fresh (d)
(cdro l d)
(lolo d)))))
(run 5 x
(lolo x))
;; => '(() (()) ((_0)) (() ()) ((_0 _1)))
```

`TRS1*`

```
(define listo
(lambda (l)
(conde
((nullo l) succeed)
((pairo l)
(fresh (d)
(cdro l d)
(listo d)))
(else fail))))
(define lolo
(lambda (l)
(conde
((nullo l) succeed)
((fresh (a)
(caro l a)
(listo a))
(fresh (d)
(cdro l d)
(lolo d)))
(else fail))))
(run 5 (x)
(lolo x))
;; => '(() (()) ((_.0)) (() ()) ((_.0 _.1)))
```

Notice that, in the 2nd experiment, `TRS2`

and `TRS1*`

produced the same result, but `TRS1`

produced a different result.

It seems that the conde in `TRS2`

and `TRS1*`

use the same search algorithm, but `TRS1`

use a different algorithm.

These makes me very confusion.

Could someone help me to clarify these different search algorithms in each minikanren implementation above?

Very thanks.

---- ADD A NEW EXPERIMENT ----

3nd experiment:

`TRS1`

```
(define (tmp-rel y)
(conde
((== 'c y) )
((tmp-rel-2 y))))
(define (tmp-rel-2 y)
(== 'd y)
(tmp-rel-2 y))
(run 1 (r)
(fresh (x y)
(conde
((== 'a x) (tmp-rel y))
((== 'b x) (conde
((== 'e y) )
((== 'f y)))))
(== `(,x ,y) r)))
;; => '((a c))
```

However, `run 2`

or `run 3`

loops.

If I use `condi`

instead of `conde`

, then `run 2`

works but `run 3`

still loop.

`TRS2`

```
(defrel (tmp-rel y)
(conde
((== 'c y) )
((tmp-rel-2 y))))
(defrel (tmp-rel-2 y)
(== 'd y)
(tmp-rel-2 y))
(run 3 r
(fresh (x y)
(conde
((== 'a x) (tmp-rel y))
((== 'b x) (conde
((== 'e y) )
((== 'f y)))))
(== `(,x ,y) r)))
;; => '((b e) (b f) (a c))
```

This is OK, except that the order is not as expected.

Notice that `(a c)`

is at the last now.

`TR1*`

```
(define (tmp-rel y)
(conde
((== 'c y) )
((tmp-rel-2 y))))
;;
(define (tmp-rel-2 y)
(== 'd y)
(tmp-rel-2 y))
(run 2 (r)
(fresh (x y)
(conde
((== 'a x) (tmp-rel y))
((== 'b x) (conde
((== 'e y) )
((== 'f y)))))
(== `(,x ,y) r)))
;; => '((a c) (b e))
```

However, `run 3`

loops.

Solution

After several days of research, I think I have been able to answer this question.

First of all, I'd like to clarify some concepts:

There are two well-known models of non-deterministic computation: the stream model and the two-continuations model. Most of miniKanren implementations use the stream model.

PS. The term "backtracking" generally means depth-first search (DFS), which can be modeled by either the stream model or the two-continuations model. (So when I say "xxx get tried", it doesn't mean that the underlying implementation have to use two-continuations model. It can be implemented by stream model, e.g. minikanren.)

`conde`

or `condi`

`conde`

and `condi`

in `TRS1`

`TRS1`

provides two goal constructors for non-deterministic choice, `conde`

and `condi`

.

`conde`

uses DFS, which be implemented by MonadPlus of stream.

The disadvantage of MonadPlus is that it is not fair. When the first alternative offers an infinite number of results, the second alternative is never tried. It making the search incomplete.

To solve this incomplete problem, `TRS1`

introduced `condi`

which can interleave the two results.

The problem of the `condi`

is that it can’t work well with divergence (I mean dead loop with no value). For example, if the first alternative diverged, the second alternative still cannot be tried.

This phenomenon is described in the Frame 6:30 and 6:31 of the book. In some cases you may use `alli`

to rescue, see Frame 6:32, but in general it still can not cover all the diverged cases, see Frame 6:39 or the following case: (PS. All these problems do not exist in `TRS2`

.)

```
(define (nevero)
(all (nevero)))
(run 2 (q)
(condi
((nevero))
((== #t q))
((== #f q))))
;; => divergence
```

Implementation details:

In `TRS1`

, a stream is a standard stream, i.e. lazy-list.

The `conde`

is implemented by `mplus`

:

```
(define mplus
(lambda (a-inf f)
(case-inf a-inf
(f)
((a) (choice a f))
((a f0) (choice a (lambdaf@ () (mplus (f0) f)))))))
```

The `condi`

is implemented by `mplusi`

```
:(define mplusi
(lambda (a-inf f)
(case-inf a-inf
(f)
((a) (choice a f))
((a f0) (choice a (lambdaf@ () (mplusi (f) f0)))))) ; interleaving
```

`conde`

in `TRS2`

`TRS2`

removed the above two goal constructors and provided a new `conde`

.

The `conde`

like the `condi`

, but only interleaving when the first alternative is a return value of a relation which be defined by `defref`

. So it is actually more like the old `conde`

if you won't use `defref`

.

The `conde`

also fixed the above problem of `condi`

.

Implementation details:

In `TRS2`

, a stream is not a standard stream.

As the book says that

A stream is either the empty list, a pair whose cdr is a stream, or a suspension.

A suspension is a function formed from (lambda () body) where (( lambda () body)) is a stream.

So in `TRS2`

, streams are not lazy in every element, but just lazy at suspension points.

There is only one place to initially create a suspension, i.e. `defref`

:

```
(define-syntax defrel
(syntax-rules ()
((defrel (name x ...) g ...)
(define (name x ...)
(lambda (s)
(lambda ()
((conj g ...) s)))))))
```

This is reasonable because the "only" way to produce infinite results or diverge is recursive relation. It also means that if you use `define`

instead of `defrel`

to define a relation, you will encounter the same problem of `conde`

in `TRS1`

(It is OK for finite depth-first search).

Note that I had to put quotation marks on the "only" because most of the time we will use recursive relations, however you still can produce infinite results or diverge by mixing Scheme's named `let`

, for example:

```
(run 10 q
(let loop ()
(conde
((== #f q))
((== #t q))
((loop)))))
;; => divergence
```

This diverged because there is no suspension now.

We can work around it by wrapping a suspension manually:

```
(define-syntax Zzz
(syntax-rules ()
[(_ g) (λ (s) (λ () (g s)))]))
(run 10 q
(let loop ()
(Zzz (conde
((== #f q))
((== #t q))
((loop)))) ))
;; => '(#f #t #f #t #f #t #f #t #f #t)
```

The `conde`

is implemented by `append-inf`

:

```
(define (append-inf s-inf t-inf)
(cond
((null? s-inf) t-inf)
((pair? s-inf)
(cons (car s-inf)
(append-inf (cdr s-inf) t-inf)))
(else (lambda () ; interleaving when s-inf is a suspension
(append-inf t-inf (s-inf))))))
```

`conde`

in `TRS1*`

`TRS1*`

originates from the early paper "From Variadic Functions to Variadic Relations A miniKanren Perspective". As `TRS2`

, `TRS1*`

also removed the two old goal constructors and provided a new `conde`

.

The `conde`

like the `conde`

in `TRS2`

, but only interleaving when the first alternative itself is a `conde`

.

The `conde`

also fixed the above problem of `condi`

.

Note that there is no `defref`

in `TRS1*`

. Therefore if the recursive relations are not starting from `conde`

, you will encounter the same problem of `condi`

in `TRS1`

. For example,

```
(define (nevero)
(fresh (x)
(nevero)))
(run 2 (q)
(conde
((nevero))
((== #t q))
((== #f q))))
;; => divergence
```

We can work around this problem by wrapping a `conde`

manually:

```
(define (nevero)
(conde
((fresh (x)
(nevero)))))
(run 2 (q)
(conde
((nevero))
((== #t q))
((== #f q))
))
;; => '(#t #f)
```

Implementation details:

In `TRS1*`

, the stream is the standard stream + suspension.

```
(define-syntax conde
(syntax-rules ()
((_ (g0 g ...) (g1 g^ ...) ...)
(lambdag@ (s)
(inc ; suspension which represents a incomplete stream
(mplus*
(bind* (g0 s) g ...)
(bind* (g1 s) g^ ...) ...))))))
(define-syntax mplus*
(syntax-rules ()
((_ e) e)
((_ e0 e ...) (mplus e0 (lambdaf@ () (mplus* e ...)))))) ; the 2nd arg of the mplus application must wrap a suspension, because multiple clauses of a conde are just syntactic sugar of nested conde with 2 goals.
```

It also means that the named let `loop`

problem above does not exist in `TRS1*`

.

The `conde`

is implemented by the interleaving `mplus`

:

```
(define mplus
(lambda (a-inf f)
(case-inf a-inf
(f)
((a) (choice a f))
((a f^) (choice a (lambdaf@ () (mplus (f) f^))))
((f^) (inc (mplus (f) f^)))))) ; interleaving when a-inf is a suspension
; assuming f must be a suspension
```

Note that although the function is named `mplus`

, it is not a legal MonadPlus because it does not obey MonadPlus law.

Now I can explain these experiments in the question.

`TRS1`

=> `'((a c) (a d) (b e) (b f)) `

, because `conde`

in `TRS1`

is DFS.

`TRS2`

=> `'((a c) (a d) (b e) (b f)) `

, because `conde`

in `TRS2`

is DFS if no `defref`

involved.

`TRS1*`

=> `'((a c) (b e) (a d) (b f))`

, because `conde`

in `TRS1*`

is interleaving (the outmost `conde`

make the two innermost `conde`

s interleaving).

Note that if we replace `conde`

with `condi`

in `TRS1`

, the result will be the same as `TRS1*`

.

`TRS1`

=> `'(() (()) (() ()) (() () ()) (() () () ())) `

, because `conde`

in `TRS1`

is DFS. The second clause of `conde`

in `listo`

is never tried, since when `(fresh (d) (cdro l d) (lolo d)`

is `bind`

ed to the first clause of `conde`

in `listo`

it offers an infinite number of results.

`TRS2`

=> `'(() (()) ((_0)) (() ()) ((_0 _1))) `

, because now the second clause of `conde`

in `listo`

can get tried. `listo`

and `lolo`

being defined by `defrel`

means that they will potentially create suspensions. When `append-inf`

these two suspensions, each takes a step and then yield control to the other.

`TRS1*`

=> `'(() (()) ((_.0)) (() ()) ((_.0 _.1))`

, is the same as `TRS2`

, except that suspensions are created by `conde`

.

Note that replacing `conde`

with `condi`

in `TRS1`

will not change the result. If you want to get the same result as `TRS2`

or `TRS1*`

, wrap `alli`

at the second clause of `conde`

.

Note that as @WillNess said in his comment of the question:

BTW I didn't know you could write

`(define (tmp-rel-2 y) (== 'd y) (tmp-rel-2 y))`

like that, without any special minikanren form enclosing the two goals...

Yes, the 3rd experiment about `TRS1`

and `TRS1*`

has a mistake:

```
(define (tmp-rel-2 y) ; <--- wrong relation definition!
(== 'd y)
(tmp-rel-2 y))
```

Unlike `TRS2`

, `TRS1`

and `TRS1*`

have no build-in `defrel`

, so the `define`

form is from Scheme, not minikaren.

We should use a special minikanren form enclosing the two goals.

Therefore,

For `TRS1`

, we should change the definition to

```
(define (tmp-rel-2 y)
(all (== 'd y)
(tmp-rel-2 y)))
```

For `TRS1*`

, there is no `all`

constructor, but we can use `(fresh (x) ...)`

to work around it

```
(define (tmp-rel-2 y)
(fresh (x)
(== 'd y)
(tmp-rel-2 y)))
```

I made this mistake because I was not familiar with minikanren before.

However, this mistake won't affect the final result, and the explanation below for `TRS1`

and `TRS1*`

are suitable for both the wrong definition and the correct definition.

`TRS1`

=> `'((a c))`

, because `conde`

in `TRS1`

is DFS. The `tmp-rel`

diverges at `tmp-rel-2`

.

Note that replacing `conde`

with `condi`

and `(run 2 ...)`

, we will get `'((a c) (b e))`

. This because `condi`

can interleave. However, it still cannot print the third solution `(b f)`

because `condi`

can’t work well with divergence.

`TRS2`

=> `'((b e) (b f) (a c)) `

, because `TRS2`

can archive complete search if we use `defrel`

to define relation.

Note that the final result is `'((b e) (b f) (a c))`

instead of `'((a c) (b e) (b f))`

because in `TRS2`

, a suspension only initially be created by `defrel`

. If we expect `'((a c) (b e) (b f))`

, we can wrap the suspension manually:

```
(define-syntax Zzz
(syntax-rules ()
[(_ g) (λ (s) (λ () (g s)))]))
(run 3 r
(fresh (x y)
(conde
((== 'a x) (tmp-rel y))
((== 'b x) (Zzz (conde ; wrap a suspension by Zzz
((== 'e y) )
((== 'f y))))))
(== `(,x ,y) r)))
;; => '((a c) (b e) (b f))
```

`TRS1*`

=> `'((a c) (b e))`

, because in `TRS1*`

, suspensions be wrapped at `conde`

s .

Note that it still cannot print the third solution `(b f)`

because `tmp-rel-2`

does not be wrapped in `conde`

, so no suspension is created here. If we expect `'((a c) (b e) (b f))`

, we can wrap the suspension manually:

```
(define (tmp-rel-2 y)
(conde ((== 'd y) (tmp-rel-2 y)))) ; wrap a suspension by conde
```

All in all, minikanren is not one language but families of languages. Each minikanren implementation may have its own hack. There may be some corner cases which have slightly different behaviors in different implementations. Fortunately, minikanren is easy to understand. When encountering these corner cases, we can solve them by reading the source code.

The Reasoned Schemer, First Edition (MIT Press, 2005)

From Variadic Functions to Variadic Relations - A miniKanren Perspective

The Reasoned Schemer, Second Edition (MIT Press, 2018)

µKanren: A Minimal Functional Core for Relational Programming

Backtracking, Interleaving, and Terminating Monad Transformers

- What is the Lisp's symbol equivalent of JavaScript?
- Difference between Print and Display
- Are there any purely functional Schemes or Lisps?
- Is such a function structure tail recursive?
- Mathematically, why does this SICP algorithm for the exponent of a number modulo another number work?
- What's the best way to learn LISP?
- Do tail-recursive functions reuse a single environment in Scheme?
- Y combinator discussion in "The Little Schemer"
- Difference between null? and empty? in Scheme
- Does GNU Guile not have the vector->string function?
- A Scheme compiler for ARM processors
- `1.0+1e-100=1.` in MIT-scheme
- What is the best way to automatically transpose a LilyPond source file into multiple keys?
- How do I get the partition to return two list output when pivot and the list are given as inputs?
- Creating Custom GnuCash Reports with Scheme
- Redefining the special form after the usage of that special form in one func definition has no effects to that definition in Scheme
- Compiling a .ss file
- Why isn't promise a data type in Scheme?
- Is environment model necessary for higher-order procedures?
- How to make `set!` change the variable in `let` (Scheme)?
- Inheritance classes in Scheme
- How do I get the functions put and get in SICP, Scheme, Exercise 2.78 and on
- Trouble understanding / visualising SICP streams Hamming numbers program
- Unbound variable error in cube root function
- Scheme - Replacing elements in a list with its index
- What is the relation of parent env and the child env in MIT-Scheme?
- conda, condi, conde, condu
- Pipe-Function in scheme
- DrRacket: atom? and symbol? undefined - What's wrong?
- curry in scheme