Re: BLD: two issues with the BNF

On Thu, 10 Jul 2008 14:23:54 +0200
Jos de Bruijn <debruijn@inf.unibz.it> wrote:

> I uncovered two issues with the BNF in BLD.  For me they are not 
> critical for last call, but for some they might be.

Jos,
thanks for uncovering these inconsistencies.

> The first issue is an error: Profile is not a Unicode string in the 
> presentation syntax, but it is a term (see section 2.4).

Yes, this is how it is defined in the math syntax, but EBNF is not consistent
with this. But looking at your SWC, your profiles are not terms either. They
are not even constants! So, let's decide what we want them to be.
A term as a profile is very general and will suffice for all future needs. But
this may also turn out to be an overkill. A constant is more like what you need
right now. But what you are using is really a bunch of ASCII strings - not
terms and not constants.

> The second issue is not an error, but it can be considered misleading 
> (the BNF is too liberal): in the presentation syntax, rules are 
> quantified rule implications.  So, an atomic formula is not a rule and 
> may thus not be directly included in a group.  According to the BNF, an 
> atomic formula can be considered a rule; this is misleading.

There was a mistake in the math syntax. Groups should also allow atomic
formulas. Fixed.

m

> 
> Best, Jos

Received on Thursday, 10 July 2008 18:04:50 UTC