[ANN] Logical: logic programming framework inspired by microKanren (0.1.0)

It’s only logical. - Spock

Logical is a minimalistic logic programming, which is

  • Simple implementation with only a few building blocks
  • Easy to understand and use
  • Supports negation free constraint logic programming by using Sets

It has a pretty decent readme, so if you are interested you should visit the repository.

The only future improvement, I’m thinking about now is also supporting (lazy) sequences in Logical, so negation free constraint system has a workable solution for infinit domains with a custom search strategy thanks to sequence generation.

I created this package mainly, because I couldn’t find any published microkanren based package, evethough there are some unpublished implementations. The other reason was that I want to experiment with how well can logic programming be used for business logic implementation.

It was my first time using Esy for a personal project and it was really easy to work with. I can only recommend it for others, because it makes the barrier to entry for others really low.

Links in readable form:


You may be interested in OCanren which also ports Kanren ideas into an OCaml EDSL (Embedded Domain-Specific Language).

1 Like

Am I missing something or your library doesn’t have the run function, which will actually perform the inference?

I looked at Ocanren, but I didn’t really try it out, because

  • it’s not published on opam
  • seemed a little bit heavy weight compared to what I wanted
  • I also found the examples a little bit too complex for my taste

I also looked at the other implementation minikanren-ocaml, which is also unfortunately not published on opam.

Inference is basically what the State.unify functions does if I’m correct and this function is used in every Goal.equal function and every complex goal is build upon equal, so it get’s run when goal is applied to a state. Also the original microKanren implementation also doesn’t have a run function, although it has it as a syntax extension.

I mostly followed this guide, although I also removed some stuff from it that seemed unnecessary for me. :grin:

Well, a declarative language without a solver is like a car without an engine. I would suggest you to follow the rest of the guide and actually implement the solver. You can even follow their approach and use enumerators, either via the Base’s Sequence module or via the Iter library. You can even pack this in a monad, to make it easier to use and extend.

@ivg Which parts do you recommend implement using solver and which without? I think that implementing arithmetic is worthwhile, but maybe something else?

Well, here by solver I didn’t really mean a SAT or SMT solver, but rather the procedure that will tight the stream of states into a fixed point, basically the run operator of this Logic monad. While the language will progress (if it will) more complex operations will require backtracking and state nondeterminism, which could be easily added by splicing in the Continuation and Multi State monads. At this point of time, a decision procedure that will drive the stream of events in some optimal way, will be required. This would be the time when we will start thinking about a non-trivial solver and ask ourselves such questions :slight_smile: So far, what I think is missing from the announced library, is the sequencing of states, which could be implemented directly using sequence or just hidden under the monad interface.

Ah, OK. We had some thoughs about adding SMT into Ocanren because resolving arithmetical constraints using Peano natural numbers (Succ+Zero) seem to be slow. So, I misunderstood.

Yep, you basically are thinking about the theory of bitvectors, something like QF_BV. I believe, that in general there is no good answer to the question on which part of the logic should be implemented as a theory and which reified into lower-level logics, that is why SMTLIB has its hierarchy of small theories and each particular application is making its own choice.

I followed the guide and implemented everything except the variables list and with_goal (and also Peano numbers) and I guess you meant the following code is missing form Logical:

class State
  def results(n)
      map { |variable| value_of(variable) }

  def result

I didn’t implement this, because it seemed like a syntactic sugar, which doesn’t really do much. This is also the reason why I removed the above mentioned things.

I’m not sure if you meant the above code or not, because based on the microKanren paper it’s basically a reifyer. Based on that paper the run and run* functions are just calls to reifyers with the first n result or with all of the results. Paper also mentions that reification is left to the user, so the user has more flexibility how to handle it.

microKanren paper: http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf