Skip to content

Development

Jump to bottom
Leo Osvald edited this page Apr 15, 2016 · 17 revisions

In ASCII art, we use the following symbols:

  1. {n,}/{,m} (or {n,m}) to indicate at least/most n/m (or both) repetitions (with shorthands {n}={n,n}, ?={,0}, *={0,}, +={1,}), () for grouping, | and [] for choice, all from POSIX regular expressions; these can be applied to colors, deque/steque (elements), tuples (pairs and triples)
  2. ^ and v (=) to denote a pop followed by a push to the level up or down (same level, respectively), where ~ denote the newly pushed members unless the operation is conditional (i.e., followed by ?)
  3. o (and x) to denote an element (that is removed, respectively)
  4. > and < to denote an element in a prefix or suffix, respectively, forming a buffer at the top level
  5. | \, / | and / \, to represent tuples (of elements) comprising prefix, suffix or either, respectively
  6. | /, \ | and \ /, to form multiline arrows together with 5., denoting tuples in a deque/steque
  7. | that spans two or more lines to emphasize elements cannot be transferred between ends of buffers because there is a child deque/steque, holding elements in between

(Note similarity of (multiline) arrows and | to the notation in the paper; >...< ~ [...] and | ~ [].)

This allows us to compactly represent a catenable deque/steque Q0, which is mutually recursive and roughly:

  • Qn = {} | [Tn* Qn+1 Tn*Tn] | [TnTn* Qn+1 Tn*] | [TnTn* Qn+1 TnTn, TnTn Qn+1 Tn*Tn**]**
  • Tn = (Tn-1*, Qn, Tn-1*Tn-1) | (Tn-1Tn-1*, Qn, Tn-1*) ; prefix, deque/steque of tuples, suffix
  • T0 = . ; an element

e.g, [.... [(..,{},.)(..,[(,{},..) [] (,{},.)],) [] (..,[(..,{},) [(,[{} (..,{},.)(...,{},)],) {}] (..,{},)],..)] .....] as:

            _____prefix________    c l _________suffix___________
   _prefix_ tuple  another tuple   h e      single tuple           _suffix__
l  elements ----- ---------|------ i|v --------|---------\--------  elements
e   - - - - |   \ |   | \ c|l / |\ l|e /   | \ /   | /   | / |   | - - - - -
v 0 > > > > > > < > > < < h|v <    d|l > > > > > > < > > > > > < < < < < < <
e 1         |   / |   | / i|l \ |/  |2 \   | / \   | \   | \ |   |
l 2	               pfx--- l|2 ---sfx|          |---- ----/
   	                 nested tuples             -----------
                                               child level 2

Note children of same or deeper level can optionally be nested, but at least a tuple (element) in either prefix or suffix is required at each level. (The top level can be empty if the whole deque/steque is empty.)

A full-fledged example of a tricky case of fixing invariant after popping a prefix from an Orange deque.

 Pop a triple    ^ .  .  .  .  .  .  .  .  .  .  .  .Use sfx from popped
       X~~~~~|?  . X Store its/   \* X Eject|?  .  X  . ~~~~~ or ejected
>{5,7}  >{3,}|x{3,}? sfx             x{3,}  |  x{3,}    >{3,}  >{6,7}
 Use   X pfx.|sfx. X as triple\   /  X      |tripleX
 popped  ^.& v?  = .(  _____           =    v       )?  #        .  .  .  .
 triple's. d |?  OR  : /old\? /   \* /   \ :|? d        # Note x      &  .
        .  e |i      : >{3,}         >{3,} :|C e        #     .  .
 sfx as.   q |f a    : \sfx/  \   /  \   / :|a q        # denote choice of
 pfx if    u    n    Cat them with the rest  t u        # operation on sfx
 pfx empty e    y    ~~~~~~~~~~~~~~~~~~~~~     e

COMMON OBSERVATIONS:

  1. (Every preferred path that starts at) a child of Red parent is Green if not Yellow, and regular
  2. Regular: topmost is non-Red and Semiregular; no two Reds are separated by non-Greens only
  3. Reqular Qn is still (semi)regular after a push/inject (removal from either ends, respectively)
  4. Semiregularity (regularity) is preserved by catenation (if left operand is a regular steque, respectively)
  5. Color of Qn is always the worse of those of prefix/suffix, but better if one is empty and there is no child

Deq - Double-ended queue without catenation (Section 4)

Re-establishing regularity (fix)

  • Let d be the topmost Red deque, and c be its child

Commonly used observations:

  1. The child c cannot be red (if it exists), so it must be bottommost if its either buffer is empty. Similarly, either buffer must be non-full.
  2. If c contains a single pair, it must be yellow and bottommost.
  3. If c is initially green and ultimately red it must be removed unless bottommost. (Note its first non-yellow descendant may be Red, so turning GY*R into RY*R would make it non-regular.)

Two-buffer case (c will have at most 2 buffers)

  1. If either buffer of the child is empty, transfer from the other one (okay because it is bottommost).

  2. Independently make any red/yellow buffer of d green, as follows:

     [YR]~  ~        |                 [RY]
  o? o  o        |        x  x  o  o  o?
      ^                     v     # In the worst (best) case both
     | \   | \ * |?  / |*  / |    # buffers of a child become Red
     x  x  o  o  |  o  o  o  o    # (or the child is eliminated).
               [GYRX]     -  -

Note observation #3 is not a problem:

 [YR]~  ~  |  ~  ~ [YR]    # If child changes color from G to R,
  o? o  o  |  o  o  o?     # it is eliminated (it was bottommost).
      ^         ^             G              G
     | \       / |  <===  | \   | \  OR  / |   / |
     x  x     x  x        o  o  o  o    o  o  o  o
      R    X    R

One-buffer case (c will have at most 1 buffer)

In this case, the bigger buffer of d has at least 2 elements.

0) Empty smaller buffer
                 |  ~ G~
     o? o? o  o  |  o  o
            v         ^
           | \ ?     /\
           o  o     o  o
           ~  ~ [YX]  G
1) Full bigger buffer(s)
        R        |     [GRY]           [YR]
  o  o  o  x  x  | (o  o  o?|x  x  o  o  o?)
            v      ( ^?  OR    v           )
         ( | \    /\ ?)       / |
           o  o  o  o        o  o
              [YXG]            Y

No-buffer case (c will be eliminated)

In this case, buffers of d contain at most 1 element in total. Consequently, c must contain a single pair (otherwise, d would be yellow).

 [YR]~  ~  |  R
  o? o  o  |
       ^
      /\
     x  x
       X

CatSteq - Catenable stack supporting inject (Section 5)

Let > and < denote an element that belong prefix and suffix at level 0. Similarly, let a (2*i + 1)-line string starting (ending) with |..\ (|../) or /..| (\..|) denote a pair that belongs to prefix or suffix at level i. For instance, the following

pref.                                       |
>  >                                        |                         <
      ______Prefix_pair____________             _____Suffix_pair_____
  	  P   -------pair-steQue-------                ---pair-steque--
      |   |P1\  |P2  /  |\  |  /S3|\  |  \+ |? /    |\{2,} |? ? /|* |*
      >>  >>>   >>>  >>>>   |  >>>    >>+   |  >>+ (       | )
      |   |__/  |  Q'\S'|/  |  \__|/  |  /  |  \    |/     |    \|  |
          empty      suf.  chi empty       opt.     prefix chi suf.
          steq.      only  ld  steq.      child     pairs  ld  pairs

denotes an two-level expansion of a steque with the following structure:

  • 2 (1) elements in the prefix (suffix) at the top level (i.e., level 0)
  • at least 2 pairs in the prefix at level 1 (note tall version of > and < spanning 2*1+1 = 3 lines)
  • pair P has >> as prefix and a non-empty steque of pairs (Q), which is composed of:
    • pairs P1 and P2 that comprise its prefix
    • an unexpanded child steque (note | spanning three lines)
    • S3, its single-pair suffix
  • nested pairs in P (comprising pair steques) have an additional element for each level of nesting
    • P2 stores a suffix-only pair steque Q', which is bottommost and stores a single pair S'
    • S' stores an empty pair steque
  • an optional child steque (note | followed by ?), preceded by at least one other pair that forms a prefix
  • any valid number of suffix pairs at level 1, as described by the regular expression on the right-hand side of level 1

CatDeq - Catenable Double-ended queue (Section 6)

CATENATE

Some buffers are empty (in Only without children)

Subcase: In both deques (4.)

  • Combine into >{8,} if one is x{,7}, or >{,8} <{,8} otherwise.

Subcase: In first (symmetrically last) deque only (2. & 3.)

  new pfx
------------                  |?   only OR left |?
>{,8}? >{5,} x+    :  x{5,}   |   (<{6,}|, >  > | <{6,})
 .     ~~~~~  v?
  .          /   \?         /   \*
   OR .  .  .>{8,}
             \   /          \   /
             ---------------------
                maybe new child

All 2-4 buffers are non-empty

Subcase: Only without child (1d.)

 old pfx          old sfx      old pfx        old sfx
  -----         ----------      -----      --------------
( >{5,} >{3,6}  x{3,6} < <  OR  >{5,} >{3} x{3} <{4,} < < )  : Q0
        ~~~~~~         ---            ~~~~       v    ---
  ------------         new      ----------      /   \ new
  new pfx            sfx        new pfx         <{4,} sfx
                                                \   /
                                                ~~~~~

Subcase: Only with child (1c.)

          |
  >{5,}   |    <{3,} < <  : Q0
          =     v    ---
        /   \+ /   \ new
               <{3,} sfx
        \   /  \   /
               ~~~~~
        ------------
          new child

Subcase: Left without child and Right -> Only (1b.)

      old sfx
         ----       |?
  >{5,}  o  o, o  o | <{5,}  : Q0
  -----------------
      new pfx

Subcase: Left with child and Right (1a.)

          |               |?
  >{5,}   |    <  <, >  > | <{3,} < <  : Q0
          =      v    v   v       ---
        /   \+ /          |?    \ new
               >  >  >  > | <{3,} sfx
        \   /  \          |     /
               ~~~~~~~~~~~~~~~~~~
        -------------------------
            new child

POP: Fixing after popping the prefix that causes the Redness

  • semiregularity implies a regular child deque, which exists due to color shift

Left and Right, or Only with neither prefix nor suffix of size less than 8

Subcase: First triple's either buffer is empty (no child deque)

        ~~~~~     |            only OR left |?
   >{5} >{3,}     |      <  < (<{6,}|, >  > |  <{6,})
          ^
Pop a  X     X  /   \*
triple  x{3,}
& use  X buf X  \   /
non-empty       ~~~~~~

Subcase: First triple's buffers are non-empty (possible child deque)

 Pop a triple
       X~~~~~|?    X Store its  |          only OR left |?
>{5,7}  >{3,}| x{3,} sfx        |    <  < (<{6,}|, >  > |  <{6,})
 Use   X pfx |   . X as triple
 popped  ^ & v   = .   _____                            #     x
 triple's  d |?  AND : /old\  /   \*                    # Note  .  denotes
         C e |i a    : >{3,}                            #         .
         a q |f n    : \sfx/  \   /                     #           .
         t u    y  with the new rest                    # operation on sfx
           e ~~~~~~~~~~~~~~~~~~~~~~~

Only with both prefix and suffix of size less than 8

 Pop a triple    ^ .  .  .  .  .  .  .  .  .  .  .  .Use sfx from popped
       X~~~~~|?  . X Store its/   \* X Eject|?  .  X  . ~~~~~ or ejected
>{5,7}  >{3,}|x{3,}? sfx             x{3,}  |  x{3,}    >{3,}  >{6,7}
 Use   X pfx.|sfx. X as triple\   /  X      |tripleX
 popped  ^.& v?  = .(  _____           =    v       )?  #        .  .  .  .
 triple's. d |?  OR  : /old\? /   \* /   \ :|? d        # Note x      &  .
        .  e |i      : >{3,}         >{3,} :|C e        #     .  .
 sfx as.   q |f a    : \sfx/  \   /  \   / :|a q        # denote choice of
 pfx if    u    n    Cat them with the rest  t u        # operation on sfx
 pfx empty e    y    ~~~~~~~~~~~~~~~~~~~~~     e
Clone this wiki locally