Re: Review of FLD

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.


-- 
    -- michael

Received on Tuesday, 19 May 2009 00:48:50 UTC