CORE WD - a few remarks

Dear Harold, dear Michael,

Having a flue, I could spend time carefully reading the CORE working 
Draft. Impressive work! Below are a few remarks on this document in two 
lists: principles and style. I hope, my remarks are clear enough. If 
not, please, tel me!

Regards,

François

1. principles

- are tuple of length 0, i.e. (), allowed or precluded? Both choices 
make sense. Mathematical logicians tend, or better tended in the past, 
to preclude tuples of length 0. Computational logicians often allow 
them, as e.g. in the programming language ML. Allowing a (single) tuple 
of length 0 make a systematic treatment of tuples easier. Both choises 
are possible but RIF CORE should, I think, be explicit. Otherwise there 
will be different interpretations and inconsistent implementations.

- stating that the empty set as the set of sorts for a variable means 
that this variable 'can be bound to any term' poses, I think, three 
problems. First,  this is inconsistent with the usual assignment of set 
of sorts to variables. Indeed, one expects here the set of all sorts. I 
appreciate that using the empty set might be convenient. But this might 
turn out to be misleading and makes a systematic treatment (e.g. in 
proofs) more difficult. Why not introducing a notation for the set of 
all sorts and use it instead of the empty set? Second, the usage assumed 
is that specifying no (set of) sort(s) for a variable is like specifying 
the empty set. It might be misleading and surely will make the parsing 
more complicated to identify 'nothing' with the empty set. Third, 
according to the semantics introduced in the document, variables are not 
bound to terms (as would be the case with Herbrand structures) but to 
elements of the universe or domain D. The sentence 'variable can be 
bound to term' is incorrect in this context and eould only be correct if 
the samenctics would preclude other structures than Herbrand structures.

- the notion of 'well formed atomic formula' is introduced but that of 
'well formed formula' or 'well formed condition' is missing. The later 
is needed, e.g. for properly conjuncting or disjuncting formulas and for 
existential quantification.

- somewhere it is said that quotes in scalar terms, i.e. constants, are 
escaped using backslash. A more precise specification of the syntax of 
scalar terms is needed, stating e.g. that / cannot be used (except for 
escaping). Furthermore, RIF should not specify yet another such 
spoecification but instead take over that of XML and/or RDF.

- the notion of 'well sorted expression' (with expression meaning here 
term or formula), or however this concept is to be called, should make 
it possible not to attached sort(s) to each occurrence of a constant or 
variable but only to some, in the very same style as type assignementsi 
n ML do not have to be given everywhere. Otherwise, the language might 
be unnecessarily difficult to use.

- the notation proposed for assigning sorts to constants and variables 
dooes not seem to easily extend to assigning several sorts to a constant 
or variable.

- using equality atoms for assigning several sorts to a constant or 
variable seems rather undesirable because it might unnecessarily 
complicate the processing of the language: those equalities serving this 
purpose would have to be recognized in a preprocessing state. Why not 
simply, or more rigourously, have a specific notation for assigning 
several sorts to a constant or a variable. Why not further make it 
possible to specify such an assignement in a foreword to a foormula (r 
rule) very much like in a variable declaration? Why not have a simple 
sort language making it possible to give names to finite sets of sorts?

- the paragraph beginning with "Many primitive sorts in RIF may be based 
..." concludes saying "these sorts will haved the form _uri"..."." This 
means that some sorts have exactly the same syntax as a constant with a 
sort assignement. My guess is this was not meant!

2. style

- the words 'constants', 'names' (like in 'predicate names') and 
'symbols' (like in 'function symbol') are not consistently used. Why not 
to speak only of 'constants' with the three special cases 'term 
constant', 'predicate constant' and 'function constant'. This would be 
consistent and pave the way for dialect à la HiLog where there also are 
'predicate variables'.

- in the definition of a structure, the notation is not fully 
consistent. I_TV denotes the interpretation of formulas, the index TV 
refers to truth value, i.e. the values formulas are assigned. All other 
functions, I_C, I_R, I_F, have index referring to what is given a value. 
  Why not rename I_TV in I_Formula (however this is abbreviated)?

- is it necessary to denote a Boolean signature <s1 x ... x sk> with > 
... >. the < > seem later not to be used.

- well formed function term. Under this name, the document specified 
terms that are 'well sorted'. It would probably be preferable to 
distinguish between terms that are properly constructed, i.e. well 
formed, regardless of sort assignments, and (properly constructed terms) 
with well formed sort assigments.

Received on Wednesday, 7 March 2007 13:43:58 UTC