> 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
