CLRS array merge-sort executions and resource model

CLRS.Memory. For every type $\alpha$ in universe $u$ and natural number $N$, this abbreviation is the type of all functions from the finite index set $\{i\in\mathbb N:i<N\}$ to $\alpha$. It imposes no condition on the values. When $N=0$, the domain is empty; when $N>0$ and $\alpha$ has no elements, there is no such function.

CLRS.Buffer. For every type $\alpha$ in universe $u$ and natural number $n$, this abbreviation is the type of functions on $\{i\in\mathbb N:i<n\}$ with values either absent or present with a value of $\alpha$. Each cell may independently be absent or present. For $n=0$ there are no cells, and no requirement that $\alpha$ contain an element is imposed.

CLRS.write. Given any type $\alpha$ in universe $u$, natural $N$, function $A:\{0,\ldots,N-1\}\to\alpha$, natural index $i$ together with a proof of $i<N$, and value $x\in\alpha$, this defines the function taking index $j<N$ to $x$ if $j=i$, and to $A[j]$ otherwise. The proof of the bound does not affect this formula. There can be no such index argument when $N=0$. This declaration assigns no resource record or numerical cost.

CLRS.emptyBuffer. For every type $\alpha$ in universe $u$ and natural number $n$, this defines a function on the indices smaller than $n$ that returns an absent value at every index. In particular it defines the empty function for $n=0$, and it is defined even if $\alpha$ has no elements.

CLRS.ValidSlice. For arbitrary natural numbers $N,p,r$, this proposition is exactly the conjunction $p\le r$ and $r\le N$. It admits the empty interval $p=r$, including $p=r=N$, and for $N=0$ holds exactly when $p=r=0$.

CLRS.split. For any natural numbers $p,r$, this defines $p+\lfloor((r\mathbin{\dot-}p)+1)/2\rfloor$, where $r\mathbin{\dot-}p=\max(r-p,0)$ is truncated natural-number subtraction and division is natural-number division. No assumption $p\le r$ is required. For $p\le r$ it is $p+\lceil(r-p)/2\rceil$; for $r\le p$ it is $p$. Consequently it equals $r$ on a slice of length one and equals $p=r$ on a slice of length zero.

CLRS.sliceList. For any type $\alpha$ in universe $u$, natural numbers $N,p,r$, and function $A:\{0,\ldots,N-1\}\to\alpha$, this defines the list consisting of $A[i]$ for exactly those natural indices with $i<N$ and $p\le i<r$, in increasing index order. The definition requires no validity of $p,r$. Thus $r>N$ includes no indices beyond the array, and the list is empty when $N=0$, when $r\le p$, or when $N\le p$.

CLRS.SortedSlice. For any type $\alpha$ in universe $u$ equipped with a binary relation denoted $\le$ (without an assumption that it is reflexive, transitive, or an order), any natural numbers $N,p,r$, and array $A:\{0,\ldots,N-1\}\to\alpha$, this proposition says that for all $i,j<N$, the three hypotheses $p\le i$, $i\le j$, and $j<r$ imply $A[i]\le A[j]$. No validity hypothesis on $p,r$ is imposed; only actual array indices are quantified. It is vacuous if there is no index in the slice, but for any included index it also requires $A[i]\le A[i]$, because $i=j$ is permitted.

CLRS.PermSlice. For any type $\alpha$ in universe $u$, naturals $N,p,r$, and arrays $A,B:\{0,\ldots,N-1\}\to\alpha$, this proposition says that the list of $A[i]$ at indices $i<N$ with $p\le i<r$, in increasing index order, is a permutation of the analogous list from $B$. It preserves values with multiplicity and does not require the two lists to have equal order. Bounds need not be valid: only in-range indices are used, and if no such index exists both lists are empty and the proposition holds.

CLRS.OutsideEq. For any type $\alpha$ in universe $u$, naturals $N,p,r$, and arrays $A,B:\{0,\ldots,N-1\}\to\alpha$, this proposition requires $A[i]=B[i]$ for every array index $i<N$ satisfying $i<p$ or $r\le i$. No validity of the interval is assumed. For $r\le p$ the requirement covers every index; for $N=0$ it is vacuous; it imposes no equality condition on indices satisfying $p\le i<r$.

CLRS.Usage. This record consists of three independent natural-number fields named time, heap, and stack. Every triple $(t,h,s)\in\mathbb N^3$ is an allowed record, including $(0,0,0)$; the structure itself asserts no relation among the fields and no relation to an execution. Equality of records is decidable, and a printable representation is derived.

CLRS.CopyLoop. For any type $\alpha$ in universe $u$, naturals $N,n$, array $A:\{0,\ldots,N-1\}\to\alpha$, and natural start index $s$, this inductively defines a relation among a natural current index $i$, an initial and final function $B,B'$ on $\{0,\ldots,n-1\}$ with absent-or-present $\alpha$ values, and a natural cost $t$. Its stopping rule, for every $i,B$ with $n\le i$, relates $i,B$ to the same $B$ with cost $2$. Its step rule, for arbitrary $i,t,B,B'$ with $i<n$ and $s+i<N$, relates $i,B$ to $B'$ with cost $6+t$ whenever the relation holds from index $i+1$ and the buffer obtained by replacing cell $i$ by the present value $A[s+i]$, ending at $B'$ with cost $t$. These are the only rules and derivations must be finite. There is no order assumption on $\alpha$ and no initial requirement that buffer cells be absent. An exhausted index may exceed $n$ and then does not require any array bound; if $n=0$ every current index has the stopping rule, whereas a needed out-of-range read provides no step rule.

CLRS.MergeMain. For any type $\alpha$ in universe $u$ with a linear order, natural lengths $N,a,b$, and fixed absent-or-present-valued buffer functions $L$ of length $a$ and $R$ of length $b$, this is a relation between an initial array $A$ and natural indices $(i,j,k)$, a final array $A'$ and natural indices $(i',j',k')$, and a natural cost. The only rules are finite applications of the following: if $a\le i$, finish with the same array and indices at cost $2$; if $i<a$ and $b\le j$, finish unchanged at cost $4$; otherwise require $i<a$, $j<b$, $k<N$, $L[i]$ present with value $x$, and $R[j]$ present with value $y$, for arbitrary $x,y\in\alpha$. If $x\le y$, replace array cell $k$ by $x$ and continue from $(i+1,j,k+1)$; if $\neg(x\le y)$, replace that cell by $y$ and continue from $(i,j+1,k+1)$. In either step, a continuation ending at any $A',i',j',k'$ with cost $t$ gives the same final outputs with cost $12+t$. Other cells and the fixed buffers are unchanged by each update. Equal values select the left branch. A stopping rule does not check the destination bound or require present buffer entries; a required absent entry or out-of-range destination supplies no step rule. No relationship of the indices to slice bounds and no sortedness assumption is included.

CLRS.RemainderLoop. For any type $\alpha$ in universe $u$, natural lengths $N,n$, and fixed buffer function $B$ of length $n$ with absent-or-present $\alpha$ values, this relation takes an initial array $A$, natural indices $i,k$, a final array $A'$, natural final indices $i',k'$, and a natural cost. For every $A,i,k$ with $n\le i$ it finishes at exactly $A,i,k$ with cost $2$. For arbitrary $A,A',i,k,i',k',t,x$, if $i<n$, $k<N$, and $B[i]$ is present with value $x$, and there is a continuation from the array formed by replacing cell $k$ by $x$ and indices $i+1,k+1$ to $A',i',k'$ with cost $t$, then it runs from $A,i,k$ to those same final outputs with cost $6+t$. These are the only rules, used finitely. No ordering assumption or initial slice invariant is required. The stopping case permits $i>n$ and arbitrary $k$, including when $n=0$; needed absent entries or invalid destinations have no step rule.

CLRS.mergeUsage. For any seven natural numbers $a,b,c_L,c_R,m,d_L,d_R$, this defines the resource triple $(8+a+b+c_L+c_R+m+d_L+d_R,\ a+b,\ 1)$. There are no assumptions that the numbers describe valid loops, that either length is positive, or that any of the supplied costs are positive. In particular the stack field is always $1$ and the heap field is zero when both lengths are zero.

CLRS.MergeExec. For an arbitrary type $\alpha$ in any universe with a specified linear order, an array of natural length $N$ means a function from $\{0,\ldots,N-1\}$ to $\alpha$. A resource record $u=(u_t,u_h,u_s)$ consists of three natural numbers. The relation is given for every natural $N$ and every pair of arrays of that length. Here a finite merge execution on bounds $p,q,r$ means the following inductively generated process, which requires $p\le q\le r\le N$. Put $a=q-p$ and $b=r-q$. Starting from two functions of lengths $a,b$ whose values are all absent, copy $A[p+i]$ into left cell $i$ and $A[q+j]$ into right cell $j$, respectively, beginning at zero and increasing the copy index by one; each copied cell contributes $6$ to its copy cost and the terminating test contributes $2$, including for an empty buffer. Start merging with array $A$ and indices $(i,j,k)=(0,0,p)$. If $i\ge a$, stop this main loop with cost $2$; otherwise, if $j\ge b$, stop with cost $4$. Otherwise both buffer entries must be present and $k<N$: write the left value when it is at most the right value, and otherwise write the right value; increase the selected buffer index and $k$ by one and add $12$ to the remaining main-loop cost. Next copy all remaining left entries, then all remaining right entries, using the indices produced by these preceding stages; each remainder step requires a present entry and an in-range destination, increases its buffer index and destination by one, and contributes $6$, with a final cost $2$ per remainder loop. Each write changes only its indicated array cell. If the five stage costs are $c_L,c_R,m,d_L,d_R$, the final record is $(8+a+b+c_L+c_R+m+d_L+d_R,\ a+b,\ 1)$. All these derivations are finite; sortedness is not part of this execution relation. More explicitly, for arbitrary initial and three intermediate/final arrays $A,A_1,A_2,A_3$, buffer functions $L,R$, natural bounds, all intermediate/final loop indices, and all five natural stage costs, its sole constructor takes precisely the bounds and five loop derivations described above: both copies read the original $A$; the main loop goes from $A,0,0,p$ to $A_1,i,j,k$; the left remainder goes from $A_1,i,k$ to $A_2,i_2,k_2$; and the right remainder goes from $A_2,j,k_2$ to $A_3,j_3,k_3$. Its conclusion has output $A_3$ and the displayed record. There is no separate test on the last loop indices and no uniqueness or existence assertion. The buffers are represented solely by functions; the relation has no block-identity or allocation/deallocation-state arguments. Either adjacent slice may be empty, including the entirely empty slice $p=q=r$, for which the rules give the unchanged array and record $(18,0,1)$.

CLRS.baseUsage. This defines the resource record to have time $5$, heap $0$, and stack $1$. It has no arguments and imposes no execution premise.

CLRS.sortUsage. For any three resource records $v,w,z$, each an arbitrary triple of natural numbers, this defines the new time to be $8+v_t+w_t+z_t$, the new heap to be $\max(v_h,\max(w_h,z_h))$, and the new stack to be $1+\max(v_s,\max(w_s,z_s))$. No execution, positivity, or relationship between those input records is required.

CLRS.MergeSortExec. For an arbitrary type $\alpha$ in any universe with a specified linear order, an array of natural length $N$ means a function from $\{0,\ldots,N-1\}$ to $\alpha$. A resource record $u=(u_t,u_h,u_s)$ consists of three natural numbers. The relation is given for every natural $N$, natural bounds $p,r$, initial and final arrays of length $N$, and resource record. Here a finite merge execution on bounds $p,q,r$ means the following inductively generated process, which requires $p\le q\le r\le N$. Put $a=q-p$ and $b=r-q$. Starting from two functions of lengths $a,b$ whose values are all absent, copy $A[p+i]$ into left cell $i$ and $A[q+j]$ into right cell $j$, respectively, beginning at zero and increasing the copy index by one; each copied cell contributes $6$ to its copy cost and the terminating test contributes $2$, including for an empty buffer. Start merging with array $A$ and indices $(i,j,k)=(0,0,p)$. If $i\ge a$, stop this main loop with cost $2$; otherwise, if $j\ge b$, stop with cost $4$. Otherwise both buffer entries must be present and $k<N$: write the left value when it is at most the right value, and otherwise write the right value; increase the selected buffer index and $k$ by one and add $12$ to the remaining main-loop cost. Next copy all remaining left entries, then all remaining right entries, using the indices produced by these preceding stages; each remainder step requires a present entry and an in-range destination, increases its buffer index and destination by one, and contributes $6$, with a final cost $2$ per remainder loop. Each write changes only its indicated array cell. If the five stage costs are $c_L,c_R,m,d_L,d_R$, the final record is $(8+a+b+c_L+c_R+m+d_L+d_R,\ a+b,\ 1)$. All these derivations are finite; sortedness is not part of this execution relation. A finite sort execution on $[p,r)$ is defined recursively as follows. It requires $p\le r\le N$. For $r-p\le1$ it returns the same array with record $(5,0,1)$. For $r-p>1$, set $q=p+\lfloor(r-p+1)/2\rfloor$, sort $[p,q)$ first, sort $[q,r)$ in the resulting array second, and perform the just-defined merge on the resulting array third. If these three executions have records $v,w,z$, its record is $(8+v_t+w_t+z_t,\ \max(v_h,w_h,z_h),\ 1+\max(v_s,w_s,z_s))$ and its output is the merge's output. No other sort executions are admitted. In the recursive rule the first sort changes $A$ to some $A_1$, the second changes $A_1$ to some $A_2$, and the merge changes $A_2$ to some $A_3$; these arrays and the three resource records are otherwise arbitrary subject to the indicated premises. The empty and singleton cases include $N=0,p=r=0$, and always have identical initial and final arrays. Invalid bounds admit no constructor. This relation asserts neither that an execution exists for given inputs nor that its output or resource record is unique.