<div dir="ltr">Like I mentioned, co-inductive types are used to deal with non-determinism in formal proofs, although I don't know enough about the subject to give an example.<br></div><div class="gmail_extra"><br><div class="gmail_quote">2016-01-29 23:29 GMT+01:00 Pavel Velikhov <span dir="ltr"><<a href="mailto:pavel.velikhov@gmail.com" target="_blank">pavel.velikhov@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Trees won’t help much here. The difficulty with path expression is due to the // step, which adds non-determinism.<div><br></div><div>//w/x subsumes /w/x/y/z/w/x</div><div>//w/w doesn’t subsume /w/x/w</div><div><br></div><div>Regular languages also have determinism and all the algorithms for them are exceptionally well-studied.</div><div>Or you can do an algorithm with backtracking, but it could get hairy.</div><div><div class="h5"><div><br></div><div><br><div><div><blockquote type="cite"><div>On 29 Jan 2016, at 20:53, W.S. Hager <<a href="mailto:wshager@gmail.com" target="_blank">wshager@gmail.com</a>> wrote:</div><br><div>This is the best I (actually Google) can do.<div><br><div>Proof:<br><a href="https://coq.inria.fr/library/Coq.MSets.MSetGenTree.html" target="_blank">https://coq.inria.fr/library/Coq.MSets.MSetGenTree.html</a><div><p dir="ltr">Test:</p><p dir="ltr"><a href="http://www.geeksforgeeks.org/check-if-a-binary-tree-is-subtree-of-another-binary-tree/" target="_blank">http://www.geeksforgeeks.org/check-if-a-binary-tree-is-subtree-of-another-binary-tree/</a></p><p dir="ltr">At some point I'll look into this myself, it's a nice challenge.</p></div><div><br></div><div>donderdag 28 januari 2016 heeft Pavel Velikhov <<a>pavel.velikhov@gmail.com</a>> het volgende geschreven:</div><div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto" style="word-wrap:break-word">Hmm.. testing subsumption is not as trivial as I thought. Here's a cleaner way to do it: represent both path expressions as DFAs and then test subsumption. You'll get DFAs A and B and then test if minimized(B-A) is empty.</div>
</blockquote></div>
</div></div><br><br>-- <br><div><p> 
W.S. Hager<br>
Lagua Web Solutions<br>
<a href="http://lagua.nl/" target="_blank">http://lagua.nl</a><br></p></div><br>
</div></blockquote></div><br></div></div></div></div></div></blockquote></div><br><br clear="all"><br>-- <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>