¿Demostración del algoritmo estándar de la suma?

Question

¿Puede alguien presentar o indicarme una prueba formal de la validez del algoritmo estándar que todos utilizamos para sumar (alinear los números uno sobre otro, sumar el lugar de los unos, llevar los dígitos "sobrantes" al siguiente valor posicional, etc.)?

Esto es lo que resulta de repasar la teoría de conjuntos, la aritmética elemental y la teoría de la prueba al mismo tiempo :)

Answer 1

Notación Para denotar una cadena de dígitos utilizaré $\bar c$ y $\bar c d$ para denotar una cadena de dígitos con una sola cifra $d$ al final. Por ejemplo $\bar c = 84868786$ y $d = 2$ entonces $\bar c d = 848687862$ pero es importante tener en cuenta que se trata de cadenas de dígitos y no números naturales.

Inducción Utilizaremos el siguiente principio de inducción sobre pares de cadenas no vacías de dígitos decimales:

Dado un predicado $P$ definida en cadenas de dígitos no vacías, entonces si demostramos

• para todos los dígitos $d,d'$ , $P(d,d')$
• para todas las cadenas de dígitos $\bar c, \bar c'$ y dígitos $d, d'$ , $P(\bar c, \bar c') \implies P(\bar c d, \bar c' d')$

podemos deducir $P(\bar c, \bar c')$ es válida para todos los pares de cadenas no vacías de dígitos de la misma longitud.

Este principio de inducción se demuestra fácilmente a partir del esquema de inducción normal para los números naturales.

Declaración Queremos demostrar que el algoritmo de la suma funciona por inducción sobre las cadenas de dígitos, también tendremos que preocuparnos por los acarreos. Definamos el algoritmo de suma de dos cadenas (con un acarreo que siempre será 0 o 1) de la misma longitud como una función:

$$\begin{array}{rcl} \text{add}(k,d,d') &=& \text{carry}(k,d,d')\text{adder}(k,d,d') \\ \text{add}(k,\bar c d,\bar c' d') &=& \text{add}(\text{carry}(k,d,d'),\bar c,\bar c')\text{adder}(k,d,d') \end{array}$$

Dejo las definiciones de $\text{carry}$ y $\text{adder}$ al lector.

Para decir que el algoritmo da lo mismo que la suma verdadera, necesitamos definir una interpretación de cadenas de números naturales:

Primero definimos $[\![d]\!] = d$ de los dígitos (el conjunto $\{0,1,2,3,4,5,6,7,8,9\}$ ) a los números naturales. Entonces definimos recursivamente $[\![\bar c d]\!] = 10 \cdot [\![\bar c]\!] + d$ . Por ejemplo $[\![42]\!] = 10\cdot 4 + 2 = 42.$

Así que ahora podemos definir el predicado $$P(\bar s,\bar s') :\!\!\iff \forall k, [\![\text{add}(k,\bar s,\bar s')]\!] = k+[\![\bar s]\!]+[\![\bar s']\!]$$ que afirma que el algoritmo de la suma da el mismo resultado que la suma verdadera para las cadenas $\bar s,\bar s'$ con cualquier carga $k$ .

Prueba Demostramos por inducción $\forall \bar s, \bar s', P(\bar s, \bar s')$ .
caso base : Debemos demostrar que $$\begin{array}{rcl} \forall k \in \{0,1\}, && [\![\text{carry}(k,d,d')\text{adder}(k,d,d')]\!] \\ &=& 10 \cdot \text{carry}(k,d,d') + \text{adder}(k,d,d') \\ &=& k + d + d' \\ &=& k+[\![d]\!]+[\![d']\!] \end{array}$$

esto puede hacerse probando todos los casos posibles ( $200$ de ellos), o un poco menos directamente utilizando la aritmética modular. En cualquier caso $\text{carry}$ y $\text{adder}$ se definen para que esto se cumpla.

paso recursivo : Debemos demostrar que para todo $k \in \{0,1\}$ , $$\begin{array}{rcl} && [\![ \text{add}(\text{carry}(k,d,d'),\bar c,\bar c')\text{adder}(k,d,d') ]\!] \\ && 10 \cdot [\![ \text{add}(\text{carry}(k,d,d'),\bar c,\bar c')]\!] + \text{adder}(k,d,d') \\ &=& 10 \cdot ([\![\bar c]\!]+[\![\bar c']\!]) + k + d + d' \\ &=& k+[\![\bar c d]\!]+[\![\bar c' d']\!] \end{array}$$

Para ello, primero reutilizaremos nuestro caso base para reescribir el problema como $$\begin{array}{rl} && 10 \cdot [\![ \text{add}(\text{carry}(k,d,d'),\bar c,\bar c')]\!] + \text{adder}(k,d,d') \\ &=& 10 \cdot ([\![\bar c]\!]+[\![\bar c']\!]) + 10 \cdot \text{carry}(k,d,d') + \text{adder}(k,d,d') \end{array}$$

y de esto se desprende $$\begin{array}{rl} && [\![ \text{add}(\text{carry}(k,d,d'),\bar c,\bar c')]\!] \\ &=& \text{carry}(k,d,d') + [\![\bar c]\!]+[\![\bar c']\!] \end{array}$$ que es inmediata por nuestra hipótesis de inducción.

De esto concluimos que el algoritmo de adición es legítimo.

Answer 2

Si conoces la aritmética polinómica, la suma de enteros no es más que un caso especial de la suma de polinomios en $\rm\:\Bbb Z[x]/(x\!-\!b) = $ polinomios de coeficiente entero modulo $\rm\:x\!-\!b,\:$ donde $\rm\:b\:$ es el radix. En efecto, mod $\rm\:x\!-\!b\:$ podemos elegir como sistema completo de repeticiones los polinomios cuyos coeficientes se encuentran en el intervalo $\rm[0,b\!-\!1]$ . Entonces la adición es simplemente una adición de polinomios, seguida de la propagación habitual de los transportes para reducir la suma a la forma normal. Esta es una forma constructiva explícita del isomorfismo $\rm\:\Bbb Z \,\cong\, \Bbb Z[x]/(x\!-\!b)\:$ que surge del homomorfismo de evaluación $\rm\:f(x)\to f(b).$

Por ejemplo, el cálculo $\ 298 + 97\, =\, 395\ $ en el radix $\,10\:$ es el siguiente

$\qquad\begin{eqnarray}\rm mod\ x\!-\!10\!:\,\ \,2x^2\!+\!9x\!+\!8\,+\, 9x\!+\!7\!\!\! &\ \equiv\ &\rm 2x^2+18x+15\\ &\equiv\, &\rm 2x^2+18x+(x\!+\!5)\\ &\equiv\, &\rm 2x^2+19x+5\\ &\equiv\, &\rm 2x^2+(x\!+\!9)x+5\\ &\equiv\,&\rm 3x^2+9x+5\\ \end{eqnarray}$

Por encima, la propagación del carry equivale a interpretar $\rm\:10\!+\!n\,\equiv\, x\!+\!10\:$ como regla de reescritura, para reescribir el polinomio a uno en forma normal, es decir, con todos los coeficientes en el intervalo $\,[0,9].$

Nota: $\ $ Para un ejemplo más interesante, véase la siguiente generalización para real números, donde el manejo adecuado de la propagación del acarreo es mucho más complicado: $$ F. Faltin, N. Metropolis, B. Ross, G.-C. Rota, Los números reales como producto de la corona. Avances en Matemáticas. 16 (1975), 278-304.