<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto"><div><br></div><blockquote type="cite"><div dir="ltr">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)?</div></blockquote><div><br></div>Okay, now we are close! However now formal do you want the proof to be? I can give this informal proof:<div><br></div><div>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.</div><div><br></div><div>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. <br><div><br></div><br><blockquote type="cite"><div><div class="gmail_extra"><div class="gmail_quote">2016-01-27 17:46 GMT+01:00 Christian Grün <span dir="ltr"><<a href="mailto:christian.gruen@gmail.com" target="_blank">christian.gruen@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">> Well, so, to continue, let's assume that there are no user-defined<br>
> functions, and in fact the only thing we want to proof is select+filter,<br>
> where a filter is limited to the default operators. From that is it follows<br>
> that<br>
><br>
> -path1:<br>
> select-child-nodes-by-name(select-child-nodes-by-name($context,'x'),'w')<br>
> -path2: select-descendant-nodes-by-name($context,'w')<br>
<br>
</span>Just to complete this: The predicate must not be numeric (//w[1] is<br>
not equivalent to /descendant::w[1]).<br>
<div><div class="h5"><br>
<br>
<br>
> Op woensdag 27 januari 2016 heeft daniela florescu <<a href="mailto:dflorescu@me.com">dflorescu@me.com</a>> het<br>
> volgende geschreven:<br>
>><br>
>> ><br>
>> > It seems to be a long-standing tradition that computer scientists, when<br>
>> > asked to prove a difficult conjecture C, respond by giving a proof for a<br>
>> > simplified conjecture C'. While this might lead to progress in the long run,<br>
>> > and enables them to get papers published in the academic literature, it is<br>
>> > totally useless to practical engineeers who want to know whether they can<br>
>> > safely rely on C.<br>
>><br>
>> Michael,<br>
>><br>
>><br>
>> what you say is nice and true.<br>
>><br>
>> However given that:<br>
>> 1. path expressions point (syntactically hence esemantically) into<br>
>> XQuery’s expressions<br>
>> 2. XQuery expression language is Turing complete<br>
>> 3. Subsumption for a Turing complete language is undecidable.<br>
>><br>
>> Well, I can hardly see a way to decide this problem other then by<br>
>> introducing SOME restrictions<br>
>> of some sort… but of course some restrictions that would not nullify the<br>
>> original problem all together<br>
>> and make the solution useless.<br>
>><br>
>> Best,<br>
>> Dana<br>
><br>
><br>
><br>
> --<br>
><br>
> W.S. Hager<br>
> Lagua Web Solutions<br>
> <a href="http://lagua.nl" rel="noreferrer" target="_blank">http://lagua.nl</a><br>
><br>
><br>
><br>
</div></div>> _______________________________________________<br>
> <a href="mailto:talk@x-query.com">talk@x-query.com</a><br>
> <a href="http://x-query.com/mailman/listinfo/talk" rel="noreferrer" target="_blank">http://x-query.com/mailman/listinfo/talk</a><br>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div>
<p>
W.S. Hager<br>
Lagua Web Solutions<br>
<a href="http://lagua.nl/" target="_blank">http://lagua.nl</a><br></p></div></div>
</div>
</div></blockquote></div></body></html>