Re: Grammar presentation syntax FLD and BLD

Jos wrote:
>
> Dear all,
> 
> At the face-to-face I agreed to create a grammar for the presentation 
> syntax of FLD [2] which acknowledges the difference between atomic 
> formulas and terms in the productions, as well as a grammar for BLD [3] 
> that is a restriction of the FLD grammar.
> 
> When writing the grammar I came across a number of issues, which I 
> mention below.
> 
> Incidentally, I think there is a problem with the syntax for rules, as 
> specified in FLD.  Namely, a rule is an implication phi :- psi; no 
> quantification seems to be allowed. In the grammar below I also allowed 
> rules with universal quantification.

There are also quantified formulas. In FLD you can have arbitrary quantifiers.
I could have called phi :- psi a "Rule Implication" instead, but "Rule"
seemed shorter and acceptable.


> I included the noncontroversial part of the metadata proposal and the 
> built-ins. The production absolute-IRI is defined in [1].
> Incidentally, I also removed the Implies production, because I did not 
> really understand what it is for.

... snip ...

>    Const          ::= LITERAL '^^' SYMSPACE
>    Var            ::= '?' VARNAME
> 
> 
> I suppose that in the textual description which say that LITERAL and 
> VARNAME are sequences of Unicode characters.
> Actually, I would propose to make VARNAME just a sequence of 
> alphanumeric characters

Why limit? Suppose some language allows non-alphanums in variables?

> and to always delimit LITERAL with double quotes.

Yes, I agree.

> Then, it is not really clear from [2] what the syntax is of the names in 
> named-argument predicates and functions.  I would propose these names to 
> be absolute IRIs.

Are you talking about the names of the arguments or the names of the
predicates? For the former, Const is not right. They are ArgNames, where an
ArgName is a seq of unicode chars (again, why limit to alphanums?).
There is a mistake in the BNF (in the current version of the FLD/BLD document).
For the latter,  the pred names are Const'ants. As a special case, they can
be IRIs.

> Below is diagram restricted to the case of BLD.  Only three restrictions 
> were necessary:
> - a rule head may only be an atomic formula, not arbitrary condition
> - conditions may not contain negation  universal quantification
> - function and predicate identifiers may not be terms

... snip ...

> Another thing: why do we allow nesting of Forall statements in rules if 
> one can already specify multiple variables?
> I would propose to either remove the nesting or only allow mentioning of 
> 1 variable. I would prefer the former.

This is also a mistake in the current version of BNF in the document. Note
that the formal syntax does not allow that. (Of course, BNF defines a
superset of the language, so it is strictly speaking not a mistake :-)

Note that the formal syntax uses "universal" for what BNF calls a "rule".
These universals correspond to "Implies" in BNF. Unfortunately, Implies is
not so good, if FLD is taken into the account, since FLD can have two kinds
of "implies": :- and <-. Currently, <- is not used in FLD, but it could be,
so it is better to avoid the confusion.

Proposals for better names would be appreciated.


	--michael

Received on Friday, 29 February 2008 05:07:58 UTC