[Bug 3273] [FS] technical: 2.3.1 Formal values: () in Values

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





------- Comment #5 from simeon@us.ibm.com  2006-06-13 01:05 -------
...
> > * 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

Received on Tuesday, 13 June 2006 01:05:48 UTC