The first three subtractions are negative or return the already-seen zero, so addition is used. The fourth subtraction gives a new positive two; the next subtraction is negative. Thus . These are the initial terms of Recamán's sequence.[ref]
OEIS entry A005132. Initial terms, offset zero
Use the already-filled prefix itself for membership tests. The outer loop invariant is and for . The inner loop invariant says that and no processed entry before
Long intermediates avoid overflow in the candidate calculations, while a checked conversion respects the required output type:def recaman(a: Array[Int]): Unit = {
if (a.length == 0) return
a(0) = 0
var i = 1
while (i < a.length) {
val candidate = a(i - 1).toLong - i.toLong
var j = 0
while (candidate > 0L && j < i && a(j).toLong != candidate) {
j += 1
}
val next =
if (candidate > 0L && j == i) candidate
else a(i - 1).toLong + i.toLong
require(next <= Int.MaxValue.toLong, "Sequence value exceeds Int")
a(i) = next.toInt
i += 1
}
}j equals the positive candidate. Its guard either reaches the end of the prefix, finds the candidate, or immediately rejects a nonpositive candidate. Its loop variant is . This establishes exactly the choice required by the recurrence, so the outer loop invariant is preserved. The outer loop variant is .Extra storage is beyond the supplied result array. Membership scans give an upper bound for output entries. Addition, unlike the subtraction branch, is not required to avoid repeats: at indices and the value occurs twice. The code therefore does not try to enforce global distinctness. If an exact value eventually exceeds
Int, the output interface cannot hold it; the check reports that limitation rather than wrapping the recurrence.Regardless of which branch is taken, . Starting from zero and applying induction givesFor the inductive step, add to the bound for the previous value. The subtraction branch gives an even smaller result, and positivity is checked there. This bound need not describe the actual growth sharply; it is sufficient to size a finite membership representation for a requested prefix.
Let denote the entry state. A conventional meaning for the Boolean returned by Initially . In particular, re-adding an existing element returns false and does not increase the size. All operations have the stated empty precondition at the abstract level. The comment that
add is whether the call changes the set:// add(elem):
// S' = S0 union {elem}
// result == !S0.contains(elem)
// contains(elem):
// S' = S0
// result == S0.contains(elem)
// size:
// S' = S0
// result == cardinality(S0)add adds an element does not itself completely specify its Boolean result; the explicit changed/not-changed convention above completes that contract. As with any Int-valued size operation, exact cardinalities are understood to be representable by that result type.Represent the characteristic values of a bounded universe by one Boolean slot per possible member, a Boolean-array form of a bitset:The abstraction function is . The representation invariant is that
class BitMapSet(val MAXVALUE: Int) extends IntSet {
require(MAXVALUE >= 0)
private val bits = Array.fill(MAXVALUE)(false)
private var count = 0
def contains(elem: Int): Boolean =
0 <= elem && elem < MAXVALUE && bits(elem)
def add(elem: Int): Boolean = {
require(0 <= elem && elem < MAXVALUE, "Outside bitmap universe")
if (bits(elem)) false
else {
bits(elem) = true
count += 1
true
}
}
def size: Int = count
}bits.length==MAXVALUE, its entries are Boolean, and count equals the number of true entries. Initialization gives the empty set; changing a false entry to true adds exactly its index and increments the count once. A repeated addition preserves both. All three operations have time complexity after initialization; storage and explicit array initialization are .The constructor requires , and
add requires . contains remains total by returning false outside the representable universe; short-circuit evaluation protects the index. This finite representation cannot implement unrestricted addition of every Int while preserving the abstract contract. Its strengthened add precondition therefore makes it a restricted implementation, not a behaviorally substitutable implementation of the unrestricted trait for arbitrary clients. The sequence client below proves that it stays within the restricted universe.For result entries the largest required index is , so the bound in part (a)(iii) permits universe size . Check that the chosen universe can itself be expressed as an array length:The loop invariant is that the result prefix contains exactly and the abstraction function of
def recamanBitmap(a: Array[Int]): Unit = {
val n = a.length
if (n == 0) return
val capacity = n.toLong * (n.toLong - 1L) / 2L + 1L
require(capacity <= Int.MaxValue.toLong, "Bitmap universe too large")
val seen = new BitMapSet(capacity.toInt)
a(0) = 0
seen.add(0)
var i = 1
while (i < n) {
val candidate = a(i - 1).toLong - i.toLong
val next =
if (candidate > 0L && !seen.contains(candidate.toInt)) candidate
else a(i - 1).toLong + i.toLong
a(i) = next.toInt
seen.add(a(i))
i += 1
}
}seen is their set of values. The universe bound ensures that each positive candidate being queried and each actual next value is less than capacity; values are nonnegative. Thus the conversions and the restricted add precondition are justified, rather than merely hoped to succeed. At a repeated addition, add returning false is harmless: the set of previously seen values is still updated correctly. The loop variant is . At return every result entry agrees with the original recurrence.The original routine uses auxiliary space and at most membership work. A bitmap with universe size uses extra storage and work in the sequence-generation loop because membership and insertion each take constant time. Here the safe universal bound chooses , so extra storage is for growing .
Initialization must be accounted for separately: creating and clearing a Boolean array of length takes work in the usual array-initialization model. Consequently the complete one-shot routine takes , which is with this conservative universe bound. The faster lookup does not make that quadratic setup disappear. If the bitmap is already initialized, or the analysis explicitly charges only the generation phase, the remaining phase is linear. A tighter known bound on values can reduce the universe cost, but no unproved growth bound is needed here.
A fixed array containing the distinct seen integers needs capacity at most , because at most one new distinct value is introduced per result entry. Its auxiliary space is therefore , rather than the bitmap's universe storage. A size field identifies the occupied prefix; insertion first checks membership, and appends only when absent.
An unsorted occupied prefix needs linear membership scans, giving total work by the same summation as in the original version. Keeping it sorted permits binary search membership in , but inserting a new value can shift entries, so the overall worst-case upper bound remains quadratic. Unlike a bitmap, the space cost depends on the number of stored values rather than their largest possible numerical magnitude. Compared with part (a)(ii), this extra set array also duplicates information already present in the output prefix; its principal benefit is a separate set interface, not an automatic asymptotic speedup.
Articles by others on the same topic
There are currently no matching articles.