Miscellaneous thoughts & Answers to previous post's quiz

I haven't been on the computer lately. A tough flu has kept me in the bed mostly. I have been taking care of my own nutrition while stretching my shoulders so they wouldn't get as stiff during the next writing session.

The last few weeks has made me realise I've been trying to treat this blog as something it perhaps should not be. I'm not sure what I should do with this blog. Maybe I continue it as a real log, rather than attempt to "create content" about subjects I like about.

Here's my weight from the last month:

A chart

It shows 4% weight loss during the last month. I plugged in some values into bmi calculator to estimate how soon I'll be in a healthy weight. I got slightly over 30% body fat percentage and at this rate it'll take about 6 months to get into 10%-15%.

Thinking I focus on this for a while. I'm still writing every week but the subjects are probably quite randomized for a good while.

Answers to the last week's quiz

The task to prove the equation requires that we examine the properties of the modulo.

max(divisors(a) ∩ divisors(b)) = max(divisors(b) ∩ divisors(a % b))

We can conclude that...

a % b = 0, max(divisors(a) ∩ divisors(b)) = b
max(divisors(b) ∩ divisors(0)) = b

The equation holds when a % b = 0. If the modulus is zero, then b is a divisor of a, so we can conclude it's the gcd.

The equation also holds when a % b = a. That is, the b does not divide a at all.

a % b = a, max(divisors(a) ∩ divisors(b)) = max(divisors(b) ∩ divisors(a))

We can model the a % b as:

r = a - b*q

Assume everything has a greatest common divisor k:

a = k*a'
b = k*b'
r = k*r'
k*r' = k*(a' - b'*q')
r' = a' - b'*q'

So we can confirm that the greatest common divisor doesn't change when we take a modulus because we are technically subtracting b from a until a is smaller in magnitude than b.

  max(divisors(a) ∩ divisors(b))
= max(divisors(a) ∩ divisors(b) ∩ divisors(a % b))

Next we should be able to prove that we can discard a in this case:

  max(divisors(a) ∩ divisors(b) ∩ divisors(a % b))
= max(divisors(b) ∩ divisors(a % b))

If a%b is less than a, then either b or a%b are limiting the greatest common divisor. Otherwise a%b is exactly as much as a, and we end up exchanging the a, b with each other.

These pieces allow to construct a formal proof, while they're also informal explanations for why the algorithm is correct.

The error on the previous post are the two conflicting statements about divisors:

max(divisors(a)) = a
divisors(0) = all

For both of these to hold, the zero would have to be the largest number in our system. Therefore the first statement must be weaker.

max(divisors(a)) = a when a ≠ 0
divisors(0) = all

Retrieving greatest common divisor between 0, and 0 gives max(all).

  max(divisors(0) ∩ divisors(0))
= max(all ∩ all)
= max(all)

The base case can only provide correct result when a ≠ 0. If we feed gcd(0,0) to our implementation, we get an incorrect result.

I'd have also wanted to show how to actually carry out these proofs in a theorem prover. I guess I'll try things out in coq and read the Coq'Art book. If I get somewhere with this, I'll write a post about it.

Similar posts