# What does the algorithm calculate?

We have the following

i <- 0
j <- 0
x <- 1
y <- 1
z <- 1
c <- 1
u <- 1
while i<n do
i <- i+1
j <- i
x <- x*i
z <- x
y <- i+1
y <- x*y
while j<2*i do
j <- j+1
z <- z*j
od
c <- z div (x*y)
od


I want to find the loop invariant for both while-loops.

I applied the algorithm some times to understand what it does:

The inner while loop calculates the following: $$z=z\prod_{m=1}^{2i-1}(i+m)=x\prod_{m=1}^{2i-1}(i+m)$$ or not? Is this also the loop invariant of the inner while loop?

So I got the following results:

First loop:

i=1
j=i=1
x=1
z=x=1
y=i+1=2
y=x*y=2
inner while loop: z=x(i+1)=2
c = z div (x*y) = 2 div 2 = 1


Second loop:

i=2
j=i=2
x=1*2=2
z=x=2
y=i+1=3
y=x*y=2*3=6
inner while loop: z=x(i+1)(i+2)(i+3)=2*3*4*5
c = z div (x*y) = 2*3*4*5/2*6=10


Third loop:

i=3
j=i=3
x=2*3=6
z=x=6
y=i+1=4
y=x*y=24
inner while loop: z=x(i+1)(i+2)(i+3)(i+4)(i+5)=6*4*5*6*7*8
c = z div (x*y) = 6*4*5*6*7*8/6*24=5*7*8=280


Is everything correct? But what exactly calculates the algorithm? What is a general formula of the results?

## 1 Answer

Note that $x=i!$. Now it's easy to see $y=(i+1)!$ and $z=(2i)!$. So $c=\frac{(2i)!}{i!(i+1)!}$, which is the $i$th Catalan number.

P.S. Your formula is wrong. The condition of the inner loop is $j=i+m\le2i$, so $m$ is from $1$ to $i$ instead of $2i-1$ or something.

• Ah I got it now!! So the algorithm computes the $n$th Catalan number, right? Is the loop invariant of the inner loop the $z=(2i)!$ and of the outer loop $c=\frac{(2i)!}{i!(i+1)!}$ ? – Mary Star Jan 18 '17 at 9:31
• @MaryStar Right. More precisely, I would say it computes the first $n$ Catalan number since $c$ is computed inside the loop (which is not necessary if you only need the $n$th). But if you are considering loop invariant, I guess it should be $z=j!$ of the inner loop since $z=(2i)!$ only holds after the termination. For the outer loop, those $x,y,z,c$ equations are all loop invariants and I think $x=i!$ is the most critical one in the sense of induction. – aaaaajack Jan 18 '17 at 11:53