Lists Home |
Date Index |
>Dare Obasanjo wrote:
>> I'm still waiting for someone with a theoretical background to debunk the
>> statements in the paper "On Database Theory and XML" that it is is an
>> unsolvable problem to guarantee that one can create a query that for any
>> given XML input will generate output that conforms to a specified XML schema.
>  http://www.cs.washington.edu/homes/suciu/files/_F2066943700.ps
> As for Suciu's claim that "When one adds joins, typechecking
> becomes undecidable" [p. 5]: I'm not quite up to debunking it,
> but it sounds bogus to me; regular languages are closed under
> cartesian product and homomorphisms, which is basically what
> a join gives you.
Having taken a look at the paper where Dan actually *proves*
this to be the case , I take that back :-)
But this paper appears to be using a stronger than usual
definition of the typechecking problem:
"Given an input DTD tau_1, an output DTD tau_2 [...],
and a query q, we say that q _typechecks_ (wrt. tau_1 and tau_2)
iff q(inst(tau_1)) [is a proper subset of] inst(tau_2)"
That is, it demands that the algorithm be both sound *and*
complete. The paper then presents some (impressive!) results
showing that this problem is decidable for certain restricted
classes of query languages and DTDs , but for "specialized DTDs"
(roughly speaking: something at the level of RELAX-NG) or full XQuery,
the typechecking problem as stated is undecidable.
On the other hand, in practice a weaker definition of typechecking
is often satisfactory: "if a query q typechecks wrt. L1 and L2,
then for all s in L1, q(s) is in L2". A guarantee from a type
checker that a program never produces bad output from good input is
a useful thing to have, even if the typechecker rejects some
 "XML with Data Values: Typechecking Revisited",
<URL: http://www.cs.washington.edu/homes/suciu/files/_F1359680672.ps >
 the term "DTD" is used in the paper as a generic term for
grammar-based schema languages, not XML DTDs per se.