Some notes on FLD


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,

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

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

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

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

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

- 4.2.1 "Mapping of the Non-annotated RIF-FLD Language"
 o I'm missing a version info.
 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.
 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.
 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.
   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?
 o In general I would prefer to handle lists in the following way:
   for example
   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.
 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.

   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.

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.

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.

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.

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.

With best Regards,

Thomas Krekeler
Research & Development
ontoprise GmbH - know how to use Know-how
Ontoprise offers services for companies around Semantic MediaWiki:
An der RaumFabrik 29; 76227 Karlsruhe
Tel.: +49 (0) 721 509 809 64; Fax: +49 (0) 721 509 809 11
Sitz der Gesellschaft (registered office): Karlsruhe, Germany, Amtsgericht Mannheim, HRB 109540 Geschäftsführer (managing directors): Prof. Dr. Juergen Angele, Dipl.Wi.-Ing. Hans-Peter Schnurr 

Received on Wednesday, 3 September 2008 07:22:01 UTC