[Bug 1730] New: [FS] difficult use of "?" in inferences in 8.1 "Judgments for accessing types"

http://www.w3.org/Bugs/Public/show_bug.cgi?id=1730

           Summary: [FS] difficult use of "?" in inferences in 8.1
                    "Judgments for accessing types"
           Product: XPath / XQuery / XSLT
           Version: Last Call drafts
          Platform: PC
        OS/Version: Windows 2000
            Status: NEW
          Severity: major
          Priority: P2
         Component: Formal Semantics
        AssignedTo: simeon@us.ibm.com
        ReportedBy: fred.zemke@oracle.com
         QAContact: public-qt-comments@w3.org


8.1 Judgments for accessing types
Throughout this section there are rules with a question mark following
a syntactic item.  This usage needs to be clarified, since it is
not explained in section 2.1.2 "Notations for judgments" or
section 2.1.3 "Notations for inference rules", and it is not the 
same use of a question mark as in a type such as "xs:integer?".
It appears to be related to the use of a question mark to denote
optional syntax in an EBNF.

The first occurrence is in 8.1.1 "Derives from", the second 
inference under "semantics", where the second hypothesis is

  statEnv.typeDefn(expanded-QName) = 
  define type TypeName restricts BaseTypeName Mixed? { Type? }

In this example there are two of these question marks.  I think 
the intent is that this rule is shorthand for four rules, the 
four being formed from (Mixed present or absent) crossed with
(Type present or absent).

I believe this interpretation works for any inference in which
the question-marked nonterminal only appears once.  The tricky
stuff is when the question-marked nonterminal appears in more
than one premise.  I think the first occurrence of that phenomenon is
in 8.1.9 "Type expansion", last inference under "Semantics".
The complete inference is

statEnv |- TypeName of elem/type expands to expanded-QName  
statEnv.typeDefn(expanded-QName) =
  define type TypeName extends BaseTypeName Mixed? { Type1 }  
statEnv |- Type2 is Type1 extended with union interpretation of 
           TypeName  
statEnv |- Mixed? Type1 adjusts to Type2  

--------------------------------------------------------------------------------
 
statEnv |- of type TypeName expands to Type2  

Note that Mixed? appears in the second and fourth hypothese.
This can't be an occurrence indicator, so I think
it is shorthand for a pair of rules, one with and one without the 
question mark.  The mystery is how to interpret the fact that there
are two "Mixed?" to deal with.  The possibilities are that these
are independent choices (ie, this is shorthand for four inferences,
with the first Mixed present or absent independent of the second
Mixed being present or absent) or they are dependent choices
(ie, two inferences, one with both Mixed present and the other 
with both Mixed absent).  

The inference in 8.1.10 "Union interpretation of derived types"
has this problem big-time, with (n + m) instances of "Mixed?".
Hopefully the interpretation is that in all (n + m) cases, either
Mixed is present in all, or Mixed is absent in all.  Otherwise 
you have a shorthand for 2 ^ (n + m) cases here.

All in all, it would be better to come up with some other symbol 
for these shorthands, instead of overloading the question mark.
In addition, the notation must indicate when choices are 
orthogonal, and when a choice in one premise is intended to be
the same as a choice in another premise.  One way to do this
would be to introduce named variables such as Mixed1, where
Mixed1 is either Mixed or the empty string.  Using such a 
convention, the inference quoted above becomes:

statEnv |- TypeName of elem/type expands to expanded-QName  
statEnv.typeDefn(expanded-QName) =
  define type TypeName extends BaseTypeName Mixed1 { Type1 } 
Mixed1 in { "mixed", ""} 
statEnv |- Type2 is Type1 extended with union interpretation of 
           TypeName  
statEnv |- Mixed1 Type1 adjusts to Type2  

--------------------------------------------------------------------------------
 
statEnv |- of type TypeName expands to Type2  

Note that this notation conveys that that Mixed1 is a single
choice, not two orthogonal choices.

If you adopt such a convention, please be sure to explain it.
I think one of the current weaknesses is to leave a lot of
notational conventions implicit.  (Someone observed to me that
the formal inferences are unintelligible without the 
accompanying English descriptions.  I think he meant that most
people don't know how to read them.  We joked and said they could
just cut out all the inferences and publish it as the Informal
Semantics.  Of course, no formal system can ever be entirely 
self-contained, so we can't expect the formal notations to stand
entirely on their own.  My issue is that the
formal inferences have some implicit assumptions that make them
poorly defined and hard to interpret.  
Also, these implicit assumptions sometimes 
vary with the context, so that a reader's deduction of a 
convention in one context can be incorrect in another.)

Received on Monday, 18 July 2005 21:55:15 UTC