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.)
]]
____________________
Racket Users list:
http://lists.racket-lang.org/users
