Re: [racket-users] Formal semantics of PLT Redex
Wow!, that was fast! No need to thank, I'm just using your awesome tool to perform random testing. Thanks, Mallku El martes, 21 de diciembre de 2021 a las 18:22:09 UTC-3, Robby Findler escribió: > There was a bug in the matcher; I've pushed a fix. > > With that fix, you'll get > > (list > (match > (list >(bind 'A '(hole (hole hole))) >(bind 'x '(hole (hole hole)) > > as the result. That's different than the matcher because the pattern `A` > is really shorthand for something like `(name A (nt A))`, where the `name` > part introduces the name and the `nt` pattern matching construct matches > only non-terminals without binding a name. > > Thanks for finding the bug! > > Robby > > > On Tue, Dec 21, 2021 at 2:50 PM Mallku Ernesto Soldevila Raffa wrote: > >> 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 c
Re: [racket-users] Formal semantics of PLT Redex
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 < >>> mallku...@gmail.com> 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
Re: [racket-users] Formal semantics of PLT Redex
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 < >> mallku...@gmail.com> 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 < >>>> mallku...@gmail.com> 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
Re: [racket-users] Formal semantics of PLT Redex
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 < > mallku...@gmail.com> 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 < >>> mallku...@gmail.com> 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 racket-users...@googlegroups.com. >>>> 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_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 racket-users...@googlegroups.com. >> > 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_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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/14b8b2d5-41e8-4864-b194-e968a2043443n%40googlegroups.com.
Re: [racket-users] Formal semantics of PLT Redex
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 < > mallku...@gmail.com> 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 racket-users...@googlegroups.com. >> 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_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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/eba71355-dd8b-4eaa-8f0a-934a50d05ccen%40googlegroups.com.
[racket-users] Formal semantics of PLT Redex
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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/d794dd4d-34c7-4de8-a4cd-a437dfcc630cn%40googlegroups.com.
Re: [racket-users] Typesetting Redex definitions
Thank you very much for the information provided! We have a lot to experiment with. Regards, Mallku El martes, 26 de octubre de 2021 a las 18:40:49 UTC-3, Robby Findler escribió: > The only way to do that currently is to use the compound rewriters (they > rewrite anything with parens) and the atomic rewriters (they rewrite > anything without parens). The interface that redex provides is pretty > low-level and I'd like to find time to improve it, but in the meantime > there are some libraries on the package server that build higher-level ways > to do this. > > There's an example of with-compound-rewriter here: > https://docs.racket-lang.org/redex/reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._with-compound-rewriter%29%29 > > and redex doesn't care if the thing it is rewriting is defined as a > judgment form or as the syntax of a term; it'll apply the rewriter in > either case. > > As for what Redex generates, it isn't generating latex, it is generating > picts (which basically boils down to postscript-style drawing commands when > you think about them from the perspective of interoperating with other > tools -- one nice thing to do is to use scribble (which generates latex) as > it has handling to make them look nice in the rendered output, although > getting the right fonts set up can sometimes be tricky). > > hth, > Robby > > > On Tue, Oct 26, 2021 at 1:55 PM Mallku Ernesto Soldevila Raffa < > mallku...@gmail.com> wrote: > >> Hi community!, >> a colleague of mine is trying to typeset a grammar from a model in Redex, >> using redex/pict. So far, he has obtained a nice-looking typesetting of >> the productions, but with the inconvenience that they are not abstract. In >> particular, there are parentheses around every list of symbols, >> as in Redex. Since it seems that redex/pict does not generate the latex >> code >> (or does it?), we are not able to get rid of those concrete-syntax >> details. Is >> there any known/simple way of doing it? >> >> Thanks in advance!, >> Mallku >> >> -- >> 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 racket-users...@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/racket-users/3c6330fe-a048-4561-98bf-495c9b92e06an%40googlegroups.com >> >> <https://groups.google.com/d/msgid/racket-users/3c6330fe-a048-4561-98bf-495c9b92e06an%40googlegroups.com?utm_medium=email_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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/f405ba3e-559d-43f5-9df6-2b061c9277d0n%40googlegroups.com.
[racket-users] Typesetting Redex definitions
Hi community!, a colleague of mine is trying to typeset a grammar from a model in Redex, using redex/pict. So far, he has obtained a nice-looking typesetting of the productions, but with the inconvenience that they are not abstract. In particular, there are parentheses around every list of symbols, as in Redex. Since it seems that redex/pict does not generate the latex code (or does it?), we are not able to get rid of those concrete-syntax details. Is there any known/simple way of doing it? Thanks in advance!, Mallku -- 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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/3c6330fe-a048-4561-98bf-495c9b92e06an%40googlegroups.com.
