Re: Discussion on flattening

[Andrzej Tarlecki <tarlecki@mimuw.edu.pl>]

Just picking out one paragraph from Maura's message, to avoid
misinterpretation of what I wrote in this particular context:

> The same happens, for instance, in the productions for BASIC-ITEM.
> Why should we distinguish among SIG-DECL and VAR-DECL, AXIOM...? Why not to
> group all the declarations and all the property requirements and have
> BASIC-ITEM::=DECL | PROPERTY
> DECL::=SORT-DECL |...|VAR-DECL
> PROPERTY::= AXIOM | SORT-GEN
> or no distinction at all, all kinds of basic-items flattened at one level?

Actually, there is a "serious" semantic distinction between SIG-DECs,
VAR-DECLs and AXIOMs. Namely, only SIG-DECLs introduce elements of a
signature (without adding variables), VAR-DECLs do not contribute to
the signature and only add variables to be used in a special way when
interpreting the axioms (and AXIOMs only restrict the class of
models). Consequently, the coercion from SIG-DECL to BASIC-ITEM is
non-trivial in the current semantics, which in our view nicely
indicates their very special and pure role as signature forming
declarations (later on cluttered by other ugly declarations like those
of variables :-).

Best regards,

Andrzej