Results 1 to 2 of 2

Math Help - Correctness of the addition algorithm

  1. #1
    Junior Member
    Joined
    Sep 2011
    Posts
    30

    Correctness of the addition algorithm

    Hello, the addition algorithm that is commonly used in the base 10 positional notation seems to make sense:
    -we add the 1s with the 1s
    -we add the 10s with the 10s
    ...
    -when we reach at least 10 units in a position, we increment the following position and leave the remainder in the current position

    yet can someone provide me with a proof that the addition algorithm guarantees that adding, for instance, 12 with 10 will yield the same result as 12 +1+1+1+1+1+1+1+1+1... (10 times)?
    I know that 10 is the same as 1+1+1+1+1+1 (10 times) plus 12 = 1+1+1+1+1.... since the resulting number of 1s is the same. But what guarantees that this happens in the addition algorithm? What does it make to support this?

    Thanks in advance
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,536
    Thanks
    778

    Re: Correctness of the addition algorithm

    This is how I see a way to formalize your question. Long addition operates on strings of decimal digits. On the other hand, we can define our basic addition, which is our starting point, to operate on strings of 1's (unary notation), or, equivalently, on terms of the form S(S(...S(0)...)) (here S stands for "successor"). We can define unary addition and multiplication by recursion as follows.

    0 + y = y
    S(x) + y = S(x + y)

    x * 0 = 0
    x * S(y) = x * y + x

    These definition are supposed to express our intuitive concept of addition and multiplication and act as a starting point.

    We can also define a translation from decimal to unary strings, also by recursion:

    f(0) = 0
    f(1) = S(0)
    f(2) = S(S(0))
    ...
    f(9) = S(S(S(S(S(S(S(S(S(0)))))))))
    f(ds) = S(S(S(S(S(S(S(S(S(S(0)))))))))) * f(d) + f(s) where d is a decimal digit and s is a string of decimal digits.

    Finally, we define long addition on decimal string. Let's denote it by add(s1, s2). Then correctness of long addition (with respect to unary addition) means that

    f(s1) + f(s2) = f(add(s1, s2)) for all decimal strings s1, s2.

    Similar theorems for binary addition were formally proved using proof assistants like PVS, Coq and Isabelle.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Proving NFA Correctness
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: May 3rd 2011, 01:12 PM
  2. Check derivtives for correctness
    Posted in the Calculus Forum
    Replies: 5
    Last Post: January 16th 2011, 12:09 PM
  3. Minkowski addition-Straight Skeleton Algorithm
    Posted in the Math Topics Forum
    Replies: 0
    Last Post: December 1st 2009, 12:51 AM
  4. Correctness
    Posted in the Discrete Math Forum
    Replies: 2
    Last Post: September 27th 2009, 09:15 AM
  5. Correctness of a sample function
    Posted in the Math Topics Forum
    Replies: 1
    Last Post: June 25th 2006, 11:32 AM

Search Tags


/mathhelpforum @mathhelpforum