core-logic

Quentin Le Guennec 2021-12-12T11:45:48.057800Z

I'm looking for core.logic guides with real life examples (eg, math questions), does anyone know something that could help?

Ben Sless 2021-12-12T11:56:10.057900Z

I'd probably start here https://www.youtube.com/watch?v=iCuVTGWNU3s

Quentin Le Guennec 2021-12-12T13:48:54.058200Z

Thank you, I will ask questions in that channel if that's ok

πŸ‘ 1
Quentin Le Guennec 2021-12-12T13:49:47.059400Z

Is there a difference between (let [x (lvar)] goals... and (fresh [x] goals...) , when no x has been introduced in the run* expression before?

dgr 2021-12-12T16:04:29.069900Z

Yes, there is a difference. Fresh is a goal constructor (I.e. returns a function that takes a substitution/state and returns a stream of answers). A let form is not a goal constructor by itself. You would have to wrap the goals in a conjunction goal. In other words, it's close but not identical. I'm not close to the source at the moment, but you can macro expand fresh and see what's underneath. In microkanren, which is not core.logic, fresh basically maps to a call to a lambda where the parameter is a newly created lvar and the function is a goal constructor that returns a goal that is a conjunction of the goals in the fresh. I highly encourage you to read through the microkanren paper (see the papers section of http://minikanren.org. It's less than a page of source for the whole implementation and it will really help you understand what's happening under the hood.

Quentin Le Guennec 2021-12-12T16:31:32.070500Z

I see, thank you, it helped a lot.

πŸ‘ 1
Quentin Le Guennec 2021-12-12T15:46:02.060Z

Why doesn't this output [:c :f]?

(do
    (db-rel signal input output)
    (db
     [signal [:a :b :c :e :f] 0]
     [signal [:c :f] 1]
     [signal [:a :c :d :e :g] 2]
     [signal [:a :c :d :f :g] 3]
     [signal [:b :c :d :f] 4]
     [signal [:a :b :d :f :g] 5]
     [signal [:a :b :d :e :f :g] 6]
     [signal [:a :c :f] 7]
     [signal [:a :b :c :d :e :f :g] 8]
     [signal [:a :b :c :d :f :g] 9])
    (run* [q]
      (fresh [a b]
        (signal [a b] 1)
        (== q [a b]))))

Quentin Le Guennec 2021-12-12T15:53:13.060100Z

Got it, I forgot with-db

Quentin Le Guennec 2021-12-12T17:03:51.071600Z

Will two lvars defined like this: (lvar :a true) will be the same?

dgr 2021-12-12T18:41:09.071700Z

The REPL is your friend:

clojure.core.logic> (identical? (lvar :a true) (lvar :a true))
false
clojure.core.logic> (= (lvar :a true) (lvar :a true))
false
So, no. They are not the same and won’t compare as the same. You can see this in the printed representation:
clojure.core.logic> (lvar :a true)
<lvar::a__4588>
clojure.core.logic> (lvar :a true)
<lvar::a__4591>

dgr 2021-12-12T18:44:14.071900Z

If you look at the source, around line 714 you can see most of the creation paths use a unique counter to instantiate the lvar. You can force them to compare as equal using the false flag:

clojure.core.logic> (= (lvar :a false) (lvar :a false))
true
clojure.core.logic> (lvar :a false)
<lvar::a>
clojure.core.logic> (lvar :a false)
<lvar::a>

Quentin Le Guennec 2021-12-12T19:21:08.072200Z

I see, very helpful thank you.

Quentin Le Guennec 2021-12-12T20:10:34.073600Z

Is it safe to assume that run* returning '() means a contradiction in the goals?

Ben Sless 2021-12-12T20:11:46.073700Z

I think so. It means there is no substitution which meets the goals

Quentin Le Guennec 2021-12-12T20:12:18.073900Z

Okay, thank you

Quentin Le Guennec 2021-12-12T20:36:40.074800Z

I'm getting a stack overflow error with run*:

(StackOverflowError) at clojure.core.logic.Substitutions/walk (logic.clj:359)
Does that mean my constraint set is too broad?

Quentin Le Guennec 2021-12-12T21:07:17.075200Z

Oh nevermind, sets aren't supported.