Okay thanks to everyone for the replies. I think the scope of what I was looking for got thrown out in all the discussion, or perhaps I wasn't clear enough early in my initial post.
I am not interested in XQuery, and I am only interested in a small subset of XPath. I am concerned with comparing two path expressions, these path expressions may have predicates, what I didn't make clear is that those predicates may not contain functions, only the comparison operators eq, ne, gt, ge, lt, le, and =, !=, >, >=, <, <=. As Christian observed, [1] is not the same as [@a eq 'b']. In my original post, I posed these two path expressions: 1. //w 2. /x/y/z/w[@a = 'v'] In this instance I can actually ignore the predicate, as I can see that /x/y/z/w would already produce the subset of //w and the predicate only serves to restrict that further. I am not looking for a formal proof in any sense. I am looking for something practical that I can use in code. On 28 January 2016 at 09:55, Pavel Velikhov <[email protected]> wrote: > > Finally, can it be proved that /w[@a=b] is a subset of /w, taking into > account that the filter can only contain standard operators (eq, gt, lt, etc > as defined in the op namespace)? > > > Okay, now we are close! However now formal do you want the proof to be? I > can give this informal proof: > > The first path expression selects some subset of the children of the node > that it applies, where the label is 'w'. The second one selects all > descendants with label 'w', hence it's result contains all nodes of the > first path expression. > > But if you want to go formal, you need to use the semantics of XQuery path > expressions, as well as the formal specification of the data model. There > used to be a formal document on XQuery data model. > > > > 2016-01-27 17:46 GMT+01:00 Christian Grün <[email protected]>: >> >> > Well, so, to continue, let's assume that there are no user-defined >> > functions, and in fact the only thing we want to proof is select+filter, >> > where a filter is limited to the default operators. From that is it >> > follows >> > that >> > >> > -path1: >> > select-child-nodes-by-name(select-child-nodes-by-name($context,'x'),'w') >> > -path2: select-descendant-nodes-by-name($context,'w') >> >> Just to complete this: The predicate must not be numeric (//w[1] is >> not equivalent to /descendant::w[1]). >> >> >> >> > Op woensdag 27 januari 2016 heeft daniela florescu <[email protected]> >> > het >> > volgende geschreven: >> >> >> >> > >> >> > 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. >> >> >> >> Michael, >> >> >> >> >> >> what you say is nice and true. >> >> >> >> However given that: >> >> 1. path expressions point (syntactically hence esemantically) into >> >> XQuery’s expressions >> >> 2. XQuery expression language is Turing complete >> >> 3. Subsumption for a Turing complete language is undecidable. >> >> >> >> Well, I can hardly see a way to decide this problem other then by >> >> introducing SOME restrictions >> >> of some sort… but of course some restrictions that would not nullify >> >> the >> >> original problem all together >> >> and make the solution useless. >> >> >> >> Best, >> >> Dana >> > >> > >> > >> > -- >> > >> > W.S. Hager >> > Lagua Web Solutions >> > http://lagua.nl >> > >> > >> > >> > _______________________________________________ >> > [email protected] >> > http://x-query.com/mailman/listinfo/talk > > > > > -- > > W.S. Hager > Lagua Web Solutions > http://lagua.nl -- Adam Retter skype: adam.retter tweet: adamretter http://www.adamretter.org.uk _______________________________________________ [email protected] http://x-query.com/mailman/listinfo/talk
