# [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.)
]]