[PRL] space-saving tricks

[Dave Herman]

I'm working on a paper where I define the semantics of a language via 
translation to a target language which is an extension of the original 
language. The target language is almost exactly the same as the source 
language, except for one extra syntactic form and a couple new type rules.

When we write papers that describe a language incrementally, we describe 
later languages via extension of earlier ones, e.g.:

     e ::= ... | new form

This is meant to extend the definition of e. In my case, I want to 
define a language that is an extension of the first language, while 
still keeping it distinct from the first language. More concretely, it 
might look something like this:

     Source language:
         e ::= x | \x:T.e | e e
     Target language:
         e ::= ... | <T> e

This defines two different languages, and the latter is defined as an 
extension of the former (in the OO sense, i.e., it's an "open 
recursion") -- but this doesn't change the definition of the former.

Does that make sense? Does it seem clear enough? It seems a shame to 
completely rewrite the definitions, e.g.:

     Source language:
         e ::= x | \x:T.e | e e
     Target language:
         t ::= x | \x:T.t | t t | <T> t

Of course, the nice thing about the latter is that it's more honest and 
more explicit. Especially if you need to talk about the two languages at 
the same time and keep them separate. But in my case I'm really just 
talking about a simple translation from source to target language, and 
after that point I never deal with the source language.

Thanks,
Dave