3
$\begingroup$

I'm working through a proof of correctness for merge sort.

I'm given a loop invariant for a for loop, which makes reference to a subarray $A[p..k-1]$. During the initialization step of the correctness proof, my textbook says "Prior to the first iteration of the loop, we have $k=p$, so that the subarray $A[p..k-1]$ is empty".

In other words we're saying $A[p..p-1]$ is empty. Suppose $p=1$, then it's saying $A[1..0]$ is empty. Why is this considered empty? Is it just an axiom that subarray $A[a..b]$ is empty if $a>b$?

$\endgroup$
2
$\begingroup$

It's a convention. One reason for the convention is that the length of an array $A[i..j]$ is $j-i+1$, so if $j=i-1$, we should get an array of length zero. Due to this reason, we sometime consider $A[i..j]$ to be undefined when $j < i-1$; in other cases, the issue does not arise, and $A[i..j]$ is just the empty array whenever $j < i$. In yet other cases, we do not want to allow empty arrays, and then $A[i..i-1]$ is undefined as well.

Since these conventions are not standard (indeed, they are conflicting), if one of them is used, it should be announced beforehand, or when it occurs.

$\endgroup$
1
$\begingroup$

Yes, you may consider this as axiom. Or try to make a definition that still works for a > b case - most probably it will give you an empty array in this case. For example, "all elements with indexes i >= a and i < b".

$\endgroup$
  • $\begingroup$ Does this axiom have a name? Is it formalised somewhere? $\endgroup$ – HumptyDumpty Jul 1 at 15:44
  • $\begingroup$ I would consider it just as all integer numbers from the [a,b] segment as defined in Math $\endgroup$ – Bulat Jul 1 at 15:46
  • $\begingroup$ [i..i-1] is undefined as an interval of real numbers in maths. $\endgroup$ – gnasher729 Jul 3 at 9:42
1
$\begingroup$

A[i..j] is a convention. We could define it any way we like, but we define it in a way that gives useful results.

One property is that if we reduce the right index by 1, then we lose the rightmost element. For example, going from A[5..10] to A[5..9] we lose element 10. So what is A[i..i] and what would you expect going from A[i..i] to A[i..i-1]?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.