- From: Francois Bry <bry@lmu.de>
- Date: Wed, 07 Mar 2007 14:43:54 +0100
- To: Michael Kifer <kifer@cs.sunysb.edu>, "Boley, Harold" <Harold.Boley@nrc-cnrc.gc.ca>
- Cc: public-rif-wg@w3.org
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