23 Inclusion transform on lists

Let [] denote the empty list. Let A+B denote the concatentation of lists A and B.

Definition: We say a list of atomic operations L = [O1 ... On] is contextually serialised if the output state of each operation equals the input state of the next operation in the sequence. i.e. for each i, stateout(Oi)=statein(Oi+1). This means the operations can be executed in the order they appear in the list.

Definition: We define statein and stateout on a list of operations as follows: Given a list L = [O1 ... On] of contextually serialised atomic operations, let statein(L) = statein(O1) and stateout(L) = stateout(On).

Definition: Let L1, L2 be linear lists of contextually serialised atomic operations. We say L1, L2 are context equivalent if statein(L1) = statein(L2).

Definition: Let L1, L2 be context equivalent linear lists of atomic operations. IT(L1, L2) denotes the inclusion transform of L1 past L2 and is defined recursively as follows

  1. IT([], []) = []
  2. IT(L1 + L2, L3) = IT(L1,L3) + IT(L2, IT(L3, L1))
  3. IT(L1, L2 + L3) = IT(IT(L1, L2), L3)

[Note that this definition appears to be ambiguous in the way in which a list is decomposed into smaller sub-lists. However, it turns out that the final result is independent of the order in which the lists are decomposed. A more formal approach could begin with an unambiguous definition then prove decomposition rules 2,3 above]

We can depict IT(L1,L2) pictorially as follows. L2 has three primitive operations and L1 has four primitive operations. The initial document state S is associated with the bottom left corner of the 3 x 4 grid of "cells".

Starting from the bottom left corner we can apply IT on the atomic operations. This can proceed to adjacent cells until we transform the operations to the top and right boundaries.

Note that IT is quadratic in the size of the lists.

Lemma: TP1 ⇒ ∀ L1,L2, (L1+IT(L2, L1)) ~ (L2+IT(L1, L2))

Proof :

A formal proof can be achieved using induction on the length of L1,L2. Informally, we can prove the result more easily as follows

We begin with L1+IT(L2, L1), which is associated with the path along the bottom and right edges. Starting from the bottom right corner we can shift the path using the known convergence property on the cell. This is repeated for adjacent cells until the path is transformed to the left and top edges, corresponding to L2+IT(L1, L2).