Re: [xml] Correct behaviour of RelaxNG interleave

[Bjoern Hoehrmann <derhoermi gmx net>]

* Daniel Veillard wrote:
> I don't see the reduction rule which would be equivalent to flattening out
> to a single interleave. The interleaves are at that point in a binary form,
> explain because I don't see how your draw that conclusion.

We know that per (interleaves 1) the following is true:

  () interleaves () ; ()

Applying (interleaves 2) with m4 := <d/> yields

  <d/>,() interleaves () ; <d/>,()

Applying (interleaves 3) with m4 := <b/> yields

  <b/><d/> interleaves <b/> ; <d/>

Applying (interleaves 2) with m4 := <c/> yields

  <c/><b/><d/> interleaves <b/> ; <c/><d/>

Applying (interleaves 3) with m4 := <a/> yields

  <a/><c/><b/><d/> interleaves <a/><b/> ; <c/><d/>

(I used that (),x = x,() = x as defined in the specification).

The <interleave> semantics are as follows:

  cx |- a1 ; m1 =~ p1   cx |- a2 ; m2 =~ p2   m3 interleaves m1 ; m2
  ------------------------------------------------------------------
        cx |- a1 + a2 ; m3 =~ <interleave> p1 p2 </interleave>

With m1 := <a/><b/>, m2 := <c/><d/>, m3 := <a/><c/><b/><d/>, p1 :=
<interleave>a b</interlave>, and p2 := <interleave>c d</interleave>:

  cx |- a1 ; <a/><b/> =~ <interleave>a b</interlave>  (assumed true)
  cx |- a2 ; <c/><d/> =~ <interleave>c d</interleave> (assumed true)
  <a/><c/><b/><d/> interleaves <a/><b/> ; <c/><d/>    (proof above)
  ------------------------------------------------------------------
               cx |- a1 + a2 ; <a/><c/><b/><d/> =~
               <interleave>
                 <interleave>a b</interlave>
                 <interleave>c d</interleave>
               </interleave>

I have ignored attributes here since there are none.
-- 
Björn Höhrmann · mailto:bjoern hoehrmann de · http://bjoern.hoehrmann.de
Weinh. Str. 22 · Telefon: +49(0)621/4309674 · http://www.bjoernsworld.de
68309 Mannheim · PGP Pub. KeyID: 0xA4357E78 · http://www.websitedev.de/