Re: Some notes on FLD

Thomas Krekeler wrote:

 > Hello,
 > I'm working on a RIF XML parser/serializer for OntoBroker.
 > Below are some questions/notes I have, intended to be a feedback for your
 > working group in the hope that they are useful.
 > If not stated else, the comments are related to the July 30th 2008 version
 > of the FLD document on your wiki site,

Thank you for all your comments, and apologies for the time it took to respond. 
We have made appropriate changes where applicable. Please see below.

 > - 2.8 Definition (Well-formed formula)
 >  o Items 1., 4.-7.: The resulting formulas are non-aggregate formulas.
 >           This is already stated in the introduction, but maybe one could
 >    repeat it explicitly (which already holds for 2. and 3.).


 > - 2.8.9 What is the benefit of making the dialect directive for a document
 >    formula optional?
 >    Even if for a BLD document it might not matter to choose all
 >    models as intended semantic structures or just the unique minimal
 >    model, one can define other dialects, for which the semantics
 >    differ for the document.
 >    How should the system know which dialect to choose if it supports
 >    several of them?
 >    Will the user have to take this job? Some of them might hardly
 >    know what a rule language is at all.
 >    Would you like to put the information into the file extension?
 >    Since all dialects share the same xml format, I would prefer to
 >    have only one extension, say "rif", and the information about the
 >    dialect should be included within the file itself.

The problem with dialect indicators is this: imagine two systems, where one only 
knows dialect D1 and the other only knows dialect D2. If the D1 system produces 
a document which happens to fall into the intersection of D1 and D2, it would be 
nice to have the D2 system be able to use it. But if it uses a dialect indicator 
to recognize what it can process, it can't do that without extra information 
about D1, which it may not have.

The idea here is that syntactic features can, in many cases, determine the 
semantics and thus a suitable dialect. So by syntactic analysis (essentially 
just collecting the XML tags), one might be able to figure out which language 
features are used by a document. If those are the features you implement and the 
semantics is unambiguous, you can process the document (correctly), without 
needing to know which dialect the author was using to do the authoring.

The optional dialect directive was primarily provided to address the scenarios 
when the above does not work, i.e., when syntactically identical (or largely 
identical) dialects differ only in their semantics. For instance, one logic 
programming dialect might use the Well-founded semantics for negation and 
another the Stable-model semantics. Their syntaxes are going to be the same or 
largely the same. In that case, it would be impossible to determine just from 
the syntax which dialect is meant.

Other possible uses of the dialect directive might be debugging and error messages.

 > - 2.9 Annotations in the Presentation Syntax... "A convention is used to..."
 >  o How would I annotate t in t[w->v] and not the whole frame term?

This has now been explained.

 > - 3.4.4 "This can be understood as treating a as a set-valued argument."
 >  o Since the interpretations for p(a->b) and p(a->b a->b) may
 >    differ, it should be "... treating a as a bag-valued argument.", I
 >    think.


 > - 3.4.5
 >  o One question I asked myself while reading this was, if
 >    I_NF(o[a->b]) may differ from I_NF(o[a->b a->b]) (see 3.4.4).
 >           The answer "no" is given in 3.6.8, maybe one could clarify this
 >    already in 3.4.5.


 >  o How do I unify o[a->b a->c] and o[a->?X a->?Y]?
 >           I see [?X/b, ?Y/c] and [?X/c, ?Y/b] as possible unifications.
 >           None of both is more general then the other, so, is there no MGU,
 >    or would an appropriate definition for an MGU state that "the
 >    ordering does not matter"?

There can be several MGUs, but this topic is outside the scope of this document. 
MGUs belong to the proof theory and run-time execution, which this document does 
not cover (and there are no plans to cover this).

 > - 3.4 "The effect of signatures"
 >  o I think the required conditions can be always trivially be made
 >    true by choosing D_sg := D, maybe one should state here, that the
 >    dialect chooses the D_sg's and not, that "..., there is a subset
 >    D_sg..." (which is too general in my opinion).

D_sg is one possibility. But other semantic structures may have D_sg as a strict 
subset. The definition is thus allowing more possibilities.

 > - 3.4 "The effect of datatypes"
 >  o Quotation marks are missing: It is "For each constant lit^^dt
 >    such that lit \in LS_dt, I_C(lit^^dt) = L_dt(lit).", but it should
 >    be "For each constant "lit"^^dt such that lit \in LS_dt,
 >    I_C("lit"^^dt) = L_dt(lit)." as in the BLD document.


 > - 3.5 "Annotations and the Formal Semantics" [second paragraph]
 >  o "Since annotations are represented by frame terms,...". Seems
 >    that I have read over this, where is a note made about this?
 >  o "...they can be reasoned with by the rules." For me the BLD
 >    version (in 3.3) of the sentence is much more understandable,
 >    although I'm not a native speaker and that might be the reason.


 > - 3.9 "Note that one consequence of the multi-document semantics is..."
 >  o It sounds a bit like rif:local constants MUST be different, but
 >    they only MAY be different.
 >  o \Delta |= ""^^rif:iri("abc"^^rif:local) MAY
 >    actually hold, but not necessarily.
 >   + In particular the following always holds if \Delta is a
 >     model: \Delta |= Exists ?X
 >     (""^^rif:iri(?X))

What does "MAY hold" mean? In some particular models certain things may hold, 
but they might not hold in other models. This is a standard property of most 
model-theoretic semantics. It is not clear what you are actually trying to say 
in the above paragraph.

 > - 4.2.1 "Mapping of the Non-annotated RIF-FLD Language"
 >  o I'm missing a version info.

(but not in FLD) we suggest the use of owl:versionInfo metadata for this. A 
similar paragraph has now been added to FLD - see

 >  o In addition, I'm missing a naming concept for a document, i.e. a
 >    document has no identifier like an OWL ontology which always has an
 >    ontology URI.

This is already covered by Document ::= IRIMETA? 'Document' '(' ... ')', where 
the annotation IRIMETA is (* id φ *) with identifier id.

 >  o Atom/Expr: One needs a look-a-head greater than one to detect if
 >    the term has named arguments or unnamed arguments.
 >    An XML attribute, like <Expr namedArguments="yes">, would
 >    simplify the parsing process.
 >    Of course this would make manually editing of RIF XML documents
 >    less comfortable, however.

If Atom/Expr contains a slot child, it has named arguments; if it contains an 
args child, it has unnamed arguments. (See Examples 6 and 5 in BLD, respectively.)

 >  o Atom/Expr with unnamed arguments: What is the "args" tag good for?
 >    For the named version there is no such tag, actually, there is no
 >    other tag encapsulating the items of a list somewhere else.

The "args" is a 'role tag' leading to positional arguments (a sequence of 
arguments, which corresponds to a 'non-parenthesized' list). Each "slot" is a 
'role tag' leading to a name-argument pair.

 >    I guess it is used for the "ordered" attribute?
 >    For me this attribute seems to be unnecessary since ordering is
 >    always required... or are you planning a positional term with
 >    unordered arguments?

The "ordered" attribute is indeed fixed in the XSDs of the element "args" (see, 
e.g.,, hence can 
be omitted in XML instances.

 >  o In general I would prefer to handle lists in the following way:
 >    <parent>
 >       <propertyName>
 >          <list>
 >             X_fld(item1)
 >             ...
 >             X_fld(itemN)
 >          </list>
 >       </propertyName>
 >    </parent>
 >    for example
 >    <Exists>
 >       <boundVariables>
 >          <list>
 >             X_fld(variable1)
 >             ...
 >             X_fld(variableN)
 >          </list>
 >       </boundVariables>
 >    <Exists>
 >    i.e., the bound variables of an exists formula are one property
 >    which has type list of variables.
 >    Of course this is a matter of taste and pretty much a personal
 >     comment.

We had a proposal for lists which, however, didn't make it into the Last Call. 
We consider to reuse OWL 2 lists, where really needed.

 >  o "Since the presentation syntax of RIF-FLD is context sensitive,
 >    the mapping must differentiate between the terms that occur in the
 >    position of the individuals and the terms that occur as atomic
 >    formulas."
 >    Hm, actually I don't understand that.
 >    And I have the feeling, that this is very BLD related.
 >    A term is always allowed to occur in a term context --- or in BLD
 >    terminology: in the context of an individual ---, except the
 >    signature is forbidding it.
 >    And a term is allowed to occur in a formula context, if and only
 >    if it has signature "atomic".
 >    Given a well formed FLD formula, it is always clear if a term
 >    occurs in the context of a term or a formula, since there is no
 >    construct which allows taking a non-atomic term or a formula for
 >    one of its properties.

The mapping is not supposed to use signature information.

 >    Anyway, if you would like to explicitly state that a term occurs
 >    in a term or a formula context or not, why are positional terms
 >    handled different from all other terms?  Only for positional
 >    terms it is made explicit by using Expr or Atom, but not for any
 >    other term type... wondering about that.

Expr/Atom can be positional or have named arguments (see above discussion).

 > One point I see on the conceptional site is the interpretation of terms
 > with respect to their signatures.
 > Let me make an example:
 > Take BLD as a template.
 > For each symbol space identifier "symbolSpaceID" let
 > "symbolSpaceIDSigature" be a sub signature of "individual".
 > A constant has signature "symbolSpaceIDSigature", if and only if it is in
 > the symbol space identified by symbolSpaceID.
 > Now, I would like to have a functional built-in called "foo".
 > I define, that "foo" has the signatures (xsd:integer xsd:integer) =>
 > xsd:integer and (xsd:double xsd:double) => xsd:double.

You seem to confuse two things here. xsd:integer is a symbol space, not a 
signature name. You can associate a particular signature with such constants, 
but once you do this carefully you will understand that your arguments break 
down. Right now, what you are saying is not even well-formed from the point of 
view of the definitions.

 > Sadly the interpretation function I_F for positional terms is independent
 > of the signature, i.e. "foo" is mapped to one and the same function,
 > regardless which of its signatures is used in a concrete term like
 > foo("1"^^xsd:double, "2"^^xsd:double), so, I cannot make "foo" behave
 > different for doubles which are also integers and the equivalent integers.

This is not true Note that "1"^^xsd:integer = "1"^^xsd:double is FALSE. So 
foo("1"^^xsd:double, "2"^^xsd:double) can have one value, but 
foo("1"^^xsd:integer, "2"^^xsd:integer) another. Perhaps you wanted to use 
xsd:decimal instead of xsd:double? In that case - yes: foo("1"^^xsd:integer, 
"2"^^xsd:integer) = foo("1"^^xsd:decimal, "2"^^xsd:decimal) because "1"^^integer 
= "1"^^decimal, etc. But this is the CORRECT behavior. Otherwise the law of 
substitution of equals by equals won't hold, and you don't get a logic with 

 > Together with paragraph "The effect of signatures." of 3.4, I get into more
 > trouble:
 > The result of "foo" must be in the intersection of the domain D_xsd:integer
 > of the signature xsd:integer and the domain D_xsd:double!
 > So, D_xsd:integer cannot be the value space of xsd:integer --- as I would
 > like to define it ---, but it must include the value space of xsd:double as
 > well.

As mentioned above, you are confusing signatures with symbol spaces.

 > In programming languages, these kinds of problems are solved by using
 > different implementations for overloading a function name with different
 > signatures.  Maybe one could do it in the same way for the interpretation
 > of terms, i.e. make the interpretation dependent on the used signatures?
 > As a consequence, one would need to make the used signatures of terms
 > explicit, at least, if it cannot be non-ambiguously resolved from the
 > context.
 > I don't know if one will get problems in other places with this approach,
 > but at least it is widely used and well understood.

First, as mentioned above, it is not clear that there is a problem, since you 
have confused different notions. Second, there are "programming languages" and 
there are "logics". In many cases one can do similar things in both, and in many 
cases things are different.

Finally, remember that the purpose of signatures is to enable concise ways for 
specifying logic dialects, i.e., dialects that have model-theoretic semantics. 
You seem to be talking about something else here, unrelated to formal 
logic-based languages.

 > Thomas Krekeler
 > Research & Development
 > ontoprise GmbH

Thank you again for your comments.


Dr. Christopher A. Welty                    IBM Watson Research Center
+1.914.784.7055                             19 Skyline Dr.                           Hawthorne, NY 10532

Received on Sunday, 5 October 2008 23:23:32 UTC