From: Michael Kifer <kifer@cs.sunysb.edu>

Date: Mon, 18 May 2009 20:48:05 -0400

To: Chris Welty <cawelty@gmail.com>

Cc: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

Message-ID: <20090518204805.139fb5f9@kiferserv>

Date: Mon, 18 May 2009 20:48:05 -0400

To: Chris Welty <cawelty@gmail.com>

Cc: "Public-Rif-Wg (E-mail)" <public-rif-wg@w3.org>

Message-ID: <20090518204805.139fb5f9@kiferserv>

Thanks, Chris, Here are my responses to your comments. On Mon, 18 May 2009 15:55:06 -0400 Chris Welty <cawelty@gmail.com> wrote: > Abstract: > > In the abstract and overview, I think the standard-speak used is too > constraining regarding the requirement of future dialects to implement FLD: I already responded to that one in a previous email. http://lists.w3.org/Archives/Public/public-rif-wg/2009May/0136.html > 2.2 Alphabet > > "Definition (Alphabet). The alphabet of the presentation language of RIF-FLD > consists of the following disjoint subsets of symbols: " > > Common Logic allows variable symbols and constant symbols to overlap. Do the > subsets need to be disjoint? All these types of things can be distinguished > by their syntactic context. This is just an unnecessary complication, which buys you nothing. In many respects, RIF is more general than Common Logic, and forcing one to decide what is a variable and what isn't by the context is a huge nuisance. In fact, you CANNOT determine what is a variable by the context alone. Many rule languages omit quantifiers. How do you distinguish then? Besides, we have already agreed early on that variables are prefixed with a ?, and this is how one identifies them. > "A countably infinite set of quantifiers...where n ≥ 1" > > It seems strange to include the variables as part of the set of quantifiers. > WHy aren't the quantifiers just Exists, Forall, ... Not strange at all. Are you proposing to define a special language for defining quantifiers? Quantifiers can be very general with all kinds of variables in various places. For instance, how would you define bounded quantifiers? You would need to invent a separate sublanguage, but this sublanguage might turn out to be too restrictive. What do you do then? Reconvene the WG to extend FLD? Sounds like a huge complication with no visible benefits. Remember that the presentation syntax allows one to "unpack" the variables from the syntax, so the definition is just a general formal device. > 2.4 Terms > > "Positional terms in RIF-FLD generalize the regular notion of a term used in > first-order logic. For instance, the above definition allows variables > everywhere, as in ?X(?Y ?Z(?V "12"^^xs:integer)), where ?X, ?Y, ?Z, and ?V > are > variables. Even ?X("abc"^^xs:string ?W)(?Y ?Z(?V "33"^^xs:integer)) is > a positional term (as in HiLog [CKW93]). " > > This idea goes back at least as far as Enderton, 1972, and has been used in > implemented systems such as SNePS and Conceptual Graphs in the 80s. Since > Enderton published in '72 what was already a "well known encoding" of > predicate variables in FOL, I don't think it's accurate to say this > "generalizes...FOL". > The fact is that this IS perfectly first-order. The idea goes back to Henkin. However, take another look at these terms and you will see that some are not expressible in Henkin's syntax or in Common Logic. It is in this context that HiLog is referred to. Second-order variables by themselves are not worth bothering to reference, as this is common knowledge. You might be confusing first-order logic with first-order logic syntax. The above paragraph says that these terms extend the terms used in first-order logic. Nowhere it says that this extends first-order logic in general (because this is a semantic, not syntactic matter). But FLD does, indeed, extend first-order logic semantics, since it allows dialects to define inference using intended models rather than all models. > Thus it seems reasonable to just say something like: "Positional terms in > RIF-FLD are quite general, and allow variables everywhere, as in ?X(?Y ?Z(?V > "12"^^xs:integer)), where ?X, ?Y, ?Z, and ?V are variables. Even > ?X("abc"^^xs:string ?W)(?Y ?Z(?V "33"^^xs:integer)) is a positional term (as > in HiLog [CKW93], SNePS [SR87], and Common Logic [CL07]). " See above. Also, SNePS has little to do with HiLog. > 3.2 Truth Values > "RIF dialects can have additional truth values. For instance, the semantics > of some versions of NAF, such as well-founded negation, requires three truth > values: t, f, and u (undefined), where f <t u <t t. Handling of > contradictions and uncertainty usually requires at least four truth values: > t, u, f, and i (inconsistent). In this case, the truth order is partial: f <t > u <t t and f <t i <t t. " > Since the document says the inverse operator needs to be defined, I suggest > you define it here for these two examples. done > 3.6 Interpretation of Non-document Formulas > > In a <t,u,f> valued dialect, I'm unsure what happens in this case: > > Exists(?x) P(?x) > Exists(?x) P(a) :- P(?x) > > If this entails anything other than P(a), then we would have a hidden > extension. Did you mean this? (*) P(a) :- Exists(?x) P(?x) First, let me say that FLD does not define entailment --- dialects do. This is a MAJOR point. Second, if you indeed meant Exists(?x) P(a) :- P(?x) then the above does not entail anything useful (not even P(a)) in any reasonably defined dialect. If you meant (*), then P(a) is entailed. Third, what did you mean by "anything other than P(a)"? Of course, if it entails P(a) then it entails P(a) /\ P(a), P(a) \/ Exists(?x) p(?x), etc. I fail to see your point here. > In general as reading I tried to think of myself using FLD to define a full > first order (+ datatypes) dialect, but I was not able to get a clear idea of > it, so I'm left unsure whether it would work. I am completely surprised. Which particular feature of FOL you had difficulty with? This should be absolutely trivial. Just use signatures to restrict the syntax (like we did in BLD) and then define entailment so that all semantic structures would be considered intended. > I note that, like BLD, FLD avoids any notion of error. I understand why we > did that for BLD, but wonder if more expressive and complicated dialects will > want it, and whether FLD should support it. Do you have a proposal for how to do that specifically? Of course one can think of many ways, but it is not particularly clear which is the "right" one. Given that our builtins do not support this notion, it is not even clear what the utility of this thing would be. Furthermore, FLD is general enough to allow dialects to support certain types of errors. For instance, they can introduce a new truth value (and a new constant for functions that return errors). However, the wisdom of imposing this through FLD is unclear to me. -- -- michaelReceived on Tuesday, 19 May 2009 00:48:50 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Tuesday, 2 June 2009 18:34:08 GMT
*