Just to clarify, I understand that the several binds of x correspond to the several patterns name in the productions, and the pattern against with we are matching, but I would have expected for the firsts to be discarded, or, if still considered in the resulting match for some reason, that I don't know, I would have expected for the application of the constraint of names, that would have rendered #f the match.
thanks!, Mallku El martes, 21 de diciembre de 2021 a las 17:38:28 UTC-3, Mallku Ernesto Soldevila Raffa escribió: > Hi to everyone!, > I'm trying to test the mechanization of Redex's semantics done in [1], > against the present version of racket, 8.3. I'm using the > random-match-test.rkt > > module from [1] to generate random grammars, patterns and terms, and to > test them > using the proposed mechanization of Redex in [1] and the actual > implementation of > it, in racket 8.3. > > In doing it, I've found an example that I cannot explain in terms of my > understanding > of the behavior of the name pattern: > > (define-language L [A (name x B)] > [B (hole (name x (hole hole)))]) > > (redex-match L (name x A) > (term (hole (hole hole)))) > > The result of the previous match is: > > (list (match (list > (bind 'A '(hole (hole hole))) > (bind 'x '(hole hole)) > (bind 'x '(hole (hole hole))) > (bind 'x '(hole (hole hole)))))) > > Which shows that 'x' is bound to different, non-equivalent, terms. While > I've never used the pattern name explicitly in such a way, while defining > grammars, I'm still curious about what is going on here. Even more, I would > have thought that the following match would return the same result as the > previous: > > (redex-match L (name x (name x B)) > (term (hole (hole hole)))) > > where I just replaced the non-term A by the rhs of its only production, but > what I obtain is: > > #f > > As a side note, the mechanization of Redex in [1] just returns something > equivalent to: > > (bind 'x '(hole (hole hole))) > > In both cases. Does anyone understand the behavior of the shown example > under racket 8.3? > > Thanks in advance!, > Mallku > > [1] : https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27 > El jueves, 9 de diciembre de 2021 a las 13:20:31 UTC-3, Mallku Ernesto > Soldevila Raffa escribió: > >> Thanks a lot for the info! If I found any mismatches, I'll report it. >> >> Regards, >> Mallku >> >> El miércoles, 8 de diciembre de 2021 a las 23:32:25 UTC-3, Robby Findler >> escribió: >> >>> I'm sorry, my sentence was ambiguous! I'm saying that I don't know of >>> any other work that is specifically focused on the semantics of Redex. (Of >>> course, there may be work I'm not aware of.) >>> >>> The paper is still a good match, I believe, yes. You're right that the >>> syntactic checks for well-formed grammars have tightened since that era, >>> but if the program is valid, then I think it should match; the underlying >>> algorithms have not changed, only bug fixes have happened. >>> >>> Of course, if you find that this isn't the case, I'd be very interested >>> to hear more :) >>> >>> Robby >>> >>> >>> >>> On Wed, Dec 8, 2021 at 6:34 PM Mallku Ernesto Soldevila Raffa < >>> [email protected]> wrote: >>> >>>> I beg your pardon!, I'm not understanding the answer, what is it that >>>> might be specific of Redex? >>>> >>>> I suspect that the answer is that there isn't some recent work on >>>> formal >>>> semantics specifically about Redex. In that case, does anybody know if >>>> the >>>> already mentioned paper [1] is still a good match for today's semantics >>>> of >>>> Redex? The paper provides a mechanization of the model in Redex, >>>> together >>>> with some tools to test it. Of interest is a tool that asks Redex to >>>> generate >>>> random patterns and terms that match against them, and tests if the >>>> mechanized model is capable of reproducing the matching (or that is what >>>> I suspect that the tests are doing :P ). It was possible to run the >>>> mechanization >>>> on a recent version of Redex, but the generated patterns are ill-formed >>>> (e.g., in-hole p1 p2, where p1 contains more than 1 hole). Of course I >>>> could >>>> provide more details about the error, but I don't know if it is of >>>> interest, it's >>>> a mechanization written for the Redex version that comes with Racket 5.* >>>> or something like that. >>>> >>>> Thanks!, >>>> Mallku >>>> >>>> >>>> [1] : https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27 >>>> >>>> El miércoles, 8 de diciembre de 2021 a las 21:03:44 UTC-3, Robby >>>> Findler escribió: >>>> >>>>> I think that might be it specifically about redex, I am sorry to say. >>>>> >>>>> Robby >>>>> >>>>> On Wed, Dec 8, 2021 at 5:28 PM Mallku Ernesto Soldevila Raffa < >>>>> [email protected]> wrote: >>>>> >>>>>> Hi community!, >>>>>> I'm interested in understanding the semantics of PLT Redex, since we >>>>>> are working on a tool >>>>>> to translate fragments of Redex models to Coq. At the moment, we just >>>>>> have a >>>>>> mechanization in Coq of the semantics proposed in a ~10 years old >>>>>> paper [1]. Does >>>>>> anybody know if there is an updated work on formal semantics of Redex? >>>>>> >>>>>> Thanks in advance!, >>>>>> Mallku >>>>>> >>>>>> [1] : >>>>>> https://link.springer.com/chapter/10.1007%2F978-3-642-25318-8_27 >>>>>> >>>>>> -- >>>>>> You received this message because you are subscribed to the Google >>>>>> Groups "Racket Users" group. >>>>>> To unsubscribe from this group and stop receiving emails from it, >>>>>> send an email to [email protected]. >>>>>> To view this discussion on the web visit >>>>>> https://groups.google.com/d/msgid/racket-users/d794dd4d-34c7-4de8-a4cd-a437dfcc630cn%40googlegroups.com >>>>>> >>>>>> <https://groups.google.com/d/msgid/racket-users/d794dd4d-34c7-4de8-a4cd-a437dfcc630cn%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>>> . >>>>>> >>>>> -- >>>> You received this message because you are subscribed to the Google >>>> Groups "Racket Users" group. >>>> To unsubscribe from this group and stop receiving emails from it, send >>>> an email to [email protected]. >>>> >>> To view this discussion on the web visit >>>> https://groups.google.com/d/msgid/racket-users/eba71355-dd8b-4eaa-8f0a-934a50d05ccen%40googlegroups.com >>>> >>>> <https://groups.google.com/d/msgid/racket-users/eba71355-dd8b-4eaa-8f0a-934a50d05ccen%40googlegroups.com?utm_medium=email&utm_source=footer> >>>> . >>>> >>> -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/1d7cb5b7-d7c2-44a7-b513-bb8280a54f13n%40googlegroups.com.
