Re: Notes on 7/20 BLD draft

> Michael,
> 
> Here are some notes I took while reading the latest BLD draft.  Most 
> of this is minor editing, which I am happy to do myself, let me know.
> 
> There are a couple of comments prefixed by "*" below that may need 
> discussion.
> 
> Let me know if you would like me to go ahead and make the non-*'d changes.

Thanks Chris,
I took care of mos of these. Please find my responses in-line.


	--michael  


> 2.1.1.1
> 
> Is a boolean signature an arrow signature?  Text implies it is

Yes. I now clarified it. In an earlier draft (in WD1) they were not, but it
is more elegant to treat them as just a special case.

> In "Well-formed terms and formulas" you switch to using "s" to 
> represent symbols, where in the previous section it is signature 
> names.  A bit confusing.

ok, changed.

> "Each ti is a well-formed term with signature σj, j = 1,...,n; and" 
> seems to imply that every ti need a different signature - which is not 
> the case (indeed, the basic case is that they are all individuals). 
> Clarify that the oj's are not distinct? - this is clear I suppose in 
> the next line.

done.

> "If φ is an atomic formula than it is also a general well-formed 
> formula." I think "atomic formula" needs to be replaced by "well 
> formed atomic formula" and "than" => "then"

done

> "φ ∧ ψ is a general well-formed formula, if so are φ and ψ" => "if φ 
> and ψ are general wff, then so is φ ∧ ψ".  Same change for disjunction.
> 
> "∃ V1 ... Vn φ is a general well-formed formula, if so is φ and V1, 
> ..., Vn are variables" => "if φ is well formed and V1, ..., Vn are 
> variables, then ∃ V1 ... Vn φ is well formed."

done

> "The basic RIF condition language presents a much simpler picture to 
> the user by restricting the set of well-formed terms with a very 
> constraint coherent set of signatures" => "The basic RIF condition 
> language presents a much simpler picture to the user by restricting 
> the set of well-formed terms to a coherent set of signatures."
> 
> "The symbols f,,n,, and p`n are reserved signature names in the basic 
> RIF logic dialect." => Subscript the n for f and add "for all n".
> 
> "basic RIF logic dialect" => "RIF basic logic dialect".  Maybe add "in 
> addition to bool and i"

all these have been fixed now

> "The equality symbol, =" subscript on p doesn't look right.

This was probably fixed earlier. Can find that one.

> 2.1.1.3
> 
> It would be best if the correspondence between the ASN and the ebnf 
> were more obvious.  Perhaps this will be generated automatically at 
> some point, but for now the productions (nonterminals) should have the 
> same names as the classes in the ASN.  I'm happy changing the names of 
> the ASN classes to CONJUNCTION, etc.

Harold responded to that.

> "firts-order logic" => "first-order logic"

done.

> * It seems to me a cleaner syntax is to remove existentials from 
> conditions and unify all quantifiers outside the rule (as with 
> universal now), and add a restriction in horn that existentially 
> quantified vars cannot appear in the conclusion.

We discussed this in a separate thread.

> * In the "XML serialization" section the language needs to be changed 
> to indicated that the xml serialization is a serialization of the ASN 
> and NOT of the eBNF.  The eBNF is a serialization of the ASN.   Thus 
> the rules for serializing the ebnf should be removed.

Harold will do something about it.

> * In 'Syntax for Primitive Types" I don't like the quotes around all 
> values - are they needed?

They are needed if you want them to be parsable by a machine instead of a
clone of yours :-) RDF also has these quotes for the same reason.


> "a priori" is generally italicized.

ok

> 2.1.2
> 
> * Signature names for dialects should be URIs

If fixed that, if I understood you correctly.

> 2.1.3
> 
> * Truth valuation for quantification is pretty vague.  I think we all 
> know what it is supposed to mean, but the paragraph is pretty vague: 
> "except possibly on the variables..."????  I can't figure out what you 
> are trying to say.

Fixed.

> "We assume that Dtype ⊆ D for each XML data type and that Dt is 
> disjoint from Ds for different XML primitive types s and t. " => add: 
> except where there is a subtype

This was pretty much garbled in the draft. I rewrote the whole thing.


> 2.2.1.1
> 
> * Why is there a special syntax for type & subclass?  These should 
> just be syntactic sugar even if they are there.

I am not sure what you mean. Subclass is a fundamental relationship in oo
and frame languages. Everything is a syntactic sugar at some level,
including frames, so I do not know what you mean here.

> 2.2.1.2
> 
> * I don't understand the subproperties for the frames and uniterms in 
> the ASN.  Subproperty of what?  What is this supposed to convey?

Me neither. I am more comfortable with BNF.

> 2.2.2
> 
> * what would a##b[s->v] mean?

This is explained in the part that explains flattening.
It means a is a subclass of b and it has an attribute s whose value is v.
That is, a##b /\ a[s->v].

> "Islot is a function form the domain" => "Islot is a function from the 
> domain"

ok

> slot terms cannot themselves be slotted - The definition of Islot 
> should clarify this (currently says "where T, sloti, and Vi are terms.").

They can (for uniformity; we can restrict that, but I see no reason
why). The definition was missing a piece, which has now been added.

> The subscripts are not necessary in the second bullet, and in fact is 
> missing from V.
> 
> 
> Note:
> Relations:  ITruth(r(t1 ... tn)) = IR(r)(I(t1),...,I(tn))
> Slots: ITruth(T[sloti->Vi]) = Islot(I(sloti))(I(T),I(V))

ok

> * Why isn't ITruth(T[slot->V]) = IR(slot)(I(T),I(v)), in other words, 
> why aren't slots just syntactic sugar for binary relations?

First, a slot should be different from a binary relation that has the same name.
Second, we allow variables over slots.

> Isub and Iisa are improperly nested.

Thanks. fixed

> * Why isn't ITruth(o#cl) = IR(cl)(I(o)), in other words, why isn't 
> type just syntactic sugar for unary predicates?

Again, we allow predicates and classes. A class is not the same as a unary
predicate with the same name. They should be kept separate for many
practical reasons. Second, we allow variables over classes.

> * I do not at all understand the need for the subclass operator.

Are you saying that subclasses are not needed? I do not understand?

> "2.3.0.1. Abstract Syntax" should be "2.3.1" I think.
> 
> 
> Section 3
> 
> * Let's move extended XML syntax examples to an appendix.

There is only one small example, and I think it is helpful to have it in-line.
Not clear what can be gained by moving it, but I can see that a reference
to the appendix for such a small thing can be annoying.

Received on Tuesday, 24 July 2007 11:58:11 UTC