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

[W.S. Hager]

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.

2016-01-29 23:29 GMT+01:00 Pavel Velikhov <pavel.velikhov at gmail.com>:

> Trees won’t help much here. The difficulty with path expression is due to
> the // step, which adds non-determinism.
>
> //w/x subsumes /w/x/y/z/w/x
> //w/w doesn’t subsume /w/x/w
>
> Regular languages also have determinism and all the algorithms for them
> are exceptionally well-studied.
> Or you can do an algorithm with backtracking, but it could get hairy.
>
>
> On 29 Jan 2016, at 20:53, W.S. Hager <wshager at gmail.com> wrote:
>
> This is the best I (actually Google) can do.
>
> Proof:
> https://coq.inria.fr/library/Coq.MSets.MSetGenTree.html
>
> Test:
>
>
> http://www.geeksforgeeks.org/check-if-a-binary-tree-is-subtree-of-another-binary-tree/
>
> At some point I'll look into this myself, it's a nice challenge.
>
> donderdag 28 januari 2016 heeft Pavel Velikhov <pavel.velikhov at gmail.com>
> het volgende geschreven:
>
>> 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.
>>
>
>
> --
>
> W.S. Hager
> Lagua Web Solutions
> http://lagua.nl
>
>
>


-- 

W.S. Hager
Lagua Web Solutions
http://lagua.nl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://x-query.com/pipermail/talk/attachments/20160201/ea18bfc9/attachment.html>