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.

-Chris


--------------


2.1.1.1

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

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.

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

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

"φ ∧ ψ 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."

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

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

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.

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

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

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

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

"a priori" is generally italicized.

2.1.2

* Signature names for dialects should be URIs

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.

"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

2.2.1.1

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

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?


2.2.2

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


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

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

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


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


Isub and Iisa are improperly nested.

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

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

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



-- 
Dr. Christopher A. Welty                    IBM Watson Research Center
+1.914.784.7055                             19 Skyline Dr.
cawelty@gmail.com                           Hawthorne, NY 10532
http://www.research.ibm.com/people/w/welty

Received on Monday, 23 July 2007 16:15:56 UTC