Re: [math-fun] Proof checking and program checking

6 Mar 2006


      ...
Define a predicate on positive integers (in Javaesque style):
boolean isToad(int n) {
  return n==2 || n==frog(4,floor((n-1)/2),1,0)-1);
}
But put a left-parenthesis just before "frog".
...
int frog(int q, int r, int s, int t) {
  if (r<t) {
    return 0;
  } else if (r==t) {
    return 1;
  } else if (q==0) {
    return 0;
  } else {
    return frog(q,r,s+1,s+t) + frog(q-1,r-t,1,0);
  }
}
...
Can you explain why this code works? ...
The explanation is essentially a fairly non-trivial theorem of Legendre.
Clever! I hadn't seen that theorem.

    But I have seen theorem 386 of Hardy&Wright (An Introduction to the
    Theory of Numbers). From that, I derive this similar program.

int crow(int q, int r, int s, int t) {
    if (r < t) {
        return 0;
    } else if (r == t) {
        return 1;
    } else if (q == 0) {
        return 0;
    } else {
        int x = crow(q, r, s+1, s+s+1+t);
        if (t == 0) x *= 2; /* account for the negative thingies :-) */
        return x + crow(q-1, r-t, 0, 0);
    }
}

boolean isLark(int n) {
    return n == (crow(4, n, 0, 0) / 8 - 1);
}

    And I shall torture the dear reader in the same ways.
    1. Which integers are larks?
       (Same as toads, of course.)
    2. Describe what the Crow method does.
    3. Explain why this code works.
       (The cited theorem should help.)

-- 
Don Reble  djr@nk.ca


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.