Michael is correct Le 20 juin 2017 06:27, "Michael Ballantyne" <[email protected]> a écrit :
I think he meant that the situation he was worried about can't actually cause a bug. This bit: "you discover part of final prefix which can profit from set-var-val optimization and later whole unification fails" So, something like: (fresh (x) (== (cons x x) (cons 1 2))) The set-var-val! optimization performs a side-effect on x that it seems like we might need to roll back when the unification fails, but ultimately it doesn't matter because when the unification fails we throw away all references to x. On Mon, Jun 19, 2017 at 8:32 PM Dan Friedman <[email protected]> wrote: > Dmitrii, > > Can you explain exactly what is impossible to achieve and its implications. > > ... Dan > > On Fri, Jun 16, 2017 at 2:05 PM, Dmitrii Kosarev < > [email protected]> wrote: > >> Actually, after some hours it seems that it is impossible to achieve. If >> it happens just after conde the scope is changed and nothing will go into >> the variable. And if it happens just after fresh than the fail will not >> affect anything be cause it will be nothing done in future with variables >> just created. >> >> >> >> On Friday, June 16, 2017 at 4:22:50 PM UTC+3, Dmitrii Kosarev wrote: >>> >>> Hey, Michael and all >>> >>> I have some issues about set-var-val optimization and unification. What >>> happens when you discover part of final prefix which can profit from >>> set-var-val optimization and later whole unification fails? It seems that >>> the one needs to rollback this set-var-val mutation after detecting failure >>> or should postpone set-var-val optimization and apply the prefix in the end >>> of successful unification. I can't detect neither of this approaches in the >>> code of faster-miniKanren. Can you clarify this? >>> >>> Related code lines >>> https://github.com/michaelballantyne/faster- >>> miniKanren/blob/master/mk.scm#L91 >>> https://github.com/michaelballantyne/faster- >>> miniKanren/blob/master/mk.scm#L211 >>> https://github.com/michaelballantyne/faster- >>> miniKanren/blob/master/mk.scm#L228 >>> >>> Best regards, >>> Dmitrii >>> >>> >>> On Wednesday, March 22, 2017 at 10:03:46 AM UTC+3, Michael Ballantyne >>> wrote: >>>> >>>> Oddly enough, I wasn't a member of this list so I didn't see your >>>> message until Jason Hemann helpfully forwarded it on to me. >>>> >>>> All of what Will writes matches my understanding, and I've written up >>>> some more down in the weeds details on the repository README: >>>> https://github.com/michaelballantyne/faster- >>>> miniKanren#what-makes-it-fast >>>> >>>> If you have further questions after reading, I'd be happy to chat >>>> during one of the hangouts or via email. >>>> >>>> >>>> On Tuesday, March 21, 2017 at 9:59:50 AM UTC-6, William Byrd wrote: >>>>> >>>>> Hi Dmitrii! >>>>> >>>>> I'll give a brief answer now. I hope Michael Ballantyne will give a >>>>> more detailed explanation. I hope Michael will also go over the >>>>> faster-miniKanren implementation during one of the upcoming hangouts. >>>>> >>>>> As I recall, there are three main reasons faster-miniKanren is faster >>>>> than previous implementations: >>>>> >>>>> 1) use of efficient immutable data structures, rather than association >>>>> lists, to implement the substitution, etc. There are other miniKanren >>>>> implementations that do this. For a detailed exploration of how >>>>> different data structures perform, please see this unpublished paper: >>>>> >>>>> https://www.cs.indiana.edu/~lkuper/papers/walk.pdf >>>>> >>>>> faster-miniKanren doesn't use the absolutely fastest representation, >>>>> at least as described in that paper, but any efficient representation >>>>> will perform much better than association lists for most real >>>>> miniKanren programs. >>>>> >>>>> 2) use of attributed variables to represent constraints. That is, >>>>> constraints other than unification (disequality, absento, numbero, >>>>> symbolo) are associated with logic variables, rather than just being >>>>> put in a list as in the original cKanren. The advantage is that it is >>>>> quick and easy to determine which constraints are involved in a given >>>>> unification. Compare this with the older approach, in which the >>>>> entire constraint store might be checked, even when unifying variables >>>>> that don't have constraints associated with them. >>>>> >>>>> This is a huge win for programs that make heavy use of constraints, >>>>> such as relational interpreters. >>>>> >>>>> As a historical note, I must take the blame for the inefficient >>>>> approach used in the original cKanren. Jeremiah Willcock suggested we >>>>> use attributed variables from the very beginning, and Claire and Dan >>>>> wanted to use them. I wasn't convinced that we'd be able to represent >>>>> all of our constraints using attributed variables, and advocated for >>>>> the slower, list-based constraint approach. I was wrong. >>>>> >>>>> I believe core.logic uses attributed variables, or something >>>>> equivalent, but I'm not sure. Michael Ballantyne wrote a very nice >>>>> implementation of our constraints using attributed variables for >>>>> faster-mk. I'm not sure if Claire used attributed variables in >>>>> Kraken, the successor to cKanren. >>>>> >>>>> Another possibility would be to implement constraints using Constraint >>>>> Handling Rules (CHR). I think Claire explored this approach for >>>>> Kraken. >>>>> >>>>> 3) Michael Ballantyne suggested another optimization, which, to my >>>>> knowledge, is only used in faster-miniKanren. Michael noticed that >>>>> many times logic variables are unified immediately after they are >>>>> created with a 'fresh'. In these cases it is not necessary to extend >>>>> the substitution. Instead, we can just mutate a structure >>>>> representing the variable (using a local mutation that is harmless). >>>>> This is the intent of the 'scope'-related comments in the code: >>>>> >>>>> https://github.com/webyrd/faster-miniKanren/blob/master/mk.scm >>>>> >>>>> Look at the definition of 'subst-add', in particular: >>>>> >>>>> ; set-var-val! optimization: set the value directly on the variable >>>>> ; object if we haven't branched since its creation >>>>> ; (the scope of the variable and the substitution are the same). >>>>> ; Otherwise extend the substitution mapping. >>>>> >>>>> I hope Michael will jump in and explain this optimization in more >>>>> detail. >>>>> >>>>> Hope this helps! >>>>> >>>>> --Will >>>>> >>>>> >>>>> On Mon, Mar 20, 2017 at 5:17 AM, Dmitrii Kosarev >>>>> <[email protected]> wrote: >>>>> > Hey, folks >>>>> > >>>>> > Can you describe why faster miniKanren [1] is.. em... faster than >>>>> every >>>>> > think else? I believe that it's true because I measured. Can you put >>>>> this >>>>> > very useful information in the repo description? What should I do to >>>>> make >>>>> > microKanren work in the same manner as faster miniKanren. >>>>> > >>>>> > Happy hacking, >>>>> > Dmitrii >>>>> > >>>>> > >>>>> > [1] https://github.com/michaelballantyne/faster-miniKanren >>>>> > >>>>> > -- >>>>> > 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. >> > -- > You received this message because you are subscribed to a topic in the > Google Groups "minikanren" group. > To unsubscribe from this topic, visit https://groups.google.com/d/ > topic/minikanren/NxF15WnfEXk/unsubscribe. > To unsubscribe from this group and all its topics, 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 a topic in the Google Groups "minikanren" group. To unsubscribe from this topic, visit https://groups.google.com/d/ topic/minikanren/NxF15WnfEXk/unsubscribe. To unsubscribe from this group and all its topics, 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.
