Development

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

                                                 |
>  >                                             |                        <
      ______Prefix_pair_________________             ____Suffix_pair_____
      |P  |P1\  |P2  |  \  Q' /  |\ /S3|\  |  \+ |? /    |\{2,}|? ? /|* |*
      >>  >>>   >>>  >>>>  |  >>>>  >>>          |  >>+ (      | )
      |   |__/  |    |P'/  |  \S'|/ \__|/  |  /  |  \    |/    |    \|  |
          empty -----non-empty---- empty                 -pair-steque-
          ---------pair-steQue----------

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 wide version of > and > spanning 2*1+1 = 3 lines
• pair P has >> as prefix and a non-empty steque of pairs (Q) that consists of three pairs (P1, P2 and S3) and is bottommost
  • pairs P1 and P2 comprise the prefix of the pair steque Q
  • S3 is a single-pair suffix of Q
• for convenience, nested pairs (comprising pair steques) have an additional element for each level of nesting
  • P2 stores a non-empty pair steque Q', whose child steque is not expanded for clarity (hence | is shown, unlike in Q)
  • pairs P' and S' form a prefix and suffix of Q', respectively, each storing an empty pair steque
• 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