Thanks for the replies from you two -  Mick and David.

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 David 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 related to the interesting fact that the human brain can 
grasp that there are 4 items in view, but as soon as there are 5 items, the 
brain must 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

-- 
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 [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/minikanren.
For more options, visit https://groups.google.com/d/optout.

Reply via email to