Re: comments on current version BLD document: symbols, datatypes, semantics

> (I am writing this e-mail in the train (the noise cancellation of my
> microphone works surprisingly well :), so I could not have look at the
> latest updates)

Hi Jos,
thanks again for the reviews. Most of the things seem to have been cleared
now, so I'll respond only to the contentious ones.

> >> 2- regarding the structure of this particular section: constants are
> >> introduced in the first paragraph, and (a couple of pages) later
> >> re-defined as pairs of literals and symbol spaces.
> > 
> > Constants are *not* "redefined" anywhere.
> > In the beginning they are just referred to as elements of Const, but there
> > is no redefinition.
> 
> They are not strictly redefined, but the definition is refined later.
> 
> The reader can always skip the section about symbol spaces and constants.

You can put it this way, but we differ in the didactic approach.
I do not think the reader will start skipping text right at the start of a
block of definitions.


> >> 6- section "symbol spaces" second paragraph, first sentence: symbol
> >> spaces are actually not subsets of the constant symbols in RIF.  First
> >> of all, a symbol space is not a set; second, constant symbols are pairs
> >> (literal, symbol space IRI). I would propose to rephrase this sentence
> >> to something like "every constant symbol in the RIF as an associate
> >> symbol space"
> > 
> > They are named subsets. (I added "named" to their abstract definition).
> 
> they are not subsets, because symbol spaces are pairs of lexical spaces
> and identifiers

Symbol spaces are defined as subsets of the set Const of all constants.


> >> 1- section "signatures": there is currently only an informal description
> >> of what partial order between signatures means.  There should be a
> >> formal definition.
> > 
> > A partial order is a partial order. What exactly do you want to define here.
> > There are no missing definitions in that section as far as I can see.
> 
> It was initially not clear what the implication of this partial order
> is.  You give an informal explanation, but no formal definition.
> However, I see now that it follows from the definitions of coherence and
> well formed terms.  So, the text is fine as it is, I think

I inserted a sentence which hopefully will make it read better.


> >> 2- section "signatures and a condition language of RIF^BLD^": the
> >> definition of equality atoms is not entirely clear: the symbol = is not
> >> a constant symbol in RIF, according to the syntax definition in section
> >> "presentation syntax" (it does not have the symbol space).  Furthermore,
> >> as it is correctly mentioned that equality is not a built-in predicates,
> >> I feel there is an impedance mismatch between this predicate symbol and
> >> all other kinds of predicate symbols.  Finally, equality is currently
> >> not mentioned when atomic formulas are initially defined.  Therefore, I
> >> would propose to define equality atoms a=b directly when first defining
> >> atomic formulas.
> > 
> > A good point! You were looking at a version before I moved = further down,
> > but the point about its symbol space is well-taken. It should be either
> > rif:local (my pref) or rif:iri.
> > 
> > I experimented with requiring all symbols to have explicit symbol spaces in
> > the examples, but I think they become unsightly due to that. Perhaps we
> > should not require ^^rif:local explicitly. Then we could write a=b as
> > before.  If people think that we should insist on explicit symbol space
> > names (as it is done now, to make the syntax look more abstract and devoid
> > of syntactic sugar) then I am fine with writing a =^^rif:local b or even
> > equal^^rif:local(a,b).
> 
> This does not yet address my concerns about the impedance mismatch
> between the equality symbol on the one hand, and predicate symbols on
> the other: Predicate symbols are interpreted as sets of tuples, whereas
> equality is interpreted as identity.

Equality is a set of tuples -- it was just defined differently, but
equivalently. I'll change its definition so that it will look like a normal
predicate. But it is a good point. Other than that, would =^^rif:local
satisfy your objection? (I already did it).


> >> 3- section "symbol spaces": why is the lexical space of the symbol space
> >> non-empty?  Why not simply define it as a set?  I think it does not hurt
> >> to allow empty lexical spaces.
> > 
> > A symbol space defines a set of constants. If the lexical space is empty,
> > the set of constants is empty. Does not make sense to contemplate such sets
> > of symbols in the syntax, IMO.
> 
> Well, I can easily think of cases where one would want an empty symbol
> space. I can, for example, easily imagine rule sets which do not use any
> local identifiers, so the lexical space of the rif:local symbol space
> will be empty.
> furthermore, the definitions just become more complicated by requiring
> the sets to be nonempty.

The lexical space of rif:local is never empty. It is defined by RIF in a
concrete way.
Does not matter if a particular rule set or language uses that or not.
There is no side effect.


> >> 4- section "symbol spaces": there should be a restriction on the kinds
> >> of datatypes which may be used.  Namely, the lexical-to-value mapping
> >> and the value space need to be well-defined;
> > 
> > what do you mean by that?
> 
> Say, you are using a datatype with an ill-defined value space, e.g.
> xsd:duration.
> If you have a symbol "xx"^^xsd:duration, the value
> IC("xx"^^xsd:duration) is not well defined, so the interpretation is not
> well defined.

"xx"^^xsd:duration is *not* a constant in rif.
I guess you are talking about "unknown" symbol spaces. In that case tey are
not going to be treated as data types and their value space will not be defined.
It is an omission in the semantics section (now fixed). 

> >> now, the RIF
> >> semantics is not well-defined. The text in the paragraph "symbols with
> >> ill-formed lexical parts" will then need to be updated accordingly.
> >> 5- "symbols with undefined symbol spaces": the description in this
> >> paragraph is incorrect, since, if the symbol space corresponds to a
> >> known datatype, and implementation will interpret the symbol according
> >> to this datatype.  I propose to remove this paragraph.
> > 
> > You were the one who proposed this paragraph in the first place. 
> 
> That was when the datatype support in the RIF was not yet extensible.
> Now it is, so the paragraph is out of date.

I do not understand that. In fact, I now added another paragraph about
unknown spaces in the semantic section.

> > Second, I
> > do not really understand what you are saying.  The paragraph you are
> > referring to talks about "undefined" symbol spaces, while in the above you
> > are talking about the known spaces.
> 
> yes, the terminology is a bit confusing.  RIF "defines" a number of
> symbols spaces, but people can use additional symbol spaces which
> correspond to /known/ datatypes.
> So, we have a number of symbol spaces defined by the RIF; of these
> symbol spaces, those which corresponds to datatypes, correspond to
> /known/ datatypes (by definition). There are a number of other symbol
> spaces which corresponds to datatypes.  Some of these will correspond to
> known datatypes, and some will corresponds to unknown data types.
> I interpreted an "undefined" symbol space as a symbol space which is not
> "defined" by RIF.

This is something I fail to understand. What is a known but unsupported
data type? We list the data types that are known and supported and all the
rest are unknown and unsupported as far as RIF is concerned.

You cannot build an implementation of a logical system based on some
undefined or unknown concepts.


> By the way, it is exactly this confusion which led me to propose to use
> datatype maps.  Interpretations will be defined with respect to a
> datatype maps, which includes all the /known/ datatypes.

Data type maps is one of the most confusing and ill-defined concepts that I
came across.


> >>    a- it is hard to grasp from the definition how a single constant
> >> symbol is interpreted; it is necessary to carefully read and try to
> >> understand all the (too lengthy) text. The definitions can be much
> >> crisper, as I showed in earlier proposals for this definition.
> > 
> > I do not think that the text is either lengthy or that it is not crisp
> > enough.
> > I believe that this is similar to your earlier proposals. If you have a
> > specific text to propose, please do so.
> 
> OK, I will send a proposal in a separate e-mail.

Please take into account the recent updates.

> >>    d- no distinction is being made between the identifier of a symbol
> >> space and the symbol space itself, whereas they are different things
> > 
> > Where did you find that?
> 
> For example, you talk about things like "the symbol space rif:text".
> However, rif:text is the identifier of the symbol space, and not the
> symbol space itself.

Well, this is quite acceptable. People do this all the time when confusion
does not arise. I was asking about the places where the use of "the symbol
space rif:text" as opposed to "the symbol space *named* rif:text" causes
confusion.


> >>    e- according to the second bullet in "the effect of the symbol
> >> spaces", the mapping IC(lit^^symsp) should be defined for every constant
> >> symbol of the form lit^^symsp with lit in the lexical space of the
> >> symbol space identified by symsp.  This would mean that every such
> >> symbol is in the vocabulary of every RIF language. I think this is
> >> highly undesirable (and should have been mentioned in the syntax
> >> section). The mapping should only be defined for symbols in the vocabulary.
> > 
> > We are defining a logic, including some specific sets of symbols that
> > belong to the language of that logic.
> 
> Yes, but it is not necessary.  Why not let the user decide exactly which
> of the symbols to use?

The user can use or not use whatever symbols they want. This has absolutely
no effect on the user! When you define a language of a logic, you are
defining a language for that logic, not for a particular set of formulas in
that logic. This is a standard textbook way of doing things.


> > Your claim that this is "highly undesirable" requires at least some explanation.
> 
> OK, because it is syntax my claim is probably a bit too strong.  The
> thing is that it is simply unnecessary to include all these constants in
> the vocabulary of every language, so why would we do it?

See above.


> An additional drawback is that if we were to consider a dialect which
> has a semantics based on Herbrand universes, all these symbols are
> included in the universe. This would have certain undesirable
> implications, e.g. ( considering a dialect with negation):

You are completely wrong. Herbrand universes are defined with respect to
the symbols mention of the rule set, not with respect to the symbols in the
entire logic language.

> 
> q(a)
> 
> s(x) :- naf q(x)
> 
> entails
> 
> s("1"^^xsd:integer)
> s("1"^^xsd:string)
> s("2"^^xsd:integer)
> s("2"^^xsd:string)
> s("3"^^xsd:integer)
> s("3"^^xsd:string)
> .....

As I said above, this is a non-example.


> > I fail to see what exactly is missing in the definition of the syntax.
> 
> from the definition of the syntax it is not clear that the vocabulary
> includes all these symbols. I think that if this is the case, and the
> reader should be notified in the syntax section.

See above.

> >>    g- the value space is required to be a subset of the domain.  This
> >> means that every interpretation includes all value spaces of all data
> >> types.  This is unnecessary.
> > 
> > So what? It makes the definition simple and uniform.
> 
> It makes every domain infinite. For most kinds of rules (especially
> those without equality in the head) this is not really a problem.
> However, as soon as we have full use of equality, or deal with
> extensions in the direction of FOL, then one often wants to talk about
> finite models.

You can still talk about finite models.  If you are not going to use
infinite relations then you are fine. If you are going to use infinite
relations then you do not have finite models anyway. Equality is
never a problem in this setting, because it is interpreted as identity.

> It also makes rule sets which only contain rules such as Forall ?x,?y
> (?x=?y)  inconsistent. I claim that this is undesirable.

I claim that this is YGWYD (you get what you deserve). Such a statement
should be treated as inconsistent if you are using data types.

Although I do not agree with any of your arguments about undesirability, I
am ok with changing things so that value spaces will not be required to be
a subset. To this end, I added a note in the appropriate place stating that
you are proposing a certain change. Let the people decide!


> On a side note, some extensions (and possibly a combination with OWL DL)
> will want to separate the (concrete) interpretation domain for datatypes
> from the individual (abstract) interpretation domain in order to be able
> to do effective reasoning.
> I believe we currently do not have such a mechanism (to separate the
> two), do we?

I am not sure what you mean. If you are not using data types then you can
map the thing into a theory where data types are not used.


	--michael  


> Best, Jos

Received on Wednesday, 10 October 2007 20:28:28 UTC