"fresh" - why not "leto"?

[Brian Damgaard]

As a newcomer to Microkanren/Minikanren I'm puzzled by the use of the word "fresh" for creating new logical variables.

Could someone please explain to me, whether there is some deep reason for this choice, instead of the seemingly much better, obvious, and more natural word "leto"?

"leto" would be in accordance with the appealing naming-convention used everywhere else in the language, e.g., "conde", "appendo", just to name a few.

"leto" would be a pleasing reference to "let", as it's known from so many other languages, including the lisp/scheme family. Furthermore, "leto" is shorter and easier to write, and is even feels more "fresh" and tasty - as a language construct - than literally using the word "fresh".

A different topic:

I have a minor "complaint", or rather a suggested improvement.

In the official book source code found here...:

https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd/blob/master/trs2-impl.scm

... all places in the source code, where an empty stream is returned, the expression "'()" is used. It would improve the code quality - making the code more self-documenting - to use the expression "empty-s" which is defined at the very beginning of the code. (Personally I'd prefer "empty-stream", but that's a different story.)

-bd

[Rick Moynihan]

On Sun, 28 Oct 2018 at 16:14, Brian Damgaard <briand...@gmail.com> wrote:

As a newcomer to Microkanren/Minikanren I'm puzzled by the use of the word "fresh" for creating new logical variables.

Could someone please explain to me, whether there is some deep reason for this choice, instead of the seemingly much better, obvious, and more natural word "leto"?

My understanding is that the o suffix isn't really used to disambiguate minikanren from scheme, it's used to indicate a relation, and the process of creating a logic variable isn't a relation, so there's no o suffix.

R.

[William Byrd]

Hi Brian!

> As a newcomer to Microkanren/Minikanren I'm puzzled by the use of the word "fresh" for creating new logical variables.
>
> Could someone please explain to me, whether there is some deep reason for this choice, instead of the seemingly much better, obvious, and more natural word "leto"?
>
> "leto" would be in accordance with the appealing naming-convention used everywhere else in the language, e.g., "conde", "appendo", just to name a few.
>
> "leto" would be a pleasing reference to "let", as it's known from so many other languages, including the lisp/scheme family. Furthermore, "leto" is shorter and easier to write, and is even feels more "fresh" and tasty - as a language construct - than literally using the word "fresh".

The 'fresh' form introduces new logic variables that have no value
assigned to them. We refer to such logic variables as "fresh", hence
the name for the form.

Syntactically, 'fresh' is closer to 'lambda' than to 'let'. 'let'
introduces variable/expression pairs, and binds the variables to the
values of those expressions before evaluating the body. The entire
point of 'fresh' is that the logic variables introduced are "fresh",
and are not associated with any value. For this reason, 'leto' would
be a misleading name.

> A different topic:
> I have a minor "complaint", or rather a suggested improvement.
>
> In the official book source code found here...:
>
> https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd/blob/master/trs2-impl.scm
>
> ... all places in the source code, where an empty stream is returned, the expression "'()" is used. It would improve the code quality - making the code more self-documenting - to use the expression "empty-s" which is defined at the very beginning of the code. (Personally I'd prefer "empty-stream", but that's a different story.)

Ah--the problem here is that 'empty-s' refers to the empty
substitution, not the empty stream! The '() expressions you see in
the code are indeed empty streams, but not an empty-s.

It would probably be better for us to define 'empty-subst' and
'empty-stream' both to be the empty list, and to use 'empty-stream'
instead of '() in the definitions.

Thanks for the observation!

Cheers,

--Will

> -bd
>
> --
> 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 post to this group, send email to minik...@googlegroups.com.
> Visit this group at https://groups.google.com/group/minikanren.
> For more options, visit https://groups.google.com/d/optout.

[Brian Damgaard]

Thanks for the replies from you two -  Rick and Will.

I understand the arguments for not using "leto" instead of "fresh", i.e., that "let" traditionally is a "let new variable = value" construct.

But in my opinion, a term like "leto" would have been - and is - a better choice anyway. I put more weight on the first property of "let": It introduces new variables in the code.The fact that the variables aren't assigned any values at the time of declaration in a Kanren program is not something which makes me feel uncomfortable with the term "leto".

As I see it, it would feel perfectly natural to read and interpret "leto" as having the meaning "let these new variables be used in the following code block".

The Kanren-family of languages has already stretched the meaning of another core term borrowed from the lisp-family: "cond". In Kanren, it comes in the three flavors conde, conda, and condu, and these terms must have been deliberately chosen to make them easier to understand  because they resemble the familiar "cond" term borrowed in Lisp.

In the same vein, "leto" is a better choice than "fresh" because of the resemblance between "leto" and the "let" - the latter traditionally being used in other languages for the same purpose, i.e., to introduce new variables in a code block.

Seen this way "leto" would not be misleading (as Will uttered). Perhaps "let" would have been problematic, but with the "o"-suffix, the "leto" construct is properly distinguishable from "let", just like conde, conda, and condu are distinguishable from "cond".

Another objection I have to the term "fresh" has to do with "musicality". As I see it, the term "fresh" is so much out of of tune, as it possible can be, with the otherwise very refreshing terminology used in the Kanren language family.

If not "leto, then the term for the "fresh" language construct should at least be another neologism adhering to the overall language design. A term like "varo" comes to mind as a splendid candidate, with its reference to the Algol-language family (e.g., Pascal, Modula, Oberon) "var" construct, which works the same way as "fresh": It introduces new variables, but without initializing them at the same time.

All that said, let me end this post by telling how much I've  enjoyed getting acquainted with Micro/Mini-Kanren. The implementation is truly mind-blowing (at least for me - quoting Winnie the Pooh: "I'm a bear of very little brain :-) It's marvelous that a language with such extraordinary features can be implemented so elegantly and so cleverly in just about 200 lines of  Lisp/Scheme code. There is so much intelligence and cleverness engraved in these 200 lines that it turns into "logical poetry and beauty" - something the original programmers and inventors can be very, very proud of.

Based on the original source code version from the literature, I wrote a micro/mini-kanren implementation so it runs on my own Lisp system - a pet-project of mine. It's probably never going to be published anywhere, so just for my own pleasure, I've listed it below. Comments, corrections, and suggestions on how to improve the code and the comments (English is not my first language) are welcome.

Even though my source is utterly uninteresting to others, I have, nevertheless, a few things to say about it, which might have a minuscule general interest:

1.
This code shows how to implement the necessary macros with quasiquotes only, i.e., without a pattern-based macro system, like Scheme has.

2.
I use the term "bindings" everywhere in the code, where the reference implementations in the literature always talk about a "substitution". The latter is misleading. The program has data for a substitution. A substitution can be made, based on the data. In simple Kanren implementations like mine, and the reference implementations in the literature, the available data is a simple, so-called "assoc-list", a list of key-value bindings.

3.
Even though I kept the term "fresh", I offer three other name improvements at the bottom of the code, in form of symbol-macros:

* "rl" for define-relation.
There is no way I as a programmer will put up with writing "define-relation" each time I define a relation.

* "oro" for disj
* "ando" for conj

I think that "oro" and "ando" are quicker to grasp when reading code. I don't know how other people feel, but my theory is that it takes more brain-power to grasp words like "disj" and "conj", i.e., that more brain-circuitry is involved in deciphering the meaning of such words, whereas basic words like "or" and "and" are decoded by the brain on a fast lane.

I guess this is similar to the interesting observation that the human brain can grasp that there are 4 items in view, but as soon as there are 5 items, the brain changes much change to some different circuitry and do the actual counting!

- bd

(mc variable-tag      (variable) `(first ,variable))
(mc variable-name     (variable) `(rest  ,variable))
(mc make-variable     (name)     `(cons  micro-kanren-variable-tag ,name))
(mc variable?         (u)        `(and (pair? ,u) (same-object? (variable-tag ,u) micro-kanren-variable-tag)))
(mc bindings->stream  (bindings)  `(list ,bindings)) ; elevates a set of bindings to a stream of sets of bindings
(const empty-stream   nil) ; must be nil
(const fail           empty-stream) ; must be nil
(const succeed        (fn (bindings) (bindings->stream bindings)))
(const micro-kanren-initial-bindings (list nil)) ; must be non-nil
(const micro-kanren-variable-tag (list nil)) ; must be unique

(fn extend-bindings (variable value bindings) ; associates "variable" with "value" in a new set of bindings
  (if (not (occurs-in? variable value bindings))
      (acons variable value bindings))) ; using built-in "acons" function

(fn occurs-in? (variable value bindings) ; checks whether "variable" occurs in "value"
  (let value (walk value bindings)
    (if (variable? value)
          (same-object? variable value)
        (pair? value)
          (or (occurs-in? variable (first value) bindings)
              (occurs-in? variable (rest  value) bindings)))))

(fn == (u v) ; tries to unify the two terms "u" and "v", using the given bindings
  (fn (bindings)
    (if (set bindings (unify u v bindings))
        (bindings->stream bindings)          
        empty-stream)))

(fn walk (value bindings) ; dereferences the value, using the given bindings
  (let binding _
    (while (and (variable? value)
                (set binding (assoc value bindings same-object?))) ; compare: identity, i.e., "eq" in Common Lisp
      (set value (rest binding)))
    value))      

(fn unify (u v bindings) ; tries to unify the two terms "u" and "v", using the given bindings
  (let u (walk u bindings)
       v (walk v bindings)
    (if (same-object? u v)
           bindings
        (variable? u)
          (extend-bindings u v bindings)
        (variable? v)
          (extend-bindings v u bindings)
        (and (pair? u) (pair? v))
          (and (set bindings (unify (first u) (first v) bindings))
               (unify (rest u) (rest v) bindings))
        (=? u v)
          bindings)))

(fn call/fresh (variable-name function) ; runs the function with a newly created variable as argument
  (fn (bindings)
    ((function (make-variable variable-name)) bindings)))

(mc disj2 (goal1 goal2) `(fn (bindings) (append-streams (,goal1 bindings) (,goal2 bindings))))
(mc conj2 (goal1 goal2) `(fn (bindings) (append-map-streams ,goal2 (,goal1 bindings))))

(fn append-streams (stream1 stream2)
  (if (nil? stream1)
        stream2
      (function? stream1)
        (fn () (append-streams stream2 (stream1)))
      (cons (first stream1) (append-streams (rest stream1) stream2))))

(fn append-map-streams (goal stream) ; applies "goal" to every member of "stream"
  (if (nil? stream)
        empty-stream
      (function? stream)
        (fn () (append-map-streams goal (stream)))
      (append-streams (goal (first stream)) (append-map-streams goal (rest stream)))))

(fn stream-pull (stream)
  (while (function? stream)
    (set stream (stream-pull (stream))))
  stream)

(fn stream-take (count stream)
  (if (nil? stream)
        nil
      (=? count 1)
        (list (first stream))
      (cons (first stream) (stream-take (and count (1- count)) (stream-pull (rest stream))))))

(fn call/initial-state (count goal)
  (stream-take count (stream-pull (goal micro-kanren-initial-bindings))))

(mc define-relation (name-and-arguments . goals)
  (let name      (first name-and-arguments)
       arguments (rest  name-and-arguments)
       bindings  (new-symbol)
    `(fn ,name ,arguments
       (fn (,bindings) (fn () ((conj ,@goals) ,bindings))))))

(fn ifte (condition_ then_ else_) ; if-condition-then-else
  (fn (bindings)
    (let (fn loop (condition_)
           (if (nil? condition_)
                 (else_ bindings)
               (function? condition_)
                 (fn () (loop (condition_)))
               (append-map-streams then_ condition_)))
     in  (loop (condition_ bindings)))))

(fn once (goal)
  (fn (bindings)
    (let (fn loop (stream)
           (if (nil? stream)
                 empty-stream
               (function? stream)
                 (fn () (loop (stream)))
               (list (first stream))))
     in  (loop (goal bindings)))))

(mc project (variables . goals)
  `(fn (bindings)
     (let ,@(mappend (fn (variable) `(,variable (walk* ,variable bindings))) variables)
      in  ((conj ,@goals) bindings))))

(mc disj (? . goals) ; zero or more goals
  (case (length goals)
      0 fail
      1 (first goals)
      (foldr (fn (goal rest) `(disj2 ,goal ,rest)) (last goals) (but-last goals))))

(mc conj (? . goals) ; zero or more goals
  (case (length goals)
      0 succeed
      1 (first goals)
      (foldr (fn (goal rest) `(conj2 ,goal ,rest)) (last goals) (but-last goals))))

(mc fresh (variables . goals) ; runs goals with newly created variables
  (foldr (fn (variable rest) `(call/fresh ',variable (fn (,variable) ,rest)))
         `(conj ,@goals)
         variables))

(fn walk* (value bindings)
  (let value (walk value bindings)
    (if (variable? value)
          value
        (pair? value)
          (cons (walk* (first value) bindings) (walk* (rest value) bindings))
        value)))

(fn reify (value)
  (fn (bindings)
    (let (fn make-reification-bindings (value bindings)

           (let (fn make-reification-name (index)
                  (coerce (format "_.~d" index) 'symbol))

            in  (if (variable? (set value (walk value bindings)))
                      (extend-bindings value (make-reification-name (length bindings)) bindings)
                    (pair? value)
                      (make-reification-bindings
                        (rest value)
                        (make-reification-bindings (first value) bindings))
                    bindings)))

         value (walk* value bindings)

     in  (walk* value (make-reification-bindings value nil)))))

(mc run (count goal-variables . goals) ; "goal-variables" may be a list of symbols, or a single symbol
  (let goal-variables (listify goal-variables) ; e.g., (x y z)
    (if (=? (length goal-variables) 1)
        `(let ,(first goal-variables) (make-variable ',(first goal-variables))  
           (map (reify ,(first goal-variables))
                (call/initial-state ,count (conj ,@goals))))
        (let goal-variable (new-symbol)
          `(run ,count
                ,goal-variable
                (fresh ,goal-variables (== ,goal-variable (list ,@goal-variables)) ,@goals))))))

(mc run* (goal-variables . goals)
  `(run nil ,goal-variables ,@goals))

(mc conde (? . goals) ; each goal is a goal-sequence. make the goals a disjunction of conjunctions
  `(disj ,@(map (fn (goal-sequence) `(conj ,@(listify goal-sequence))) goals)))

(mc conda (? . goals) ; committed choices
  ; each goal is a goal-sequence. just perform the first goal-sequence whose first goal succeeds
  (case (length goals)
      0 fail
      1 `(conj ,@goals)
      (foldr (fn (goal-sequence else_)
               `(ifte ,(first goal-sequence) (conj ,@(rest goal-sequence)) ,else_))
             `(conj ,@(last goals))
             (but-last goals))))

(mc condu (? . goals) ; committed choices, where the condition-clause succeeds only once
  `(conda ,@(map (fn (sequence) `((once ,(first sequence)) ,@(rest sequence))) goals)))

; symbol-macros
(sm rl   define-relation) ; for convenience
(sm oro  disj) ; more readable
(sm ando conj) ; more readable

[Dan Friedman]

My first reaction to leto was that "leto" was too weak.   

There is "named let," which I strenuously fought again, but I finally gave in.

There were simply no good words for the named-let construct.  If there were

to be such a word, it would have to "let*o", since, at least in principle, this should

be legal:  (let*o (x y z x) 

                  body*)

should have the meaning, as it does now with fresh

But, I do see your point and we hope to be writing a third edition, scheduling being quite an issue.

As for ando and oro.  Here, again, these are not user words, but implementation words.

We want no association with Bppleans.  Thinking that #s or #u has anything to do with #t and #f,

can destroy a person's viewpoint, in my opinion.   conj and disj are merely convenient macro names.

But, they could also be functions that take n-1 thunks, and of course, putting in the thunks could

be a macro.  

It is hard to teach old dogs new tricks is my last observation.  Perhaps if we had thought of it, we

would have used it.  Prior to fresh, we were using "exists", which on some level is better than fresh,

but seems too off-putting.  

I am flying soon, so I will be reading your code on the plane and will respond.  Since I was a Lisper,

before I was a Schemer, I am looking forward to reminiscing my way through your code.

Thanks for your kind words.

... Dan

--

[Dakota Fisher]

On 11/01/18 12:47, Dan Friedman wrote:
> It is hard to teach old dogs new tricks is my last observation. 
> Perhaps if we had thought of it, we
> would have used it.  Prior to fresh, we were using "exists", which on
> some level is better than fresh,
> but seems too off-putting.  
>

I'm interested, why did you decide on "fresh" as opposed to "exists"?

-Dakota

[Dan Friedman]

The primary motivation was the writing came out much easier to talk about.

Each conde line refreshes its variables.  Also, one syllable, and we wanted

to distinguish it from lexical variable and thought meta-variable and unification

variable did not belong in the language.  With regard to substitution.  What was

described is very different from what is a substitution.  Applying a substitution, walk

or walk*, never fails, but without the occurs-check, it could.  In most uses of an association

list, it can fail because something is not present in the lhs of s such a list.  So, here we felt

using the technical word made the most sense and it is only used as a data structure fof

the implementation.

... Dan