MHB What does the algorithm calculate?

[mathmari]

Hey!

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? (Wondering)

 

[I like Serena]

Hey mathmari! (Smile)

A proof of correctness works like this:

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

So the algorithm calculates $ (2n)! \operatorname{div} (n! (n+1)!)$. (Thinking)