3273
2006-05-11 08:08:39 +0000
[FS] technical: 2.3.1 Formal values: () in Values
2006-10-19 19:47:14 +0000
1
1
1
Unclassified
XPath / XQuery / XSLT
Formal Semantics 1.0
Candidate Recommendation
All
All
CLOSED
WORKSFORME
P2
normal
---
1
jmdyck
simeon
public-qt-comments
oldest_to_newest
9749
0
jmdyck
2006-05-11 08:08:39 +0000
2.3.1 Formal values
[7 (Formal)] Value ::= Item | (Value "," Value) | ("(" ")")
Presumably, the Value () represents the empty sequence. (I don't think
the FS actually says so; maybe it should.) The odd thing is that this
production allows Values with () *within* them. E.g., Value derives
1 of type xs:integer, (), (), "a" of type xs:string
Since an item (in a sequence) can't be the empty sequence, what is the
point of such a Value? (Please note that I'm talking about Values, not
Exprs.)
At first, I thought it was just a mistake in the production, so I was
going to suggest an (editorial) change to:
Value ::= "(" ")" | Item ("," Item)*
But then I noticed the example in 8.2.3.2, which actually shows a Value
with embedded ()'s. The following Note ("while preserving the structure
of the sequence") appears to indicate that the embedded ()'s are
essential to the workings of the 'test' judgment (though as far as I
can tell, they aren't).
Moreover, the inference rule 4.3.1 / DEv / rule 1 appears happy to
construct such values. E.g., I can use it to conclude that
dynEnv |- 1, () => 1 of type xs:integer, ()
I would have expected the resulting Value to be just
1 of type xs:integer
So maybe it's more than an editorial matter.
(On a related note, the corresponding STA rule allows me to conclude:
statEnv |- 1, () : xs:integer, empty
but presumably the Type should be just xs:integer.)
9939
1
simeon
2006-06-05 21:41:52 +0000
Michael,
The ability to use the empty sequence (resp. the empty type) for values (resp. types). Is intentional.
For values, the values follows the same rules as the corresponding sequence constructors in XQuery. so (),((),1,()),2 = 1,2. I believe there used to be a sentence about that in the formal values section.
For types, there are many expressions which generate sequences or unions of empty types. (e.g., if Expr then () else 1). Fortunately all those types are equivalent ((), xs:integer = xs:integer ; () | xs:integer = xs:integer?, etc.).
That is covered by the subtyping/equivalence rules in 8.3.2 Subtyping (<:).
So I believe this may be editorial, although I'm not sure what you think would help clarify. I would recommend at least to add the sentence about values (explaining the first part above)
Best,
- Jerome
9943
2
jmdyck
2006-06-06 00:12:44 +0000
I think you misunderstood me somewhat. Please note that I'm talking about "Values" (i.e., syntactic objects that can be derived from the symbol 'Value') as distinct from "values" (i.e., members of an abstract value space). (Similarly for Type vs type.) I agree with what you say about values & the empty sequence, or types & the empty type, but what concerns me is that the formal machinery that operates on Values and Types doesn't reflect what we know to be true of values and types.
To repeat, the inference rules allow me to conclude:
dynEnv |- 1, () => 1 of type xs:integer, ()
but I can find no way to conclude:
dynEnv |- 1, () => 1 of type xs:integer
Similarly, I can conclude:
statEnv |- 1, () : xs:integer, empty
but not:
statEnv |- 1, () : xs:integer
In each case, I think the latter conclusion is necessary to satisfy premises elsewhere, but it's unreachable.
Perhaps we need rules such as
dynEnv |- Expr => Value, ()
-----------------------------
dynEnv |- Expr => Value
and
statEnv |- Expr : Type, empty
------------------------------
statEnv |- Expr : Type
9971
3
simeon
2006-06-12 17:17:39 +0000
Michael,
Some more thoughts on that thread. Notably a few things:
* I can't think of a place where we get in trouble with this at this point. The type infered can be xs:integer,() or many other more complex types.
* There are may syntactic variations for the same type (T | () or T?, T* or T+|() or T?+, T*,T or T,T* etc.). To the best of my knowledge there is no finite set of rules to define those equivalances.
* It seems that those rules would merely reinvent the notion of equivalence that is already in section 8.3.2.
- Jerome
9980
4
jmdyck
2006-06-12 23:23:16 +0000
(In reply to comment #3) [in a slightly different order]
>
> * It seems that those rules would merely reinvent the notion of equivalence
> that is already in section 8.3.2.
Do the rules of 8.1.4 "reinvent" the notion of type lookup, or those of section 8.5.1 "reinvent" the notion of type promotion? Not really, they just *formalize* those notions. Similarly for rules that would formalize the notion of type equivalence.
> * There are may syntactic variations for the same type (T | () or T?, T* or
> T+|() or T?+, T*,T or T,T* etc.). To the best of my knowledge there is no
> finite set of rules to define those equivalances.
According to 8.3.1, "the structural component of the [XPath/XQuery] type system can be modeled by regular expressions", so equivalence of two Types presumably reduces to equivalence of two regular expressions, for which algorithms exist. So I imagine you could express it with a finite set of rules, though you probably wouldn't want to.
> * I can't think of a place where we get in trouble with this at this point.
> The type infered can be xs:integer,() or many other more complex types.
This is the main point, I think; if the inability to conclude
dynEnv |- 1, () => 1 of type xs:integer
or
statEnv |- 1, () : xs:integer
doesn't actually cause problems in the inference process, then the other points are irrelevant.
I *thought* I had examples of problems, but now they're deserting me, hiding behind unformalized things like subtyping and built-in functions. However, it doesn't seem like the FS was written in such a way as to *guarantee* the absence of such problems, so they might still be out there. I'll let you know if I find one.
9981
5
simeon
2006-06-13 01:05:41 +0000
...
> > * It seems that those rules would merely reinvent the notion of equivalence
> > that is already in section 8.3.2.
>
> Do the rules of 8.1.4 "reinvent" the notion of type lookup, or thoseof section
> 8.5.1 "reinvent" the notion of type promotion? Not really, they just
> *formalize* those notions. Similarly for rules that would formalize the notion
> of type equivalence.
>
sorry I wasn't clear. the purpose of 8.5.1 is to be a replacement for such rules
(which as far as I know can't be written using the inference rules notations --
see below).
> > * There are may syntactic variations for the same type (T | () or T?, T* or
> > T+|() or T?+, T*,T or T,T* etc.). To the best of my knowledge there is no
> > finite set of rules to define those equivalances.
>
> According to 8.3.1, "the structural component of the [XPath/XQuery]
> type system
> can be modeled by regular expressions", so equivalence of two Types presumably
> reduces to equivalence of two regular expressions, for which algorithms exist.
Right and the typical algorithms for regular expression operations usually
go through automatas which is what 8.5.1 is about.
> So I imagine you could express it with a finite set of rules, though you
> probably wouldn't want to.
>
Actually I believe I recall there is a theoretical result showing there isn't a finite
set of rules. The reference eludes me though. If I recall you can build a family
of regexps of depth n for which you would need a number of rules depending on n.
something along those lines. In addition, it seemed that this kind of treatment
would take a lot of space and be mostly reproducing state of the art material
from the literature on regexp/FSAs and I believe the WGs decided not to go there.
> > * I can't think of a place where we get in trouble with this at this point.
> > The type infered can be xs:integer,() or many other more complex types.
>
> This is the main point, I think; if the inability to conclude
> dynEnv |- 1, () => 1 of type xs:integer
> or
> statEnv |- 1, () : xs:integer
> doesn't actually cause problems in the inference process, then the
> other points
> are irrelevant.
>
> I *thought* I had examples of problems, but now they're deserting me, hiding
> behind unformalized things like subtyping and built-in functions. However, it
> doesn't seem like the FS was written in such a way as to *guarantee* the
> absence of such problems, so they might still be out there. I'll let you know
> if I find one.
I believe that the FS was designed in such a way that locations where you would
get into such problems are checked through subtyping.
Based this your last commentis it ok with you if we close that bug now without action?
Thanks,
- Jerome
10930
6
simeon
2006-08-01 12:54:51 +0000
Michael,
Since there does not seem to be any specific issue or fix suggested at this point, so the working groups have decided to close that issue with no action.
Best,
- Jerome