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

[Pavel Velikhov]

A user-defined function in any reasonable language (including Haskell and XQuery) is Turing-complete.

So you cannot prove that:
  - two functions are equivalent
  - the functions terminate
  - basically any non-trivial fact

Unless you make some strong assumptions about these functions.

> On 27 Jan 2016, at 13:31, W.S. Hager <wshager at gmail.com> wrote:
> 
> There's the notion of co-inductive types. I think in Haskell you could proof the case, so why not in xquery?
> 
> 2016-01-27 11:24 GMT+01:00 Pavel Velikhov <pavel.velikhov at gmail.com <mailto:pavel.velikhov at gmail.com>>:
> 
>> 
>> Indeed, the expressions should terminate.
> 
> Since you can include a function call in your path expression, and you can include your own custom function, there is
> no guarantee that the expression will terminate.
> 
> I.e. you need to take a subset of possible path expression already, in general case the problem is undecidable.
> 
>> 
>> 2016-01-27 11:11 GMT+01:00 Pavel Velikhov <pavel.velikhov at gmail.com <mailto:pavel.velikhov at gmail.com>>:
>> 
>>> 
>>> Or simplified: is the set selected by p1 equal to the set selected by p2?
>> 
>> If we allow p1 and p2 to be arbitrary XQuery path expressions, then its undecidable.
>> I can reduce the halting problem of Turing machines to this test.
>> 
>>> 
>>> 2016-01-27 11:09 GMT+01:00 W.S. Hager <wshager at gmail.com <mailto:wshager at gmail.com>>:
>>> Isn't the constraint in this case the test: is p2 a subset of p1?
>>> 
>>> 2016-01-27 11:04 GMT+01:00 Pavel Velikhov <pavel.velikhov at gmail.com <mailto:pavel.velikhov at gmail.com>>:
>>> 
>>> > On 27 Jan 2016, at 12:54, W.S. Hager <wshager at gmail.com <mailto:wshager at gmail.com>> wrote:
>>> >
>>> > Can't we formally proof something as obvious Adam's case?
>>> 
>>> In Adam’s case we want to test whether path expression p1 subsumes path expression p2.
>>> If we don’t put any conditions on p1 and p2, the problem is undecidable: p1 and p2 may include
>>> function calls, so the expressive power of p1 and p2 are that of a Turing Machine.
>>> 
>>> 
>>> 
>>> -- 
>>> W.S. Hager
>>> Lagua Web Solutions
>>> http://lagua.nl <http://lagua.nl/>
>>> 
>>> 
>>> 
>>> -- 
>>> W.S. Hager
>>> Lagua Web Solutions
>>> http://lagua.nl <http://lagua.nl/>
>> 
>> 
>> 
>> 
>> -- 
>> W.S. Hager
>> Lagua Web Solutions
>> http://lagua.nl <http://lagua.nl/>
> 
> 
> 
> 
> -- 
> W.S. Hager
> Lagua Web Solutions
> http://lagua.nl <http://lagua.nl/>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://x-query.com/pipermail/talk/attachments/20160127/bf6a4081/attachment.html>