Stray thoughts about the possibilities of miniKanren with LVars

[Jonas Kölker]

Lindsey Kuper has done some work on LVars that people may be familiar with:

• https://hackage.haskell.org/package/lvish
  
• https://www.youtube.com/watch?v=8dFO5Ir0xqY
  

Short summary: if you have a parallel program in which all data is in a semi-lattice and all writes are monotonic (i.e. x <= y whenever x is overwritten with y), and you don't read any variables except when returning a result, the result is always the same no matter what the scheduling decisions are. In particular, miniKanren's substitution dictionary a lattice and unification is a monotonic write, so we get for free some theorem saying that miniKanren has a lot of freedom when deciding in which order to process goals.

Furthermore, such a parallel program over lattice data can also do threshold reads, and maintain determinism. A threshold read is a operation which takes a variable and a set of values {x_1, ..., x_n}, such that for any pair x_i and x_j, there is no value x' such that x_i <= x' and x_j <= x' except the top of the lattice. The read blocks until the variable takes a value at or above of the x_i's, then returns the x_i (which might or might not equal the value of the variable).  In the obvious application in miniKanren, the values we're talking about are sets of scheme-values that a logic variable could be bound to, and the ordering is is-superset-of. So for example, {x | (number? x)} <= {5}. The least upper bound is the intersection of two sets.

I've observed that one cannot really read in miniKanren; the closest thing to reading whether x=3 is to <write x=3 or else destroy the universe>.

It's not clear to me, but I think it would be interesting to find out: would adding threshold reads allow MK to do something that it couldn't (easily) do without them?

The first application that comes to mind has to do with program synthesis: run the relational interpreter for synthesis, and "in parallel" do a threshold read waiting for the program to become somewhat specified; when the read unblocks, run a type checker/inferencer on the specified parts of the program.

If this works, then maybe the general principle is: being able to defer sub-programs until particular threshold reads unblock allows for greater modularity: you wouldn't need to weave the type checker and interpreter together into one, but could keep them separate.

Now, if the program is instantiated to "a lambda application", `(,a ,b), there's not a whole lot you can type-check just yet, so the recursive self-calls in the type checker would need to be guarded with threshold reads on the sub-parts of the program. Probably one can abstract away whether the recursive calls are done immediately or after a threshold read by doing some kind of program transformation by either hand or macro.

I noticed that Will has an experimental implementation of minikanren-with-lvars at https://github.com/webyrd/latticeKanren; Will, have you thought about what the possibilities are? What are your impressions so far? Everyone else, what do you think the implications of threshold reads are?

[Greg Rosenblatt]

Hi Jonas,

You've made some good observations.  I haven't thought of this in terms of threshold reads before, but what you're describing sounds like the implementation of deferred goals in some MK variants.

Deferred goals are resumed when the variables they depend on become known, which should be able to support dynamic interleaving, as in your interpreter/type-inferencer example.  A few of us have been experimenting with exactly this example in dKanren, though it's not working well enough to be useful yet.

--
You received this message because you are subscribed to the Google Groups "minikanren" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minikanren+unsubscribe@googlegroups.com.
To post to this group, send email to minik...@googlegroups.com.
Visit this group at https://groups.google.com/group/minikanren.
For more options, visit https://groups.google.com/d/optout.

[Jonas Kölker]

You've made some good observations.  I haven't thought of this in terms of threshold reads before, but what you're describing sounds like the implementation of deferred goals in some MK variants.

Deferred goals are resumed when the variables they depend on become known, which should be able to support dynamic interleaving, as in your interpreter/type-inferencer example.

Yep, that sounds like a threshold read. What does "known" mean? Fully ground, or just non-fresh?

In the former case, the tripwire set would be {{x} | x is any value}; in the latter case, ignoring constraints for the moment, I think it would be something like [{x} for all non-compound values x] ++ [{ x | x equals (cons <anything> <anything>) }], where 'cons' is the only compound-value constructor.

I suspect it's easy to prove that you can also defer until symbolo/numbero constraints are applied, if you're happy with a more coarse-grained read; then the tripwire is [{x | x is a symbol}, {x | x is a number}, {x | x is a cons}] ++ [{x} for all non-number, non-symbol, non-compound values x].

I guess one immediate conclusion is: if "known" means threshold-reading a valid tripwire set, Lindsey Kuper has proven that you're free to schedule goals in any way you like without changing the results of the user's program. [Completeness of the search still requires attention.]

It's not working well enough to be useful yet.

Interesting; what are its shortcomings? 

[Greg Rosenblatt]

On Sunday, August 20, 2017 at 6:28:59 AM UTC-4, Jonas Kölker wrote:

You've made some good observations.  I haven't thought of this in terms of threshold reads before, but what you're describing sounds like the implementation of deferred goals in some MK variants.

Deferred goals are resumed when the variables they depend on become known, which should be able to support dynamic interleaving, as in your interpreter/type-inferencer example.

Yep, that sounds like a threshold read. What does "known" mean? Fully ground, or just non-fresh?

As soon as any information becomes known (so symbolo and numbero qualify for this case), a goal is resumed.  If the new information turns out to be insufficient, the goal may suspend itself again right away.  In a lot of cases, it will use the new information to perform some simplification before re-suspending.  You could say there are implicit tripwires.

 

It's not working well enough to be useful yet.

Interesting; what are its shortcomings? 

It seems to be due to bad implementation on my part.  I haven't had time to dig in to figure out why, but the scheduling of goals isn't distributed in the way we expected.  Once this is fixed, I imagine there won't be any serious shortcomings.  It will take a while to get back to this, but I'll let you know when I find out.

[William Byrd]

Hi Jonas!

I agree with you that there seem to be many similarities between LVars
and miniKanren! I think you could build a miniKanren-like system on
top of an LVars-like system, and also, as you point out, mix ideas
between the two systems. More generally, the concepts of lattices pop
up all over programming languages (static analysis, fixpoint finding,
unification, tree automata, incremental computation, etc.). A more
general, lattice-oriented approach to programming might subsume many
or all of these tasks.

I need to look at the latest version of the LVars work. When I was
looking for connections with Lindsey and Ryan, years ago, the LVars
formalism was missing a feature or two that I wanted for implementing
miniKanren-in-LVars.

I agree with Greg that there is a connection between these ideas and
delayed goals (which are helpful in many contexts involving logic
programming--for example, in probKanren, and in this paper
https://lirias.kuleuven.be/bitstream/123456789/166921/1/ESOP90.pdf).
I think, though, that there may be other ways to mix this ideas, for
distributed computation, etc., that might have a different feel than
the standard approach to delayed goals.

This is definitely worth thinking about more! Here is my challenge to
you: using the latest version of LVish, implement miniKanren (or
microKanren) using LVars! I'll bet you can do it now!

Cheers,

--Will

> --
> You received this message because you are subscribed to the Google Groups
> "minikanren" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to minikanren+...@googlegroups.com.

[Jonas Kölker]

Hi Will :-)

 

I agree with you that there seem to be many similarities between LVars
and miniKanren!  I think you could build a miniKanren-like system on
top of an LVars-like system, and also, as you point out, mix ideas
between the two systems.

I see two potential benefits: either an extremely short MK implementation (because MK is basically LVars plus conde minus threshold reads), or a better and more capable MK.

The one thing that's not clear to me is how you do disjunction and multiple results. Can you clone the store? IIRC the Haskell library implements the key data structures backend by mutable data on the plain ol' heap, which suggests "no".

The key concepts of LVars could be implemented by an alist/path-copying-HAMT/etc. backing; in that case disjunction appears easier.

 

the concepts of lattices ... [static analysis] [...]

Oh yeah, I vaguely remember that class. Thanks for prodding at my memory.

 

When I was looking for connections with Lindsey and Ryan, years ago ...

 

That's the repo I linked to?

 

the LVars formalism was missing a feature or two that I wanted for implementing miniKanren-in-LVars.

Something to do with disjunction? Or something else?

 

I agree with Greg that there is a connection between these ideas and delayed goals

Sure sounds like it to me :) One can rephrase "blocking threshold read" as "delay until the value is above any one of {x, y, z}, then tell me which", so... yeah.

 

This is definitely worth thinking about more!  Here is my challenge to
you:  using the latest version of LVish, implement miniKanren (or
microKanren) using LVars!  I'll bet you can do it now!

I appreciate the encouragement, but it'll have to come after my current toy projects, which are (1) a miniKanren in TypeScript (working-but-messy, but for one well-understood bug); (2) a miniKanren search tree visualizer, perhaps growing out of no. 1; and (3) some kind of propositional calculus workbench, with a theorem prover, axiom independence prover and soundness checker, tautology enumerator just for shits and giggles, perhaps some flavor of datalog to query streams of formulae; all it needs is a raison d'être and plenty of time :D

 

I think it would be interesting to combine the top-down proof search strategy of my current theorem prover with the bottom-up approach of BFS-ish iterated condensed detachment. Anyways, that's veering off topic.

Cheers,

Jonas

[Greg Rosenblatt]

The one thing that's not clear to me is how you do disjunction and multiple results. Can you clone the store? IIRC the Haskell library implements the key data structures backend by mutable data on the plain ol' heap, which suggests "no".

The key concepts of LVars could be implemented by an alist/path-copying-HAMT/etc. backing; in that case disjunction appears easier.

I'm not familiar with this Haskell library, but our implementations use an immutable data structure for the store.  Barliman's implementation uses an array-mapped-trie (no hashing necessary, variables are created with unique indices).  You're right that this makes disjunction pretty easy.

 

I appreciate the encouragement, but it'll have to come after my current toy projects, which are (1) a miniKanren in TypeScript (working-but-messy, but for one well-understood bug); (2) a miniKanren search tree visualizer, perhaps growing out of no. 1; and (3) some kind of propositional calculus workbench, with a theorem prover, axiom independence prover and soundness checker, tautology enumerator just for shits and giggles, perhaps some flavor of datalog to query streams of formulae; all it needs is a raison d'être and plenty of time :D

 

I think it would be interesting to combine the top-down proof search strategy of my current theorem prover with the bottom-up approach of BFS-ish iterated condensed detachment. Anyways, that's veering off topic.

These projects sound pretty interesting.  I'm interested in hearing about them in more detail, if you're willing to share.  A lot of it sounds on-topic for this group.

[Jonas Kölker]

These projects sound pretty interesting.  I'm interested in hearing about them in more detail, if you're willing to share.  A lot of it sounds on-topic for this group.

Sure. It's off-topic for this thread, so I posted a lot of words in a separate thread. I hope you'll enjoy reading them :)