[racket] Transitively extend redex metafunctions

On 12/7/12 7:49 PM, Robby Findler wrote:
> This is an excellent example of one of the reasons why we'd planned to
> add a notion of modules to Redex. The idea being that you could group
> a bunch of metafunctions/judgment-forms/reduction relations together
> and then simultaneously extend the set of them to a new language.

This would be excellent and I think is exactly what's right for the 
models I'm working on now.

> Unfortunately, there isn't a way to do what you're asking at the
> moment-- not because the underlying facility isn't there, but because
> as you note, the helper function can't be redirected to the new one.
>
> Matthias recently suggested an imperative form of extension, where you
> could mutate a function so that it now works in a large language.
>
> Would something like that help in your case, or would you want to keep
> all of the different versions of these functions around?

Hmmm.  If I could typeset things incrementally, the way I can now, I 
believe that would be fine.  (Although I can certainly imagine when it's 
important to have the functions around: suppose you want to prove a 
theorem about some relationship between a language and its extension -- 
you'd need both sets of metafunctions to test the theorem.)

It sounds like the right thing for me to do in the meantime is define 
all of my metafunctions for the largest language and typeset things by 
selecting the cases for the subsets of each smaller language.

By the way, a small, good example of where this problem pops up is in a 
language with expressions and statements, defined by mutual induction. 
If you have a well-formedness judgment (e.g., a typing relation), it's 
going to be in the form of two mutually recursive judgments.  If you add 
a new kind of expression or statement, the judgment can't be extended. 
(This is why I asked about local metafunctions.)

David