Invariant and Loop Invariant

Invariant and loop invariant are very closely related concepts in algorithm analysis, but there is a subtle difference:

  • Invariant: A property that is true at a particular point in the algorithm (or data structure) regardless of input. It is a condition that is maintained as the algorithm executes.

  • Loop invariant: A property that is true at the beginning and end of every loop iteration. It must be established as true prior to loop entry, and each iteration maintains it as true.

So a loop invariant is a special case of an invariant - it focuses on a property specifically at loop boundaries.

For example, in binary search:

  • Invariant: The sorted array portion a[lo]…a[hi] always contains the search key x

  • Loop invariant: At the start and end of every loop iteration, the sorted portion a[lo]…a[hi] contains the search key x

The loop invariant is just the general invariant, but specially applied to each loop iteration in the algorithm.

Some key differences:

  • Invariants apply to whole algorithm, loop invariants only to loops
  • Loop invariants are scoped to loop boundaries
  • Loop invariants aid proving correctness of loops

So in summary, a loop invariant is an invariant specific to a loop in an algorithm. Loop invariants are useful for analyzing and proving correctness of iterative algorithms.

Code

Here is a simple code example to illustrate the difference between general invariants and loop invariants:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21

# Find index of value in sorted array 

def binary_search(arr, x):

  lo = 0
  hi = len(arr) - 1

  # Invariant: x is within arr[lo...hi] 
  while lo <= hi:

    mid = (lo + hi) // 2
    
    # Loop invariant: x is within arr[lo...hi]
    if x < arr[mid]:
      hi = mid - 1
    elif x > arr[mid]:
      lo = mid + 1 
    else:
      return mid

  return -1

The general invariant is that the value x is contained within the slice of the array from arr[lo] to arr[hi]. This is true at all points in the algorithm.

The loop invariant is the same property, but specifically applied to the start and end of each loop iteration. Before entering the loop, x is in arr[lo…hi]. After each iteration, the loop invariant is re-established by updating lo or hi.

The loop invariant aids in proving the binary search algorithm correct by focusing on what must be true on each loop iteration.

So in this simple example, the loop invariant is just a special case of the general invariant, focused on the loop boundaries. This is a common pattern in algorithm analysis.