[BLD] Signatures (BLD 7/20)

Michael,

I had to strugle to understand the formal syntax for signatures in the 
BLD draft. Here are a few suggestions that may make it easier to 
understand. I am refering to section 2.1.1.1 in the version of BLD 
produced by wiki-tr on July 20.

- First, I agree with Chris that the use of 's', first for signature 
names, then for a set of signature -in defining a coherent set of 
signatures-, and finally for symbols in "well-formed terms and formulas" 
is quite confusing;

- Signature expressions: is my understanding that signature expressions
are always in the form (s1 ... sn) -> s, and that the "s above" in the 
sentence "If s above is bool then the signature is called a Boolean 
signature" is the s in (s1 ... sn) -> s?

If yes, it implies, as Chris pointed out that boolean signature 
expressions are a subset of arrow signature expressions, right?

Maybe rewriting the def of boolean signature expression could make these 
clearer:
"Arrow and Boolean signature expressions are defined as follows:
   * Arrow signature expressions are expressions of the form (s1 ... sn) 
-> s, where s1, ..., sn, and s are signature names from SigNames and 
where n >= 0. In particular ...;
   * Boolean signature expressions are arrow signature expressions where 
s is bool, that is: (s1 ... sn) -> bool, where s1, ..., sn are signature 
names from SigNames and n >= 0."

- You define a signature as a statement of the form s{e1 ... en} with s 
a name in SigName, and a signature expression as a statement of the form 
(s1 ... sm) -> s, with si and s signature names from SigNames: since the 
2 's' are not related, it may be clearer to use different symbols;

- In 2.1.3, the remark that f() and f can be interpreted differently and 
dialect may introduce axioms to make them equal should be clearly marked 
as irrelevant to BLD (where symbol f has either signature f0 or i, but 
not both).

Or maybe I just did not understand it yet...

Also, I do not clearly understand why you need to introduce the 
signatures at this stage, although you need them only for future 
extensions: is it to make sure that all the extensions that will need 
them, even divergent ones, use the same formal syntax? In any case, what 
is general should be more clearly separated from what is specific to 
BLD. If it needs be common to all dialects, maybe it should go in the 
Arch document?

Christian

Received on Tuesday, 24 July 2007 11:59:33 UTC