core-logic

2021-12-08T14:44:26.042Z

Hi, I’m trying to understand some core logic basics. Based on the tutorial, I can do this (and it makes sense):

(run* [q r]
      (== {:a q :b r} {:a 1 :b 2}))
;=> ([1 2])
What I want to do is this:
(run* [a b c]
      (== {:a #{1 2} :b #{2 3}}
          {:a #{a b} :b #{b c}}))
;=> ()
I would naively hope for ([1 2 3]) instead of (). How can I recast this to make it work?

Ben Sless 2021-12-08T14:54:40.042200Z

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

2021-12-08T15:12:00.042500Z

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

Ben Sless 2021-12-08T15:39:00.042800Z

Right, then I'm stumped 😄

paulocuneo 2021-12-08T15:51:02.043Z

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

Ben Sless 2021-12-08T15:51:52.043200Z

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

👍 1
dgr 2021-12-11T15:20:01.055800Z

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.

dgr 2021-12-10T23:12:40.047600Z

@markbastian, 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)
works as expected, as does:
(run* [q]
      (== #{1 2} #{2 1}))
==> (_0)
because sets can be compared for equality irrespective of how items are ordered. But sets are just compared, they are not truly unified. See the code around line 900 in the main core.logic source file.

dgr 2021-12-10T23:17:38.048300Z

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

dgr 2021-12-10T23:23:56.048800Z

@paulocuneo, 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)

👍 1
2021-12-10T23:31:36.049Z

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!

👍 1
dgr 2021-12-11T00:04:26.049300Z

My pleasure

Ben Sless 2021-12-08T14:57:01.042400Z

Anyone ever written production rules or term rewriting with core logic? Can you share an example or approaches?

Ngoc Khuat 2021-12-12T08:23:36.056Z

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

Ben Sless 2021-12-12T09:28:06.056300Z

I meant production more in terms of simplification grammars 🙃

2021-12-09T00:45:09.044800Z

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

2021-12-09T00:45:50.045Z

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

2021-12-09T00:47:11.045200Z

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

2021-12-09T00:57:52.045500Z

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

Ben Sless 2021-12-09T04:57:34.045800Z

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

2021-12-09T05:05:07.046Z

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

2021-12-09T05:09:02.046200Z

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

👍 1
👀 1
Ben Sless 2021-12-09T05:24:01.046500Z

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

dgr 2021-12-10T22:38:38.047200Z

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.