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

[Pavel Velikhov]

>> 
>> If you want to do a formal proof, you might want to use simplified notions of XML documents and path expressions. 
> 
> It seems to be a long-standing tradition that computer scientists, when asked to prove a difficult conjecture C, respond by giving a proof for a simplified conjecture C'. While this might lead to progress in the long run, and enables them to get papers published in the academic literature, it is totally useless to practical engineeers who want to know whether they can safely rely on C.

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.

> 
> Michael Kay
> Saxonica
> 
> 
>