[XML-DEV Mailing List Archive Home] [By Thread] [By Date] [Recent Entries] [Reply To This Message]

Re: Relax-ng test suites & sample data?; Pre-pre-announce: rel

• To: xml-dev@l...
• Subject: Re: Relax-ng test suites & sample data?; Pre-pre-announce: relax-ng subtype checker
• From: Dan Shoutis <dan.shoutis@g...>
• Date: Fri, 21 Oct 2005 09:13:21 -0600
• Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=fo35NvQ1poDlE5IBxUmPN6kzG/3PX2PM3ERF/oUln5j13FDRy+CvFu8knIcGb1NN+OSDyjvdtQTqBPXuKuAFlF7q1GOm9NZHma8PhHWpL02jhifhrVASqZioTKcSy/qpj5Ip5dc5qYqe59G+kjtn7ltjCWCM3bV/EfcDUeZezNQ=
• In-reply-to: <48be98d70510210803x1cd588cbwd6d1acdae0652e51@m...>
• References: <48be98d70510201848x52ec40f2q87601ccabe7f44d@m...> <43588CDC.2030504@b...> <48be98d70510210803x1cd588cbwd6d1acdae0652e51@m...>

> 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

• Follow-Ups:
  • Re: Relax-ng test suites & sample data?; Pre-pre-announce: relax-ng subtype checker
    • From: Daniel Veillard <veillard@g...>

• References:
  • Relax-ng test suites & sample data?; Pre-pre-announce: relax-ng subtype checker
    • From: Dan Shoutis <dan.shoutis@g...>
  • Re: Relax-ng test suites & sample data?; Pre-pre-announce:relax-ng subtype checker
    • From: Anders Møller <amoeller@b...>

• Prev by Date: RE: Getting attributes of XML from XSD...
• Next by Date: RE: Getting attributes of XML from XSD...
• Previous by thread: Re: Relax-ng test suites & sample data?; Pre-pre-announce:relax-ng subtype checker
• Next by thread: Re: Relax-ng test suites & sample data?; Pre-pre-announce: relax-ng subtype checker
• Index(es):
  • Date
  • Thread