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 <[email protected]> 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 <[email protected] > <mailto:[email protected]>>: > >> >> 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 <[email protected] >> <mailto:[email protected]>>: >> >>> >>> 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 <[email protected] >>> <mailto:[email protected]>>: >>> 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 <[email protected] >>> <mailto:[email protected]>>: >>> >>> > On 27 Jan 2016, at 12:54, W.S. Hager <[email protected] >>> > <mailto:[email protected]>> 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/>
_______________________________________________ [email protected] http://x-query.com/mailman/listinfo/talk
