Re: Review of FLD

Michael Kifer wrote:
> 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?

As you point out below, the choice should be up to a dialect.  Allowing variable 
and constant symbols to overlap in FLD simply means that a dialect can make that 
choice, not that every dialect must support it.  As it is, Common Logic cannot 
be expressed as an FLD dialect, and thus it is not more general.

> Besides, we have already agreed early on that variables are prefixed with a ?,
> and this is how one identifies them.

We agreed on that for our existing dialects.  I never agreed to that for all 
logic languages.  I personally don't see why it is needed, unless you allow no 
quantifiers, in which case you do.  Again, seems like its a choice in language 
design, not something to require of all.

>> "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?

No, but the "set of quantifiers" including distinguishing Forall x,y from Forall 
y,z and calling them different elements of the "set of quantifiers" just seems 
strange.  I'm not calling it wrong, just strange.  Forall and Exists seem like 
different elements of the set.

This isn't a problem, I just found it odd.

> 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.

I don't get your point, how does adding the variables to the elements of the set 
of quantifiers help you with bounded quantifiers?  Bounded quantifiers need 
another argument with each variable.  I guess I don't see how this helps you 
differentiate between different languages with different forms of quantification.

> 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.

Yes of course, but this example is of positional terms and is completely first 
order.  What about it do you consider non-Henkin (other than the datatypes), or 
non-CL?  Again, I'm just talking about the positional terms item, not FLD terms 
in general.

>> 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.

I never said it did, just that this kind of syntactic freedom (to use variables 
in pretty much any position) was implemented in SNePS by 1985 at the latest, and 
probably earlier.

>> 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)

No, I meant the example I gave, though (*) is equivalent in a first-order system 
to my second sentence, and the entailment of the two sentences would of course 
be P(a).  I'd be happy with that rewrite, but now I don't know why the rewrite 
would make a difference.

> First, let me say that FLD does not define entailment --- dialects do.
> This is a MAJOR point.

I'm just wondering what the sensible entailment in a well-founded semantics 
would be for that, and if it is the same as in a first order system.  It seemed 
to me that you have a problem with a closed/open world and the entailments might 
be different.

> 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.

For certain what I wrote entails P(a) in FOL, which is a pretty reasonably 
defined dialect.

> 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.

I was wondering if it creates an "invisible extension" where e.g. the same rule 
means different things in different dialects.

>> 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.

My point was not that I had trouble, my point was that I didn't actually do it. 
  I feel like I would have had a more fundamental understanding of FLD if I had 
done that, but I didn't have time.  I guess in some sense I feel like few if any 
will really understand FLD until they try to use it for something.

>> 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.

Well, sometimes you seem to miss the point of FLD (;-) - it shouldn't impose 
anything but rather provide a range of options to logic dialect designers.

Anyway, I have no proposal for errors, just pointing out that some dialect 
designers might wish for it.  I seem to recall the (lack of a) notion of error 
we are using in BLD was my proposal anyway, so I should be happy with it...

-Chris

-- 
Dr. Christopher A. Welty                    IBM Watson Research Center
+1.914.784.7055                             19 Skyline Dr.
cawelty@gmail.com                           Hawthorne, NY 10532
http://www.research.ibm.com/people/w/welty

Received on Tuesday, 19 May 2009 03:02:22 UTC