Re: [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.

Thanks. I already made a lot of corrections and clarifications in response
to Cris and Dave, so the current version should look much better.

> - 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;

fixed

> - 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?

yes.

> 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;

done

> - 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).

why is it irrelevant?

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

maybe

> 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?


The problem is that if we do not use signatures then we have to split the
set of symbols into subsets. This introduces a lot of problems because
the names of these subsets will appear in BNF and then in XML. In the
extending dialects, the names of these subsets of symbols will make no
sense, so the XML serializations of the formulas in RIF basic logic dialect
will not be legal serializations in the upper dialects.

This is what I was trying to explain to Sandro also.


	--michael

Received on Tuesday, 24 July 2007 12:18:03 UTC