December 2012, revised April 2013
The latest release is December 2012. The header file reducible_queue.h is the whole library. The source file reducible_queue.cc is a test program. Both are MIT-licensed.
reduq
provides a C++ template class reduq::reducible_queue<Reducer>
with the following operations. All of them run in worst-case constant time assuming that Reducer
and the memory allocator are well-behaved.
reducible_queue()
: constructs a reducible_queue
bool empty()
: returns true if and only if there are no elements in the queuesize_t size()
: returns the number of elements in the queueconst Reducer::Type& front()
: returns a const
reference to the element in the queue least recently insertedconst Reducer::Type& back()
: returns a const
reference to the element in the queue most recently insertedvoid push(const Reducer::Type& x)
: inserts x
into the queuevoid pop()
: removes from the queue the element least recently insertedReducer::Type reduce()
: returns the “product” by Reducer::reduce
of the elements in the queue from least to most recently insertedThe template parameter Reducer
must have three members.
Type
: the element typeType reduce(const Type& x, const Type& y)
: returns the “product” of x
and y
; must be associativeType id()
: returns a right identity for reduce
reduq
defines the following reducer templates, whose element types are all T
.
reduq::BitwiseAnd<T>
reduq::BitwiseOr<T>
reduq::BitwiseXor<T>
reduq::IntegerMax<T>
reduq::IntegerMin<T>
reduq::Product<T>
reduq::RealMax<T>
reduq::RealMin<T>
reduq::Sum<T>
Although the implementation uses linked lists, I describe the algorithm using two infinite arrays. At a high level, it interleaves continual back-to-front suffix scans with pushes and pops.
## public ##
f = empty():
f = begin >= end
push(x):
A[end] = x
end = end + 1
current_batch = reduce(current_batch, x)
step()
# precondition: not empty()
x = pop():
x = A[begin]
begin = begin + 1
step()
y = reduce():
if empty():
y = id
else if begin >= j:
y = reduce(B[begin], current_batch)
else:
y = reduce(B[begin], previous_batch, current_batch)
## private ##
step():
if j <= begin:
j = end - 1
B[j] = A[j]
{previous_k = current_k}
previous_batch = current_batch
{current_k = end}
current_batch = id
else:
j = j - 1
B[j] = reduce(A[j], B[j + 1])
begin = 0
end = 0
j = -1
A = [...]
B = [...]
{previous_k = 0}
{current_k = 0}
previous_batch = id
current_batch = id
Statements necessary only for the analysis are surrounded by {braces}. It is clear that empty
and push
and pop
are correct and that all operations run in constant time. The following invariant implies the correctness of reduce
.
(0) 0 <= begin <= end
(1) previous_k <= current_k <= end
(2) for all i in {begin, ..., min(previous_k, j) - 1},
B[i] == reduce(A[i ... previous_k - 1])
(3) for all i in { j, ..., current_k - 1},
B[i] == reduce(A[i ... current_k - 1])
(4) previous_batch == reduce(A[previous_k ... current_k - 1])
(5) current_batch == reduce(A[ current_k ... end - 1])
(6) (j - begin) + (end - current_k) < current_k - begin
(7) j - previous_k <= previous_k - begin
(8) min(begin, end - 1) <= j
The intuition for clauses (6-7)
is that there are two intervals, previous_k ... j - 1
and current_k ... end - 1
, that begin
must not reach if reduce()
is to be correct. Clause (7)
ensures that begin
does not reach the first, and clause (6)
ensures that begin
does not reach the second. Accordingly, reduce
is correct.
Now we establish the invariant. empty
and reduce
have no side effects and thus maintain the invariant. push
, just prior to calling step
, ensures clauses (0-5)
; (6')
, a weakening of (6)
; (7)
; (8')
, a weakening of (8)
given (0)
; and a new clause, (9)
.
(6') (j - begin) + (end - 1 - current_k) < current_k - begin
(8') begin - 1 <= j
(9) 0 <= end - 1
In turn, step
ensures (0-8)
by starting the next scan or subtracting one from j
.
pop
, just prior to calling step
, ensures clauses (0-6)
; (7')
, a weakening of (7)
; (8')
; and (9)
.
(7') j - previous_k <= previous_k - (begin - 1)
In turn, step
again ensures (0-8)
.
A classic data structures interview question asks for a queue with an efficient find-min operation. One commonly proposed solution achieves amortized time bounds via two stacks. reduq
achieves worst-case time bounds without resorting to the complexity of purely functional data structures.
© 2012–2013 David Eisenstat