Skip to content

Development

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

Paper notes

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 level up or down (respectively), where - and _ denote the newly pushed elements 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

For instance, [.... [(..,{},.)(..,[(,{},..) [] (,{},.)],) [] (..,[(..,{},) [(,[{} (..,{},.)(...,{},)],) {}] (..,{},)],..)] .....] can be represented as follows (empty sequence of Tn is blank):

            _____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.)

Common observations

  1. (Every preferred path that starts at) a child of Red parent is Green if not Yellow, and regular
  2. Reqular Qn is still (semi)regular after a push/inject (removal from either ends, respectively)
  3. Semiregularity (regularity) is preserved by catenation (if left operand is a regular steque, respectively)
  4. 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.

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