Formal proofs

Discussion in 'Mac Programming' started by Cromulent, Oct 27, 2008.

  1. Cromulent macrumors 603

    Cromulent

    Joined:
    Oct 2, 2006
    Location:
    The Land of Hope and Glory
    #1
    Okay so I started reading The Art of Computer Programming and have started doing the exercises but am having a bit of difficulty with formal proofs. I'm not that great with maths but would like to get better so this is my attempt.

    One of the (supposed) easy exercises states:

    Prove that m is always greater than n at the beginning of step E1. except possibly the first time the step occurs.

    The algorithm is as follows:

    E1 [Find the remainder] Divide m by n and let r be the remainder. (We will have 0 <= r < n).
    E2 [Is it 0?] If r = 0, the algorithm terminates; n is the answer.
    E3 [Reduce] Set m <- n, n <- r, and go back to step E1.

    Okay so we do:

    E1 m = 3 and n = 5.
    3 / 5 = 0 r = 3.
    E2 r = 3, continue
    E3 m = 5, n = 3
    E1 5 / 3 = 1 r = 2
    E2 r = 2, continue
    E3 m = 3, n = 2
    E1 3 / 2 = 1 r = 1
    E2 r = 1, continue
    E3 m = 2, n = 1
    E1 2 / 1 = 2 r = 0
    E2 r = 0, terminate

    If n > m then at step E3 m => n meaning that after one iteration n is always <= m.

    How would I write this as a formal proof? Am I doing anything wrong?
     
  2. gnasher729 macrumors P6

    gnasher729

    Joined:
    Nov 25, 2005
  3. Cromulent thread starter macrumors 603

    Cromulent

    Joined:
    Oct 2, 2006
    Location:
    The Land of Hope and Glory
    #3
    Bah sorry I'm an idiot. Previous post fixed.

    Heh, stupid brain farts :).
     
  4. robbieduncan Moderator emeritus

    robbieduncan

    Joined:
    Jul 24, 2002
    Location:
    London
    #4
    I would suggest you use Proof By Induction.

    Looking at this reminds me of studying Computer Science at Uni!
     
  5. lee1210 macrumors 68040

    lee1210

    Joined:
    Jan 10, 2005
    Location:
    Dallas, TX
    #5
    I am not sure what notation is being used, but:
    r must be strictly less than n, as there cannot be a remainder greater than the divisor. This should be some sort of lemma that is already available. Since m is set to n at the end of the algorithm, and n is set to r, based on the prior assertion, at E1 n must be strictly less than m.
    Q.E.D.
    =)
    -Lee
     
  6. robbieduncan Moderator emeritus

    robbieduncan

    Joined:
    Jul 24, 2002
    Location:
    London
    #6
    I think that there must be some more assumptions that are not stated. For example if you start with m=1 and n=1 then m will never be larger than n.
     
  7. gnasher729 macrumors P6

    gnasher729

    Joined:
    Nov 25, 2005
    #7
    If m = n = 1, the algorithm will terminate immediately in Step 2 and never return to Step 1. It is correct to say "m > n whenever the algorithm returns to Step 1" if it never returns to that step.
     
  8. robbieduncan Moderator emeritus

    robbieduncan

    Joined:
    Jul 24, 2002
    Location:
    London
    #8
    Yes, you are right. This might well be a useful base case for one of 2 (or maybe 3) inductive proofs that would prove this for all cases...
     
  9. Berlepsch macrumors 6502

    Berlepsch

    Joined:
    Oct 22, 2007
    #9
    For problems like this, it is often easiest if you sort all possible start conditions into relevant categories and look at them one by one. For your problem, consider

    1) m = n , which implies r = 0
    2) m > n with r > 0
    3) m > n with r = 0
    4) m < n with r > 0
    5) m < n with r = 0 (only possible if m = 0 is allowed).

    Cases 1, 3 and 5 can be dismissed because the algorithm stops in the first iteration. For case 2, lee has already given the answer: r < n by definition, therefore m' > n' in the second and all following iterations.

    That leaves only case 4 to look at. The result is obvious, so I don't have to spell it out. :cool:
     
  10. Cromulent thread starter macrumors 603

    Cromulent

    Joined:
    Oct 2, 2006
    Location:
    The Land of Hope and Glory
    #10
    Cheers guys :).

    Looks like this book will be well worth persevering with. Does anyone have any useful maths website links at all for this kind of stuff? I looked at the wiki link provided earlier but was wondering if there was a slightly more general resource?
     

Share This Page