[xquery-talk] Function for determining one XPath as subset of another

[W.S. Hager]

Can't we formally proof something as obvious Adam's case?

2016-01-27 10:51 GMT+01:00 Pavel Velikhov <pavel.velikhov at gmail.com>:

>
> > On 27 Jan 2016, at 12:37, Christian Grün <christian.gruen at gmail.com>
> wrote:
> >
> >> Its a common practice for everybody, who needs to come up with formal
> proofs. You start with the most simplified definitions possible, that
> capture the essence of the problem.
> >> Then you get the skeleton of the proof that is hopefully very simple.
> Then you can add details back, hoping that the proof remains simple and
> tractable.
> >>
> >> So imagine starting the proof while considering all the possible
> variations of path expressions, all the Infoset stuff, all XML Schema
> details. I think its hopeless.
> >
> > I’m completely in line with Michael’s observations. It would obviously
> > be nice to have proofs for the full rule sets of the discussed
> > languages; but as experience shows, no one will do it (the rare
> > exception might prove the rule), so we are stuck with the work that is
> > of limited practical use.
>
> I can’t agree with you. There are a lot of results that automatically hold
> for the full specification, even though they are
> proved on a clean and easy-to-use subset: undecidability and
> np-completeness or np-hardness for instance.
>
> For the full specifications its sometimes hard to grasp the semantics, so
> proving anything serious is impossible.
> Example: try proving that SQL-2003 queries are equivalent to some superset
> of relational algebra.
>
>


-- 

W.S. Hager
Lagua Web Solutions
http://lagua.nl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://x-query.com/pipermail/talk/attachments/20160127/8d96be5d/attachment.html>