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

[Pavel Velikhov]

> 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.