) a b c)))
```
As you can see, the valid substitutions may appear in any order, and are not normalized by default.
Now, because I do not use natural numbers to indicate the _ordering_ of the variables, from least to most recent, I could not employ the method of projection the paper defines.
However, if one thinks about this for a bit, you realize that each of these pairs are in fact unifiable!
That is to say, to impose a projection over them, you can simply unify the pairs, and then do the reification as per normal.
Fortunately, the paper already defines a procedure for doing just this, called `valid-==`:
```scheme
(define (valid-== ==)
(foldr (λ (pr s) (and s (unify (car pr) (cdr pr) s))) '() ==))
```
where `==` is the substitution context for unification, and each `pr` is an element thereof.
Thus, we can define a projection `π` which gets everything back into shape:
```scheme
(define (reify u ¢)
(let ([v (walk u ¢)])
(cond
[(var? v) v]
[(pair? v)
(cons (reify (car v) ¢)
(reify (cdr v) ¢))]
[else v])))
(define (project §)
(let ([¢ (valid≡ (hash-ref § '≡))]) ;; I use ≡ to mean ==,
;; and ¢ to mean substitution context
(lambda (x) (reify x ¢))))
(define-syntax-rule
(run* (x ...) g₀ g ...)
(let ([x (var)] ...)
(define §* (take-all (call/empty-state (conj* g₀ g ...))))
(for/list ([§ (in-stream §*)])
(let ([π (project §)])
(list (π x) ...)))))
```
Now, everything makes sense.
```scheme
(for-each
displayln
(run* (q)
(append-o '(a b c) '(d e) q)))
'((a b c d e))
```
I haven't thought about whether this could be streamlined earlier in the process, but I thought it was neat that the total number of modifications to the paper's outline was minimal to support the use of non-indexed variables.
Mooiloop.
* * *
My implementation isn't great, but if you'd like to take a gander:
[My Single-File System](https://gist.github.com/bakgatviooldoos/8b28a49497c0aef9a37ab877342d133b)
---
### Author:  [@jasonhemann](https://racket.discourse.group/u/jasonhemann)
#### Post date: [August 20, 2025, 1:59pm UTC](https://racket.discourse.group/t/kanren-learnings/3916/2 "2025-08-20T13:59:57Z")
Hi! We should touch base. Shoot me a letter? [jason.hemann@gmail.com](mailto:jason.hemann@gmail.com)
---
### Author:  [@bakgatviooldoos](https://racket.discourse.group/u/bakgatviooldoos)
#### Post date: [August 23, 2025, 1:03am UTC](https://racket.discourse.group/t/kanren-learnings/3916/3 "2025-08-23T01:03:19Z")
Oh, this subject is so interesting.
Reading some more, I have implemented a rudimentary form of `eigen` variables.
For the interested reader, I am looking at:
- [Relational Synthesis of Programs](http://webyrd.net/cl/cl.pdf)
- [Wildcard Logic Variables How to say in miniKanren that natural number is less than 5?](https://danyaberezun.github.io/publications/assets/mk-2022-wild.pdf)
_The former is referenced by the latter._
To the point, an `eigen` variable is similar to a variable made with `fresh` except that it can only unify with itself, or a `fresh` variable created within its scope.
This will succeed:
```scheme
(eigen (𝕩)
(fresh (x)
(≡ x 𝕩)))
```
But this will fail:
```scheme
(fresh (x)
(eigen (𝕩)
(≡ x 𝕩)))
```
To demonstrate, say we want to distinguish a natural number greater than two:
```scheme
;; fail
(run* ()
(eigen (𝕩)
(fresh (x)
(≡ x `(s (s ,𝕩)))
(≡ x '(s (z)))))) ;; (s (z)) is one, i.e. less than two, so it cannot unify
```
Similarly, using disequality, we can ask for a number less than two:
```scheme
;; okay
(run* ()
(eigen (𝕩)
(fresh (x)
(≢ x `(s (s ,𝕩)))
(≡ x '(s (z))))))
```
Because `eigen` variables can reasonably be thought of as a "tree" of values, given that one has to keep track of their nested scope relative to `fresh` variables, it is convenient to define a wildcard variable, `_`, at the root of the tree, which can then unify with _any_ `fresh` variable.
```scheme
;; okay
(run* (x) (≡ x _))
;; fail
(run* (x) (≢ x _))
```
Next on my reading list, is _Constructive Negation_ and probably _Implication_ along with it.
Not that I understand the math of it all, but being able to mess around with the concepts goes a long way.
---
### Author:  [@bakgatviooldoos](https://racket.discourse.group/u/bakgatviooldoos)
#### Post date: [August 23, 2025, 1:16pm UTC](https://racket.discourse.group/t/kanren-learnings/3916/4 "2025-08-23T13:16:09Z")
> [@bakgatviooldoos](#):
>
> Relational Synthesis of Programs
The combinators from this paper are super intriguing (pg. 5 onward), but I will need to shift gears to think in this mode.
* * *
Another avenue to consider, is _typed variables!_ It ought to be simple to implement with the variables as structs formulation I am using, although I haven't considered the intricacies yet.
---
### Author:  [@bakgatviooldoos](https://racket.discourse.group/u/bakgatviooldoos)
#### Post date: [August 29, 2025, 11:28am UTC](https://racket.discourse.group/t/kanren-learnings/3916/5 "2025-08-29T11:28:26Z")
Ah, I love macros! I mean, they don't always love me back, but that's neither here nor there.
I have been thinking about how to "optimize" the pipeline from kanren-forms to streams.
One part of this, is "delaying" goals which may expand (and cause premature execution), before actually being used.
A simple way to do this, is to make sure that all the provided forms, like `fresh`, `condᵉ`, `disj*`, `conj*`, and so forth, wrap their arguments in `await` calls, which look like:
```scheme
(define-syntax-rule
(await g) (lambda (§) (pause (g §))))
```
where `pause` is an alias for `stream-lazy`.
This is perfectly serviceable, although it does cause inordinate amounts of useless wrapping, due to the fact that there is no way for the system to know what a goal looks like, before actually expanding it.
Easy fix (tongue in cheek), we make a `goal` syntax-class:
```scheme
;; syntax-parameter wrapper
(define-syntax-parameter/slot stable-forms
#:get unbox
#:set set-box!
#:new box null)
...
(define-syntax-class goal
#:attributes (paused)
#:literals (await)
(pattern (await goal)
#:with :goal (local-expand #'goal 'expression {the-stable-forms}))
(pattern (stable . _)
#:when (member #'stable {the-stable-forms} free-identifier=?)
#:attr paused this-syntax)
(pattern goal
#:attr paused #'(await goal)))
```
The stable forms then use this `goal` class, like so:
```scheme
(define-syntax (disj* stx)
(syntax-parse stx
[(_) #'failᵒ]
[(_ :goal) #'paused]
[(_ :goal g ...)
#'(disj paused (disj* g ...))]))
```
I have not yet discovered the "caveats" of using things like `local-expand` but it does the job for now.
The `the-stable-forms` expression is the content of a box held by the syntax-parameter, `stable-forms`. These forms are added to when one used a `defrel` or `defmatch` macro, to include the relation as "stable".
```scheme
(define-syntax-rule
(defrel (name . args) g₀ g ...)
(begin
(define-stable-forms name)
(define (name . args)
(define-exclude-form name
(conj* g₀ g ...)))))
```
Note the use of `define-exclude-form`, which is there to ensure runaway recursion doesn't happen.
Consider the definition,
```scheme
(defrel (fivesᵒ x)
(disj* (≡ x 5) (fivesᵒ x)))
($-each
displayln
(run 4 (x) (fivesᵒ x)))
```
Without the `define-exclude-form` the inside of the `defrel` will think that `fivesᵒ` is _already_ stable and not wrap it at all, creating a stream that never matures.
This way, we can make sure our recursive relations are stable, too.
Anyways, I was just chuffed at using `local-expand` spontaneously for the first time.
---
### Author:  [@bakgatviooldoos](https://racket.discourse.group/u/bakgatviooldoos)
#### Post date: [August 29, 2025, 12:37pm UTC](https://racket.discourse.group/t/kanren-learnings/3916/6 "2025-08-29T12:37:33Z")
"Optimized" 😂
```scheme
(time
($-each
display-numerals
(run 5 (x)
(fresh (y z)
(oddᵒ y)
(timesᵒ y y z)
(timesᵒ y z x)))))
```
```scheme
(1)
(27)
(125)
(343)
(729)
cpu time: 581328 real time: 591855 gc time: 23359
```
This has me thinking, what is a "proof" in kanren?
What I mean, is that in some sense, the substitution context produced as the result of a call like `(timesᵒ y y z)` is a proof that `y^2 = z`, right? If you substitute `u` for `y` and `v` for `z` everywhere in said context, it is a statement of proof (possibly invalidated by the substitution) of `u^2 = v`.
But how does one "canonize" a proof. The computations above take a very long time, because the intermediate work is repeated--is there a way to save the resulting substitution context to obviate unnecessary repetition?
---
### Author:  [@bakgatviooldoos](https://racket.discourse.group/u/bakgatviooldoos)
#### Post date: [August 29, 2025, 11:08pm UTC](https://racket.discourse.group/t/kanren-learnings/3916/7 "2025-08-29T23:08:48Z")
Holy smokes, 100x speedup using hash-tables instead of lists, ~~and only about a doubling of memory (at a glance)~~:
```scheme
(1)
(27)
(125)
(343)
(729)
cpu time: 5671 real time: 5698 gc time: 718
```
^ I am terrible at heuristics.
* * *
Actually memory usage is similar, if somewhat more.
Using `hasheq` tables, cuts the time down by another factor of ~4:
```scheme
(1)
(27)
(125)
(343)
(729)
cpu time: 1234 real time: 1228 gc time: 328
```
---
### Author:  [@bakgatviooldoos](https://racket.discourse.group/u/bakgatviooldoos)
#### Post date: [August 31, 2025, 12:15am UTC](https://racket.discourse.group/t/kanren-learnings/3916/8 "2025-08-31T00:15:01Z")
I initially got `eigen` a bit wrong, but I've reached a closer approximation by now.
One interesting thing you can do with `eigen`, is generate restricted patterns.
I have a macro called `cartesianᵒ`, which constructs the cartesian product of its _rows_, so that:
```scheme
($-each
(compose1 displayln list)
(run* (x y)
((cartesianᵒ
[1 2 3]
[4 5 6])
x y)))
```
shows
```scheme
(1 4)
(2 4)
(1 5)
...
(3 5)
(2 6)
(3 6)
```
Basically, it is a _conjunction of disjunctions_ (product of sums), or just `(conj* (disj* ...) ...)` for short.
Now, suppose we have the following code:
```scheme
(defrel 3-things
(cartesianᵒ
[1 2 3]
[1 2 3]
[1 2 3]))
($-each
(compose1 displayln list)
(run* (x y z)
(3-things x y z)))
```
This produces:
```scheme
(1 1 1)
(2 1 1)
(1 2 1)
(3 1 1)
...
(2 2 3)
(3 2 3)
(2 3 3)
(3 3 3)
```
which is all possible 3-combinations of the items in each row.
But what if we wanted to restrict the result to unique permutations of the values `1,2,3`?
This is where `eigen` comes in. We recall that
> `eigen` can only unify with itself, or a fresh variable created within its scope
We can exploit this behaviour to restrict unification to only certain cases, e.g.
```scheme
(defrel (3-things _₁ _₂ _₃)
(cartesianᵒ
[`(1 ,_₁) `(2 ,_₂) `(3 ,_₃)]
[`(1 ,_₁) `(2 ,_₂) `(3 ,_₃)]
[`(1 ,_₁) `(2 ,_₂) `(3 ,_₃)]))
($-each
(compose1 displayln list)
(run* (x y z)
(eigen (𝕩 𝕪 𝕫)
(fresh (u v w)
((3-things 𝕩 𝕪 𝕫) u v w)
(matchᵉ (u v w)
[{(,a ,m) (,b ,n) (,c ,o)}
(≢ m n)
(≢ m o)
(≢ n o)
(≡ (list x y z)
(list a b c))])))))
```
which shows
```scheme
(3 2 1)
(3 1 2)
(1 3 2)
(2 3 1)
(1 2 3)
(2 1 3)
```
If we only wanted a 3-repetition of a single value each time, we might say
```scheme
($-each
(compose1 displayln list)
(run* (x y z)
(eigen (𝕩 𝕪 𝕫)
(fresh (u v w)
((3-things 𝕩 𝕪 𝕫) u v w)
(matchᵉ (u v w)
[{(,a ,m) (,b ,m) (,c ,m)} ;; note that we say m is the same everywhere
(≡ (list x y z)
(list a b c))])))))
```
to produce
```scheme
(1 1 1)
(2 2 2)
(3 3 3)
```
Similarly, we can restrict the results to include two of the same value each time, like so
```scheme
($-each
(compose1 displayln list)
(run* (x y z)
(eigen (𝕩 𝕪 𝕫)
(fresh (u v w)
((3-things 𝕩 𝕪 𝕫) u v w)
(matchᵉ (u v w)
[{(,a ,m) (,b ,n) (,c ,o)}
(disj*
(conj₂ (≡ m n) (≢ m o))
(conj₂ (≡ m o) (≢ m n))
(conj₂ (≡ n o) (≢ n m)))
(≡ (list x y z)
(list a b c))])))))
```
to produce
```scheme
(2 1 1)
(1 2 1)
(3 1 1)
(1 1 2)
...
(3 3 2)
(2 2 3)
(3 2 3)
(2 3 3)
```
or even _at most_ two repetitions per result (although not unique),
```scheme
($-each
(compose1 displayln list)
(run* (x y z)
(eigen (𝕩 𝕪 𝕫)
(fresh (u v w)
((3-things 𝕩 𝕪 𝕫) u v w)
(matchᵉ (u v w)
[{(,a ,m) (,b ,n) (,c ,o)}
(disj*
(conj₂ (≢ m n) (≢ m o))
(conj₂ (≢ n m) (≢ n o))
(conj₂ (≢ o m) (≢ n o)))
(≡ (list x y z)
(list a b c))])))))
```
which shows
```scheme
(2 1 1)
(1 2 1)
(3 1 1)
(1 1 2)
...
(2 1 3)
(3 1 3)
(2 1 3)
(3 2 2)
(2 1 3)
...
(2 2 3)
(3 2 3)
(2 3 3)
```
Pretty neat.