comments on BLD draft part II

My final batch of comments:


18 - section 2.1.4, truth valuation for formulas: the notion of a
"well-formed formula" is not defined for the presentation syntax
19 - section 2.1.4, interpretation of data types: the interpretation of
symbols with datatypes is not included in the definition of an
interpretation (see also [1]).
For example:
Given a set of supported datatypes DT, IC is a mapping from Const to
elements of D, such that for every (literal, label) in Const it holds
that whenever label is an identifier of a datatype d in DT, IC((literal,
label))=L2V^d^(literal), where L2V^d^ is the literal-to-value mapping of d.

Furthermore, the discussion about value spaces should be moved to where
data types are introduced, since value spaces are part of a datatype.

20 - section 2.2.1:
  a- it seems unnecessary to introduce the formula "true"
  b- the syntax of the return value of Unnest is unclear.  I would
propose to use the presentation syntax instead.  In this way, it is easy
to avoid using the formula "true":
If f is a term, then Unnest(f)=""
Otherwise, if f is a frame of the form o[a->v] then
Unnest(f) = And(Unnest(o) Obj(o)[a->Obj(v)] Unnest(v))

21 - section 3.1.1.2: the notion of a "well-formed condition formulas"
is used here, but was never defined.

22 - There is no way to identify rules in the current syntax; this is
probably related to the metadata discussion (which has a low priority on
the face-to-face, unfortunately).

23 - Section 3.1.2.1, last paragraph: it is not clear what is meant with
extensions being required to be "compatible" with a given definition.
It seems that in many cases these is not possible, especially if the
semantics does not have a model theory. Perhaps compatibility should be
defined with respect to entailment?

24 - section 2.1.1: The notions of free variable occurrences and closed
formulas need to be defined here. A statement "We adopt the usual
scoping rules for quantifiers from first-order logic." is not sufficient
for a language specification.


best, Jos

-- 
Jos de Bruijn            debruijn@inf.unibz.it
+390471016224         http://www.debruijn.net/
----------------------------------------------
The third-rate mind is only happy when it is
thinking with the majority. The second-rate
mind is only happy when it is thinking with
the minority. The first-rate mind is only
happy when it is thinking.
  - AA Milne