Should be the final value in b be a set or map?

Good catch. I’ve updated the above. Still gives the same result.

Right, then I'm stumped 😄

afaik set and hashmap unification is not supported by core.logic, feature extraction from hashmap is supported via featurec

Should be possible to translate a set to a finite domain constraint

@U0JUR9FPH, I just looked through the source. The problem is that core.logic only unifies sequentials and maps (and Lcons, which are special but replace Clojure’s lists to make improper lists work as in Scheme/Lisp). But (sequential? #{1 2}) ==> false, so it takes the case for Java Objects. If the two Objects aren’t =, then unification fails. And to be clear, no substructure is compared in the case of anything that takes the default Object path. So:

(run* [q]
      (== #{1 2} #{1 2}))
==> (_0)

(run* [q]
      (== #{1 2} #{2 1}))
==> (_0)

Note that sorted sets are also not sequential?, so that doesn’t help either.

@U487Z32UF, map unification is supported for map values, but not keys. All maps must have the same size and the same keys, otherwise unification fails. The values corresponding to equal keys are unified correctly. Thus:

(run* [q]
      (== {:a 1} {:a q}))
==> (1)

Interesting. Key unification was my next step in leveling up. Appears I need to learn other ways of making it work. Thanks for the insights!

My pleasure

BTW, thinking about this further, the behavior for sets is expected. Unification within the substructure of a collection relies on a consistent ordering or position. Core.logic can do that with maps as long as it just unifies against values and not keys. But sets, by definition, have no internal structure whatsoever. Any permutation of items in a set is equally valid. So, there's no real way to perform unification with ING the (entirely lacking) substructure. Summary: it basically has to work like this for sets.

I have not, but I think the kind of current favored approach is using equality saturation, which solves the problem of divergence that naive rewriting can have in core.logic

(rule says a = b, encounter a, rewrite to b, next step rewrites to a again, etc)

https://www.youtube.com/watch?v=LKELTEOFY-s is a nice talk about optimizing equality saturation, but it includes a nice explanation of what it is

https://github.com/clojure-numerics/expresso does look like it uses core.logic in someway

I had the misguided idea of trying to embed pi calculus in core.logic by embedding its production rules

Oh, sure, a kind of interpreter? That is a common thing done for the lamda calculus with minikanren. There are extensions to minikanren for working with languages and binders, and I believe core.logic includes some of that stuff, if you look around the code base for nom but I am not very familiar with that

http://webyrd.net/alphamk/alphamk.pdf is the alphakanren paper and https://github.com/clojure/core.logic/blob/master/src/main/clojure/clojure/core/logic/nominal.clj is the core.logic version

It might be better to start by just implementing regular evalo, too, if I'm writing an interpreter I should cut my teeth on something I more familiar first

Are you specifically looking to use core.logic, or would something like Meander fit? Meander has reasonable support for this and I’ve used it before to do transformation from a parsed Markdown representation to HTML via term rewriting and it worked quite reasonably.

I asked the same qs a while ago, you might want to check the thread below it : https://clojurians.slack.com/archives/C0566T2QY/p1635351009001600

I meant production more in terms of simplification grammars 🙃