[racket] Redex: typesetting variable/label sets

On Oct 2, 2012, at 1:41 PM, Asumu Takikawa wrote:

> Hi all,
> 
> In PL papers, you often see grammars like the following:
> 
>  e ::= ... | λx.e | (e e)
>  x ∈ Var
> 
> In particular, variables are typeset as elements of some set. Often,
> there are other sets that might represent labels, locations, tags, and
> so on.
> 
> I don't see an obvious way to do this kind of typesetting in Redex. My
> first thought was to override the typesetting of forms like
> `variable-prefix` that I use for variables, but this doesn't work since
> I can't change the "::=" in the grammar.
> 
> Is my best option to manually build picts for these cases?


[[ Not an answer:

I consider the use of '::=' bad.  It is notation by people who don't understand mathematics. 

In mathematics '=' is used for both definitions, as in "let f(x) = x + 2", and equations, as in "find an x_0 st f(x_0) = 1". Indeed, you could argue that the first use is a second kind and you're solving for f and you get { (0,2), (1,3), ... } and you can replace all uses of f with this set. 

For grammars, e = x | (e e) has the same meaning. It's a (n inductive) definition of a set. Of if you so will, find the smallest fix point.

(I suggested the token for the in-code grammar as a compromise so that we could list several meta-vars on the left at once.) 

]]