Chapter 4: The Palimpsest Model
In this chapter, I will present a formal model of the Palimpsest sequence data type. The
presentation will include some simple proofs of consistency and properties of the model that
show that it can be used to meet the requirements for flexible, divergence tolerant collabo-
ration. The definitions in this chapter are meant to make the intuitions discussed in Chapter
3precise, and the proofs are to guarantee that the definitions are consistent and useful.
4.1 The traditional model of changes
The simplest model is the one used by most file-difference algorithms, and is the usual
one in discussions of text editing and undo. It uses the simplest possible operation set to
achieve version-completeness. Each state of a sequence is affected by one of two possible
kinds of operation: insertion of some elements into the sequence or deletion of some subse-
quence of elements. This model cannot directly represent such operations as move and copy.
Move is represented as a pair of operations, a simple insertion (representing a copy), and a
deletion (of the source data). Copy,is simply an insertion; there is no connection between
the source of the copy, and the new text inserted by it. This kind of representation is inher-
ently static, although it is well suited to implementing version-complete systems.
The standard formalism represents a history as a sequence of operations O
1 …O
k .Each op-
eration is either an insertion operation or a deletion operation, applied a sequence of data
items, D
1 ,…D
n .Whether the initial sequence is empty or contains an initial value, does not
affect the formal model. An insertion is a pair (i, seq)
consisting of an offset iinto the se-
quence, and a string to insert at that position. The position is a number from 0tonindi-
cating the element of Oafter which the subsequence is to be added. A deletion operation is a
pair of integers (s, e)withs < eand both0 £ s £ nand0 £ e £ n.Each operation defines a
In this chapter, I will present a formal model of the Palimpsest sequence data type. The
presentation will include some simple proofs of consistency and properties of the model that
show that it can be used to meet the requirements for flexible, divergence tolerant collabo-
ration. The definitions in this chapter are meant to make the intuitions discussed in Chapter
3precise, and the proofs are to guarantee that the definitions are consistent and useful.
4.1 The traditional model of changes
The simplest model is the one used by most file-difference algorithms, and is the usual
one in discussions of text editing and undo. It uses the simplest possible operation set to
achieve version-completeness. Each state of a sequence is affected by one of two possible
kinds of operation: insertion of some elements into the sequence or deletion of some subse-
quence of elements. This model cannot directly represent such operations as move and copy.
Move is represented as a pair of operations, a simple insertion (representing a copy), and a
deletion (of the source data). Copy,is simply an insertion; there is no connection between
the source of the copy, and the new text inserted by it. This kind of representation is inher-
ently static, although it is well suited to implementing version-complete systems.
The standard formalism represents a history as a sequence of operations O
1 …O
k .Each op-
eration is either an insertion operation or a deletion operation, applied a sequence of data
items, D
1 ,…D
n .Whether the initial sequence is empty or contains an initial value, does not
affect the formal model. An insertion is a pair (i, seq)
consisting of an offset iinto the se-
quence, and a string to insert at that position. The position is a number from 0tonindi-
cating the element of Oafter which the subsequence is to be added. A deletion operation is a
pair of integers (s, e)withs < eand both0 £ s £ nand0 £ e £ n.Each operation defines a
