If you want to do a formal proof, you might want to use simplified notions of XML documents and path expressions. And do you need to take the schema into account?
Here is a good paper that defines labeled ordered tree objects, schemas and simple queries for proving stuff. (And they use all these definitions to do proofs): http://db.ucsd.edu/publications/viewDTD.pdf > 27 янв. 2016 г., в 0:15, W.S. Hager <[email protected]> написал(а): > > Here's the entry on steps: > > http://www.w3.org/TR/xquery-semantics/#id-axis-steps > > I missed it before. To be continued I guess. I'd love the idea of a sound > formal proof. > > Op dinsdag 26 januari 2016 heeft W.S. Hager <[email protected]> het volgende > geschreven: >> Hi Adam, >> >> I'm looking at the formal specification of xpath/xquery: >> http://www.w3.org/TR/xquery-semantics >> >> It would really help to start with a function that implements the actual >> selection in steps. Do you know such a function? >> >> Thanks, >> >> Wouter >> >> Op dinsdag 26 januari 2016 heeft W.S. Hager <[email protected]> het volgende >> geschreven: >>> Not really, no. But my guess is that the path is not relevant, as its steps >>> simply contain variable names. The proof you want to have is a formal one, >>> and I think it doesn't have to do with the path expression, but rather the >>> formalism it implements. >>> >>> 2016-01-26 17:41 GMT+01:00 Adam Retter <[email protected]>: >>>> Any chance you could offer me an example? ;-) >>>> >>>> On 26 January 2016 at 16:40, W.S. Hager <[email protected]> wrote: >>>> > Hi Adam, >>>> > >>>> > Perhaps it helps to start with rewriting the xpath expressions as pure >>>> > lambda expressions. Maybe that way you could apply lambda calculus? >>>> > >>>> > Cheers, >>>> > Wouter >>>> > >>>> > 2016-01-26 17:26 GMT+01:00 Adam Retter <[email protected]>: >>>> >> >>>> >> Given two simple XPaths, say: >>>> >> >>>> >> 1. //w >>>> >> >>>> >> 2. /x/y/z/w[@a = 'v'] >>>> >> >>>> >> As a human I can very easily tell without evaluating the expressions >>>> >> that (2) will return a subset (or the same set) of the results that >>>> >> (1) would return *should* they both be evaluated. >>>> >> >>>> >> My goal here is given any two simple arbitrary XPaths expressed as >>>> >> strings, and without evaluating them against a context, to determine >>>> >> whether one would return a subset of the results of the other. >>>> >> >>>> >> I wondered if there might be an algorithm or library that someone >>>> >> already had or has written which might be able to give me the answer? >>>> >> >>>> >> I realise that I can only probably cover a subset of XPath itself, but >>>> >> it is only the path steps with predicates which I am interested in. >>>> >> >>>> >> Ideally I am looking for something in Java. >>>> >> >>>> >> -- >>>> >> Adam Retter >>>> >> >>>> >> skype: adam.retter >>>> >> tweet: adamretter >>>> >> http://www.adamretter.org.uk >>>> >> _______________________________________________ >>>> >> [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 >>> >>> >>> >>> -- >>> W.S. Hager >>> Lagua Web Solutions >>> http://lagua.nl >>> >> >> >> -- >> 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
_______________________________________________ [email protected] http://x-query.com/mailman/listinfo/talk
