core-logic 2019-03-12

Is it possible to use natural numbers in core.logic? i.e. define a relation (inco x y) for positive integers such that it succeeds when (inc x) = y

or do I have to resort to encoding Peano numbers via nested lists 😐

oops, so that's the entire purpose of clojure.core.logic.fd, I was thrown off by the word "finite"

the above would be (fd/+ x 1 y)

Does anyone know why the matche macro generates nested (fresh [] .. forms with no bindings?

Compared to an unrolled conde form without the nested freshes I've found it to run up to 50% slower

e.g.

(matche [a b c d e]
  ([1 2 3 4 5]))
macroexpands to
(conde
  ((fresh [] (== 1 a)
     (fresh [] (== 2 b)
       (fresh [] (== 3 c)
         (fresh [] (== 4 d)
           (fresh [] (== 5 e))))))))
which is equivalent to the un-nested:
(conde
  ((== 1 a) (== 2 b) (== 3 c) (== 4 d) (== 5 e)))

I imagine it just matches the recursive structure of the macro, which is often the simplest way to write a macro like that

to collapse it you end up needing to loop and accumulate and build a final form at the end, where as if defined recursively your macro just does a single step and lets the macro expander do the rest

oh, it isn't an artifact of the matche macro's recursive nature, but the recursive nature of the helper function ex*

the fresh isn't always empty

you can introduce a new logic var in a matche case

yeah, I realise that

but when matching against constants you end up with lots of empty fresh bindings all over the place

but the nested nature isn't great for that, I think

which results in a huge performance cost 😕

you might want to match with 'p' is multiple places being the same lvar

well, I guess it just doesn't reintroduce p so that works

I don't know much about the internals of core.logic, it seems like I can add a condition to the private ex function to optimize this case, but not sure if it might affect the correctness of other situations?

I am not sure either, the docstring for conde suggests some special handling of the first goal in a clause, which would suggest hoisting all those unifications to be goals in the clause would be different in some way, which would explain a large performance difference, but I don't see how it is the case that the first goal is anything special, so I don't know what the docstring is suggesting

Each fresh macro expands to a doubly nested fn, so I imagine that the performance difference was due to the overhead of traversing all those call stacks