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

[Pavel Velikhov]

> 
> To take an example, if someone proves that a particular equivalence holds on a simplified data model with no attribute, namespace, comment, or processing instruction nodes, then that is of absolutely no use to someone writing an optimizer for a product in which such nodes can be encountered.
> 
> Michael Kay
> Saxonica
> 

Michael, even in this case, with these simplifying assumptions, there is a very good chance that the equivalence will hold on the full data model. You can also do a 1-to-1 mapping of the full data model to the simplifed one. And an optimiser developer can read the proof procedure and extend it pretty easily with all the gory details.

But if somebody proves that the equivalence is undecidable - it definitely will hold for the full data model. So you can forget about a general method in the optimiser and immediately go for special cases.

So I don’t agree that all proofs are useless. And also we see that a lot of functional languages cleaned up their semantics precisely because they wanted to prove things.

> 
>> On 27 Jan 2016, at 09:51, Pavel Velikhov <pavel.velikhov at gmail.com> wrote:
>> 
>> 
>>> 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.
>> 
> 
>