Re: [xml-dev] Relax-ng test suites & sample data?; Pre-pre-announce: relax-ng subtype checker

[Dan Shoutis <dan.shoutis@gmail.com>]

> Can you tell more about how your "regular hedge grammar subtype prover"
> works?

Certainly; I'm not the one who came up with it so here are some
references -- and thank you for yours, a quick glance indicates that
it's taking a slightly different approach & may be very worthwhile to
read:

"Type checking in XOBE". I followed a few of its bibliographic links
as well, but this was the main paper I followed along.
http://doesen0.informatik.uni-leipzig.de/proceedings/paper/64.pdf

"An algorithm for relax ng validation":
http://www.thaiopensource.com/relaxng/derivative.html#Computing_nullable

The 2nd one is a validation approach that is very similar to the
subtype-proof approach. It works by consuming a symbol from the
instance being validated and deriving a "derivative" grammar that is
the original one with that symbol removed.

The subtyping proof is very similar -- if proving (a <= b), it will
collect all potential initial symbols from a, then derive a' and b'
for each of those symbols, then recurse for each (a' <= b').  If there
are no b', then a >= b.You can see this will work if the left-hand
grammar does not recurse & has no infinite sequences.

Next, observe that recursion in a relax-ng grammar is restricted to
"tail position": that is, recursion must be the last thing to occur in
any sequence -- so for any sequence, the very last bit to prove is the
recursive bit. This leads to a simple solution for solving recursion:
While going on to prove each a' <= b'; we add an assumption that a <=
b. If a and b are encountered again, just return true right away.

This trick also works for infinite sequences, although not because of
tail position.

Finally, there are various early outs & ways of structuring things to
try and avoid some of the n^2 worst-case behavior that will come up in
the main algorithm; these are described in the XOBE paper.

-- Dan