mini-Kanren, core.logic, clojure: Reasoned Scheme Exercise 60

Question

This is NOT homework -- the solution is already in the text. I just failed to understand the solution.

Problem

(run* (q)
  (let [a (== true q)
        b (== false q)]
    b))

Correct Solution

(false)

My believed solution

()

My Confusion

Apparently the "a (== true q)" line is NOT executed, since only b is the goal. This confuses me. My mental model so far for logic programming has been:

• consider all possible assignemnts to q

• output the ones that manages to pass through the entire program

  Thus, the "a (== true q)" forces q = true, which makes it impossible to satisfy the "b (== false q)" line.

  However, apparently only "thigns needed to compute the goal" are executed. What's going on? What's the right mental execution model for core.logic / mini-kanren?

Thanks

(BTW, I'm clearly in the wrong, since mini-karen + core.logic agre with each other -- I just want to understand what I'm doing wrong.)

Hein

When your objective is to reach the goal, it is better to leave something that isn't related to your objective to reach the goal – Toastmaster

@Ankur: you're probably right. However, I don't understand it. Can you provide some insight on how "let" fits into the execution model of mini-kanren / core.logic? It's clearly that I do not understand what "let" means -- and it's clear that "let" means something else than in pure scheme/clojure. – Hein

Answer 1

== produces a goal. But you don't pass the a goal to run. So run doesn't know about it. A comparable situation is this:

(defn call [f] (f))

(call
  (let [a #(println "a")
        b #(println "b")]
    b))

The a function is created but not passed to call. So it is never executed.

Nestorius

This makes sense now, despite fooling around with the repl, I didn't realize that == returned functions. [I thought it was just some weird type/macro trick to make core.logic work.] – Hein