Loop invariant(discrete math's)

[vvvidenov]

Homework Statement

show that {m^5 $$\leq$$n^4} is a loop invariant for the loop
while 1 $$\leq$$ m do

m:= 3m
n: = 4n

Homework Equations

similar solved example:
while 1$$\leq$$ m do
m:=2m
n: =3n

a) n^2$$\geq$$ m^3 is given [so 8n^2$$\geq$$ 8m^3 by multiplying both sides by 8; and 9 n^2 > 8 n^2 because n^2>0]
Hence ("new-n")^2=(3n)^2=9n^2>8n^2$$\geq$$8m^3=(2m)^3=("new-m").
So ("new-n")^2$$\geq$$ ("new-m")

b)2m^6 is given [so 81(2m^6)< 81(n^4) by multiplying by 81, and 64(2m^6) < 81(2m^6)]
Hence 2("new-m")^6=2(2m)^6=2^6*2*m^6<81(2m^6)<81(n^4)=(3n)^4=(new-n")

The Attempt at a Solution

m^5$$\leq$$n^4

81(m^5) < 81(n^4), and 64(m^5)< 81(m^5)

("new-m")^5=(3m)^5 < 81 (n^4)= (4n)^4

("new-m") $$\leq$$ ("new-n")

please help if I did something wrong in this attempt to solve the problem. It is confusing for me even I have the solved one above.

 

[Mark44]

No one else has replied, so I'll give it a shot. I understand the loop invariance concept as it pertains to computer science, and I understand loops such as the while loop in your example. However, I can't make much sense out of your work.

Each iteration of the loop, m gets reset to 3 times its previous value, and n gets reset to 4 times its previous value. What I don't see are the initial values of m and n. Assuming for the moment that m and n are intialized to 1, here are the values of m and n:
m 1 3 9 27 81 243 ...
n 1 4 16 64 256 1024...

In general, at any step k, m's value is 3^k, and n's value is 4^k.

Looking at your loop invariant, you need to show that m^5 <= n^4.

Let's look at the ratio m^5 / n^ 4. If you can show that this ratio is <= 1, you'll be done. I'll be working with logs, so I will show that the log of the ratio is <= 0.

m^5/n^4 = (3^k)^5 / (4^k)^4 = (3^(5k))/(4^(4k))

So ln [m^5/n^4] = ln [(3^(5k))/(4^(4k))]
= ln(3^(5k)) - ln(4^(4k))
= 5k ln(3) - 4k ln(4)
= k [ln(3^5) - ln(4^4)]
The quantity in brackets is ln(243) - ln(256), which is negative.
If k = 0, k [ln(3^5) - ln(4^4)] = 0

Therefore
ln [m^5 / n^ 4] <= 0
or m^5 / n^ 4 <= 1
or m^5 <= n^4, as required.

 

[vvvidenov]

Mark, thank you very much for showing me this way. I will work on this problem again and I will be glad if you review it for me again. It is complicated problem. I really want to find how to solve it. I am not surprise that no one else try it.

81 and 64 I have from solving (3m)^5 and (4n)^4 That is how I have to use one of the numbers and multiply both sides, but why I really don't understand.

Here is more clear solution which still confus me how it 's been done.

Look part a) n^2>= m^3
n^2>= 1
multiplay by 8
8n^2>=8m^3=(2m)^3
8n^2>=(2m)^3

9n^2>8n^2
so 9n^2> (2m)^3

(3n)^2>(2n)^2
(3n)^2>=(2m)^3
which means n^2>= m^3 (follow the top in bold.

 

[vvvidenov]

for part b) from above: 2m^6< n^4

2m^6 < n^4

multiply both sides by 81
81(2m^6) < 81n^4
162m^6 < (3n)^4

128m^6 < 162m^6

2*64=128m^6<81n^4

2(2m)^6 < (3n)^4

2^6=64 and 3^4=81 this is how they find 64 and 81 and start with them but nothing is clear.

My problem is combined from these two solved problems somehow.
Actually, it is close to the problem a) I think plus the (=) sign.

 

[Mark44]

Mark, thank you very much for showing me this way. I will work on this problem again and I will be glad if you review it for me again. It is complicated problem. I really want to find how to solve it. I am not surprise that no one else try it.

81 and 64 I have from solving (3m)^5 and (4n)^4 That is how I have to use one of the numbers and multiply both sides, but why I really don't understand.

I don't understand where you get 81 and 64. I thought it might be from 3^5 and 4^4, but those values are 243 and 256, respectively. And when you say you are "solving" (3m)^5 and (4n)^4, you have to have an equation or inequality to solve.

Here is more clear solution which still confus me how it 's been done.

Look part a) n^2>= m^3
n^2>= 1
multiplay by 8
8n^2>=8m^3=(2m)^3
8n^2>=(2m)^3

9n^2>8n^2
so 9n^2> (2m)^3

(3n)^2>(2n)^2
(3n)^2>=(2m)^3
which means n^2>= m^3 (follow the top in bold.

OK, let's look at this problem, using the same kind of analysis as I did before.
You have m >= 1, so let's start with m = 1, and assume that n = 1 to start with.
You want to show that n^2 >= m^3 is invariant.

At each iteration of the loop m is reset to 2m, and n is reset to 3n, which gives us these numbers at each loop iteration k, where the integer k >= 0:

m: 1 2 4 8 16 32 ... (after k iterations, m becomes 2^k)
n: 1 3 9 27 81 243 ... (after k iterations, n becomes 3^k)

To show that n^2 >= m^3 is equivalent to showing that the ratio (n^2)/(m^3) >= 1, or equivalently, that the log of this ratio is >= 0.

ln [(n^2)/(m^3)] = ln((3^k)^2) - ln((2^k)^3)
= ln(3^(2k)) - ln(2^(3k))
= 2k ln(3) - 3k ln(2)
= k ln(3^2) - k ln(2^3)
= k[ln 9 - ln 8]

When k = 0, the expression above is 0.
For any other value of k, the expression above is positive, so ln(3^(2k)) - ln(2^(3k)) >= 0.
Working backward, ln [(3^(2k)) / (2^(3k)) ] >= 0,
so [(3^(2k)) / (2^(3k)) ] >= 1,
so (3^k)^2 >= (2^k)^3,
and finally, n^2 >= m^3, which was to be shown.

If you'll notice, I did this problem almost exactly the same way I did the other one. I didn't grab some number and multiply both sides of something to get this result.
Mark

 

[vvvidenov]

Mark, I agree with you. I read in the book a lot.