Forgot to reply to the list, so I'm forwarding here. ---------- Forwarded message ---------- From: Paul van der Walt <paul.vanderw...@inria.fr> Date: Tue, Mar 31, 2015 at 12:06 PM Subject: Re: [racket-users] Using Redex To: Jonathan Schuster <schus...@ccs.neu.edu>
Hi Jonathan, Thanks for your response! I'm not sure if it'd be beneficial to cc: the mailing list, feel free to forward if excluding the ML wasn't intentional on your part. On 2015-03-31 at 17:44, quoth Jonathan Schuster: > Paul, my initial reaction is that this sounds like an odd use of Redex. Right. I was starting to get this suspicion too, as i went along with reading The Book and the tutorials available, etc. > Using your language terms to define implement-* macros is a valid > implementation strategy, Nice as a reality check indeed :) > but as a formal semantics it differs from the typcial Redex > approach. Yeah indeed. Notably the fact that the "image" of my language transformation is not the same as its domain makes me uneasy. What might have been possible is to model the output (that is, find an abstraction of defining macros etc) and have redex to that transformation. That way, the gap between what i eventually do in the implementation and the redex model is smaller. But it looks like actually i need to find an abstraction which is closer to the domain (the specification language). I guess in my case i should come up with some sort of mathematical/abstract model of the resulting components (e.g. a directed graph of communicating nodes) so that i can use that to prove properties (e.g. node A and B communicate iff that's in the specification terms). > It might be the case that Redex can help you develop a > separate formal semantics, though. Perhaps others on this list have > other thoughts or suggestions. Yeah, that is basically what i think i would like to do now, as a lite™ version of what i was trying to do. Or perhaps try and formalise one or two core components of my runtime system (but i'm less clear on how i could approach that. > Since you already have a working prototype, can I ask what benefit you're > hoping to get from Redex? There are certainly a number of possibilities, > but it depends on your goals. Mainly i would like to be able to make strong statements, such as "communication between component C1 and C2 is impossible, since they are independent in the specification". Currently i can argue that looking at the specifications of a set of components, but it becomes hand-wavey in the implementation -- i cannot *really* guarantee that there is no out-of-band communication except via intuitive arguments... Thank you very much for your comments! p. > On Sat, Mar 28, 2015 at 12:58 PM, Paul van der Walt < > paul.vanderw...@inria.fr> wrote: > >> Hello Racketeers, >> >> TLDR: I want to implement [1] using Redex. >> >> I hope somebody can shed some light on my problem. I'm trying to use >> Redex (which looks super cool, but i'm having trouble wrapping my head >> around all of it), and i'm a little stuck (i've tried RTFM, but i'm a >> little lost anyway). I wonder if what i'm trying to do is >> reasonable/feasible. >> >> I have a system which works, which i want to "reimplement" using Redex. >> My system (already in Racket) does the following: it provides a >> declaration language (just a set of keywords which aren't particularly >> relevant to the problem) which can be used to specify separate >> components expected in an application. It provides keywords like >> >> #lang myspeclang >> (define-component SomeName Int) ; declare a component >> >> This file should then be referred to by the "implementation module", so >> if the above is written in a file called specs.rkt, i provide a >> mechanism to write the following sort of terms: >> >> #lang "specs.rkt" >> (implement-SomeName (lambda () .....)) ; provide SomeName's implementation >> >> This is done by various macro tricks (nothing groundbreaking) -- i >> provide macros like the implement-SomeName above, depending on the >> declarations provided. >> >> Anyway, i am beginning to wonder if this type of thing can be expressed >> in Redex? I have a Redex model which specifies the grammar of my >> declarations, which i use to evaluate the declarations (thanks to David >> van Horn's approach [0]). I can see this working, but ultimately i'm not >> actually interested in a reduction relation per se: the declarations are >> already "reduced" and i'm interested in them only for their >> side-effects, e.g. defining a macro called "implement-SomeName" when a >> declaration for SomeName is encountered. I've been toying with this >> idea, and i'm worried i'd have to model (minimal) Racket itself in Redex >> to be able to express what these declarations should reduce to, but that >> (intuitively) sounds like the Wrong Way™ to go about things. My other >> idea was to add a "skip" terminal to the declaration language which >> everything reduces to, but as a side-effect running a bunch of code to >> define the needed macros. This also sounds Ugly©, though. Basically, my >> reduction goes from the domain of my declarations to the domain of >> macros or modules, and not, like in the schoolbook λ-calculus examples, >> from terms to terms in one language. >> >> Does anyone have a pointer towards something similar? Or insight into >> which Redex technique might be appropriate? Or a simple two-line email >> saying it's impossible? :p I have the PLT Redex book, but haven't got >> the impression my case fits well into one of the many examples. I would >> be happy to be told otherwise though. >> >> I'm sorry for the long-winded email, which probably still leaves details >> unclear. Don't hesitate to prod me for more details. There is a write-up >> of this exact system at [1], but it's perhaps a bit long for casual >> potential helpers to look at. >> >> Kind regards, >> p. >> >> 0. < >> https://groups.google.com/forum/#!searchin/racket-users/redex/racket-users/lKg-77Wh8M0/ULAxOHtENCQJ >> > >> 1. <http://people.bordeaux.inria.fr/pwalt/docs/decls.pdf> >> >> -- >> 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. >> For more options, visit https://groups.google.com/d/optout. >> -- 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. For more options, visit https://groups.google.com/d/optout.
