match expression's operational semantics

Dear Stephan,

This is a response to the following message, which you posted to the
XML Query Working Group's comments list:

http://lists.w3.org/Archives/Public/www-xml-query-comments/2001Jun/0005.html

The confusion comes from the fact that in Section 5.7 [Match
expressions] of the Query Algebra Working Draft explaining the dynamic
semantics of the match expression, v is not a variable but the *value*
of the input expression of the match.

In your example:

 the variable 'books' is the input of the match expression, and value
 of that variable 'books' is:

    book [ "XML Query" ], 
    book [ "Data on the Web" ] 

 the actualy run-time type (see Section 4.1 Relating data to types) of
 the variable 'books' is:

    book [ String ],
    book [ String ]

 and not

    Book{2,*}

Indeed, (book[String],book[String]) has an empty intersection with
Book{3,*}. Therefore the else first case clause is not evaluated and
the else clause is evaluated, yielding an error in your example.

More intuitively, the semantics of the match expression is such that
it evaluates the first case branch for which the input value is in the
domain of the given case type. Note that the new version of the
dynamic semantics in the latest published version of the XQuery 1.0
Formal Semantics:

http://www.w3.org/TR/2001/WD-query-semantics-20010607/#sec_dyn_match

reflects more closely the intuitive semantics.

We appreciate your feedback on the XML Query specifications. Please
let us know if this response is satisfactory. If not, please respond
to this message, explaining your concerns.

Jerome Simeon
On behalf of the XML Query Working Group

 > -----Original Message-----
 > From: Lechner Stephan [mailto:lechner@dke.uni-linz.ac.at]
 > Sent: Wednesday, June 06, 2001 3:13 AM
 > To: www-xml-query-comments@w3.org
 > Subject: match expression's operational semantics
 > 
 > 
 > I've some difficulties in understanding the operational semantics of a
 > match-expression 
 > as described in section 5.7 of the Query Algebra Working Draft of
 > February 2001. 
 > It seems to me that, according to the specification, a case-rule might
 > return a value 
 > that does not conform to its designated type. Consider following
 > example: 
 > 
 > type Book = book [ String ] 
 > 
 > 
 > let books : Book{0..*} = book [ "XML Query" ], 
 >                          book [ "Data on the Web" ] 
 > query match books 
 >         case b : Book{3..*} do b 
 >         else error 
 > 
 > 
 > The type of the match-expression should be Book{3..*} | error. 
 > I'd like to apply the semantics defined by the rules of section 5.7 to
 > this example: 
 > 
 > 
 > The first rule sets up the apropriate environment, so that a variable v
 > holds 
 > the expression books, and all the case rules are evaluated against v. 
 > 
 > 
 > The second rule checks the first case-rule, where Var is b, Type is
 > Book{3..*}, 
 > and type(v) is, as I assume, Book{2..*}. 
 > The intersection type of type(v) and Type is Book{3..*}, i.e. not empty.
 > 
 > Therefore, the variable b is bound to books and the expression b 
 > is returned, although b holds data of a type that is to conform 
 > to Book{2..*} but not to Book{3..*}. 
 > 
 > 
 > (The precondition of the third rule is not fulfilled since the
 > intersection type in the 
 > first case-rule is not empty.) 
 > 
 > 
 > What's wrong with this consideration? 
 >

Received on Thursday, 14 June 2001 19:52:53 UTC