[racket-dev] redex metafunction contract for two separate languages?

On Feb 7, 2012, at 11:21 AM, Sam Tobin-Hochstadt wrote:

> 
> In most papers that I see, nothing other than context would
> disambiguate them, and that would be plenty.
> 
> For example, take the following paper:
> http://dl.acm.org/citation.cfm?doid=1596550.1596592
> 
> That paper has a large number of metafunctions between different
> languages, and (a) doesn't disambiguate between which language is
> which, and (b) avoids the problems listed here by using different
> non-terminal names, and all of it is fine.  I spent a lot of time with
> this paper, and none of these issues were confusing.  See, for
> example, the metafunctions on page 8.


Robby is asking specifically about the case when L1 and L2 both
use non-terminal e (say to denote expressions) and translations
from L1 e to L2 e are needed. 

This kind of same-name problem will show up in Redex models, 
because when you program you think of systematic naming inside
of modules (languages plus functions) and across modules. When 
you write papers, you are much more interested in disambiguating 
names for readers. 

Redex can help in these situations to disambiguate and to make
naming conventions systematic -- if the modeler so chooses. 

-- Matthias