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

[Christian Grün]

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

…absolutely. If theory is applied at the very beginning, it may
prevent you from doing things that no one wants to prove later on.



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