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 On Sat, Aug 19, 2017 at 6:30 PM, 'Jonas Kölker' via minikanren <[email protected]> wrote: > 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? > > -- > 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 [email protected]. > To post to this group, send email to [email protected]. > Visit this group at https://groups.google.com/group/minikanren. > For more options, visit https://groups.google.com/d/optout. -- 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/minikanren. For more options, visit https://groups.google.com/d/optout.
