Skip to content

Development

Leo Osvald edited this page Apr 11, 2016 · 17 revisions

Paper notes

In ASCII art, we use:

  • POSIX regular expression symbols * and ?, subexpressions (), bracket expressions [] and sometimes | (choice); these can be applied to colors, (pairs of) elements/deques, and operations

  • symbols ^ and v to denote pop operation followed by push level up or down (respectively), where - and _ denote the newly pushed elements unless the operation is conditional (i.e., followed by ?)

  • o (and x) to denote elements (that are removed, respectively)

  • / |, | \ and /\, to represent pairs (of elements) comprising prefix, suffix or either

  • the | symbol that spans two lines to emphasize elements cannot be transferred between ends of buffers because there is a child deque/steque (holding elements in between)

Deq - Double-ended queue without concatenation (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.

Empty smaller buffer
                 |  _ G_
     o? o? o  o  |  o  o
             v        ^
            / |?     / \
           o  o     o  o
           -  - [YX]  G
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)

TODO

Clone this wiki locally