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 <[email protected]>: > 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 <[email protected]> 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 <[email protected]> > 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
_______________________________________________ [email protected] http://x-query.com/mailman/listinfo/talk
