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. On Sat, Aug 19, 2017 at 8: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.
