# Relaxed Data Types as Consistency Conditions +
## 3 Relaxed Data Types  
We here present definitions of several relaxations introduced in [10]. We restate these definitions purely in terms of legal sequences of operation instances, where [PERSON] et al. [10] combined equivalence classes of such sequences to develop a state machine notation. Several authors [6; 12; 13; 14; 15; 16] used these and similar relaxations. First, we consider the Out-of-Order relaxation. The definition of this relaxation does not immediately appear to have anything to do with ordering, but when instantiated on operations in ordered data structures such as _Dequeue_ in queues and _Pop_ in stacks, it causes those operations to return an element up to \(k\) places out of order. One way to think about this is to imagine that by deleting operation instances in the past, we are making the current instance act as if it is in a different place in the permutation of all instances. **Definition 7** (\(k\)-Out-of-Order Relaxed ADT). : _Given any ADT \(T\) and an integer \(k\geq 0\), a \(k\)-Out-of-Order relaxation of \(T\), called \(T^{\prime}\), is defined as follows:_  
1. \(OPS(T^{\prime})=OPS(T)\)__
2. _A sequence_ \(\Pi\) _of operation instances is legal in_ \(T^{\prime}\) _if for every instance op where_ \(\Pi=\pi.op.\rho\)_, there is some sequence_ \(u.v.w,|v|\leq k\)_, which is a minimum-length sequence equivalent in_ \(T\) _to_ \(\pi\)_, and there exists a sequence_ \(x\)_, where_ 1. \(u.w\) _is legal in_ \(T\) _and minimum-length among the set of sequences equivalent to it in_ \(T\)_;_ 2. \(u.w.op\) _is legal in_ \(T\)_; and_ 3. \(u.w.op\equiv x.w\) _and_ \(\pi.op\equiv x.v.w\) _or_ 1. \(u.w.op\equiv u.x\) _and_ \(\pi.op\equiv u.v.x\)_._  
Intuitively, an instance \(op\) is allowed after some prefix \(\pi\) if some contiguous portion of the prefix can be ignored. The relaxation does not want to consider past actions which have since been undone, such as an overwritten write or removed element, so we replace \(\pi\) with a minimum-length sequence equivalent to it (\(u.v.w\)). We then delete up to \(k\) consecutive mutator instances (\(v\)), making \(u.w.op\) legal in the base type. Now, \(u.w.op\) being legal in \(T\) means that \(\pi.op\) is legal in a \(k\)-Out-of-Order relaxation \(T^{\prime}\) of an ADT \(T\), but we need to specify what effect \(op\) had. We do this by saying that the set of sequences legal in \(T^{\prime}\) after \(\pi.op\) is the same set as those legal after reinserting the deleted sequence of instances (\(x.v.w\) or \(u.v.x\), as appropriate). In this and other relaxations, we refer to \(T\), the type from which the relaxation is defined, as the _base type_. Note that [PERSON] et al. [10] defined the \(k\)-Out-of-Order relaxation to allow either deleting (as above) or inserting up to \(k\) operation instances. We only allow deletions, as some operations could have arbitrary behavior if we allowed arbitrary additions. For example, _Dequeue_ on a relaxed queue can return any value \(x\), if we add \(Enqueue(x)\) to the beginning of the history. To avoid such problems, we restrict our attention to Out-of-Order with respect to deleting past instances. The next relaxation we consider is _Lateness_. This name comes because one way to view the relaxed data type is that operations may act as out-of-order, each for any finite relaxation parameter, except that each time an instance does not satisfy the specification of the base type, we increase a lateness counter. That counter can never exceed \(k\), and resets when an instance acts by the specification of the base type. Thus, we can have instances arbitrarily far from the base type's behavior, but are guaranteed that at least one in every \(k\) consecutive instances behaves normally. For example, a relaxed _Dequeue_ may return and remove any element in the queue, as long as one in every \(k\)_Dequeues_ returns the head. **Definition 8** (\(k\)-Lateness Relaxed ADT). : _Given any ADT \(T\) and an integer \(k\geq 1\), a \(k\)-Lateness relaxation of \(T\), \(T^{\prime}\), is defined as follows:_  
1.