= Solution
A suitable <precondition>, including the empty <array> case, is
$$
\boxed{bs(i)\geq1\ (0\leq i<N),\qquad 0\leq n<\prod_{i=0}^{N-1}bs(i).}
$$
A base of one is allowed: its only valid digit is zero. The empty <product> is one, so $N=0$ permits exactly $n=0$. Each <Euclidean division> extracts the next least significant digit.
``
def intToDigs(n: Int, bs: Array[Int]): Array[Int] = {
// Pre: every base is positive, and 0 <= n < product(bs).
val N = bs.length
val xs = new Array[Int](N)
var i = 0
var q = n
while (i < N) {
xs(i) = q % bs(i)
q = q / bs(i)
i += 1
}
xs
}
``
The expensive <precondition> is a caller obligation, rather than a separately computed <product> inside the conversion. Define $P_i=\prod_{j=0}^{i-1}bs(j)$. The <loop invariant> is
$$
0\leq i\leq N,\qquad
n=\sum_{k=0}^{i-1}xs(k)P_k+qP_i,\qquad
0\leq q<\prod_{j=i}^{N-1}bs(j),
$$
together with $0\leq xs(k)<bs(k)$ for each processed digit. The <Euclidean division> identity $q=(q\bmod bs(i))+bs(i)\lfloor q/bs(i)\rfloor$ proves preservation of the reconstruction equality. Positivity of the bases gives the digit bounds and the next bound on the quotient. The <loop variant> is $N-i$. At exit, $0\leq q<1$ forces $q=0$, hence
$$
\boxed{xs\otimes bs=n,\qquad 0\leq xs(i)<bs(i).}
$$
There are exactly $N$ remainder operations and $N$ divisions, hence $2N$ counted operations. The returned <array> occupies $O(N)$ space and the remaining <auxiliary space> is constant. A represented value can never exceed $\prod_i bs(i)-1$, as follows either by the same nested expansion or by telescoping $\sum_i(bs(i)-1)P_i=P_N-1$; thus the stated range is also necessary for positive bases.
Back to article page
