What loop invariant can be used for this loop? (Algorithm to check if a sequence is stack permutable)

Question

I've written a function that gets a permutation and checks if that permutation can be reached using a stack from an input sequence which is <1,2,3,...,n>. (we take elements from left)
For example: if we have an input sequence, then if the function gets these permutations:
<4,3,2,1> - Returns true since we can push (1) push (2) push (3) push (4) and then pop (4) pop pop pop to get this permutation.
<4,3,1,2> - Returns false since this permutation cannot be reached (2 will always be above 1 in the stack after reaching 4,3).

The algorithm looks something like this in pseudocode:
I've referred to the permutation we're checking by P, and the <1,2,3,...,n> sequence by In(input).
The empty stack I'm using will be S.

While (In is not empty)
   i = 0
   Take In leftmost element store it in x (1 then 2 then 3,...)
   if (x == P[i])
      i = i + 1 // i can be printed by push pop so we  keep going
      while(S is not empty)
         x = pop(S)
         if (x == P[i])
            i = i + 1 // x is the next number in the permutation
         else
            push(x) // x isn't the next number so we keep it in stack for later
            break
   else
      push(x)

if (S is not empty AND i = n+1)
   return TRUE
else
   return false

The idea is to keep taking numbers from our input sequence (In) until we reach the next permutation number (P[i]), once we reach it we check if the next one can be found in the stack before checking the next input numbers (they will be sorted such that the biggest will be on top of the stack, so if it's lower value than the top we can't really reach it, and if it's higher value then we will reach it in the input sequence).


Now what I'm trying to do is to prove the correctness of this algorithm, for that I know I need to write some loop invariants for my loops, I've tried to think of my goal, which is to check if a permutation can be reached using a stack, if the stack is not empty at the end, then we got stuck and the permutation can't be reached, just like <4,3,1,2>.
My attempt for loop-variant for the outer loop (while(In not empty)):
At the start if each iteration, the elements P[0...i-1] (As of all the elements of the permutation until the one P[i] we're looking at now), are either reached in the permutation (Pushed and popped - just like 4 in <4,3,1,2> when we're looking at 3, it would have been reached by push push push push pop), OR they're inside the stack.

Now if this worked, I would've been done since at the end if the stack isn't empty, then the permutation cannot be created, but when I looked in the inner loop, I still go into the stack to check, so the elements P[1...i-1] are really reached again sometimes and that ruined my plans, and I've been stuck trying to come up with another loop invariant or fixing this one.


I would appreciate any help and feedback, Thanks in advance.

Answer 1

This question is interesting in the sense that although people might convince themselves that the "obvious" algorithm is correct, it may not be obvious to find a good loop invariant.

The Basic Idea

Your algorithm is, in fact, simulating the possible sequence of actions that produces a given stack-permutable sequence. Given a stack-permutable sequence, there is only one sequence of actions to produce it essentially. If your algorithm takes the only possibly-successful actions upon each input number, it must be correct.

A Clearer Algorithm

Let us augment your pseudocode with a write-only queue Q to make it clear that the algorithm tries to reproduce the given permutation P. Since the queue is never read, it does not change the semantic of the algorithm in the question.

Initialize an empty queue Q and an empty stack S
Let In be input that produces 1, 2, ..., n.
Treat sequence P as a queue 
While In is not empty:
    Move the next number from In (1 then 2 then 3,...) onto S
    While S is not empty and the top of S is the front of P:
        Move the top of S to Q
        Pop P 

if S is empty
   return True    # Q is the same as the original P
else
   return False

The Loop Invariant.

Given P, the algorithm runs a sequence of moving actions of one of two types:

• move a number from In to S
• move a number from S to Q and pop P as well (only when the top of the S is the same as the front of P)

Here is the invariant of the whole algorithm: the algorithm always take the only possible moving action so that in the end Q might be the same as the original (input) P.

Proof: Before any moving action, the algorithm may find S and P in one of the following two states.

• S is not empty and the top of S is the same as the front of P. Let the number at the top of S (and the front of P) be s.

  Suppose the algorithm moves another number i from In to S.
  

  • Since S is a stack, i will be moved into Q before s if both of them will ever be moved to Q. Once i and s are in Q, no later actions can change the order of them in Q, since Q is a queue. So in the end, i will sit earlier than s in Q.
  • On the other hand, i will only be moved into Q at the point of time t later when both the top of the stack is i and the front of P also becomes i. Since P is a queue and the front of P is s now, i must sit later than s now. In other words, i sits later than s in the original P.

  The inconsistent order of i and s in Q and in the original P means this moving action from In to S cannot be successful. Hence, the only action for the algorithm to take so that in the end Q might be the same as the original P possibly is moving the number at S to Q and popping P.

• Either S is empty or the top of S is not the same as the front of P.
  In this case, the only possible action for the algorithm to take is moving a number from In to S.