Corrección de programas de matemáticas discretas

Question

Dado un número entero distinto de cero a y $b\Bbb N$ queremos calcular $a^b$ . Consideremos el siguiente algoritmo recursivo $\operatorname{POW}(a,b)$ .

Si $b=0$ devolución $1$

En caso contrario, si b es impar, devuelve $a\cdot(\operatorname{POW}(a,\lfloor b/2\rfloor))^2$ .

En caso contrario (es decir, si $b>0$ y $b$ es par), devuelve $(\operatorname{POW}(a,\lfloor b/2\rfloor))^2$ .

Y queremos demostrar que POW está en lo cierto. Es decir, demostrar que POW se detiene y devuelve $a^b$ .

Para la prueba: Sea $p(b)$ sea el predicado $\operatorname{POW}(a,b)$ se detiene y regresa $a^b$ . Es fácil demostrar el caso base que es: cuando $b=0$ observamos que $\operatorname{POW}(a,0)$ se detiene y regresa $1$ que es igual a $a^0$ . Pero no estoy seguro de cómo continuar el paso inductivo.

¿Puede alguien darme alguna pista?

Answer 1

Dado un número entero distinto de cero $a\in \Bbb N$ y $b∈\Bbb N_0$ queremos calcular $a^b$ . Consideremos el siguiente algoritmo recursivo $\operatorname{POW}(a,b)$ .

function POW(a,b):
    If b=0:
        return 1
    else if b is odd:
        return a*POW(a,[b/2])^2
    else (b is even):
        return POW(a,[b/2])^2

Prueba por inducción:

$\text{POW}(a,0)=1=a^0$ Así que $\text{POW}(a,b)=a^b$ si $b=0$

Supongamos que ya hemos demostrado esto para $b-1$ . Si $b$ es impar, entonces $b=2n+1$ . Entonces volvemos $$\text{POW}(a)=a\cdot\text{POW}(a,[b/2])^2=a\cdot\text{POW}(a,n)^2=a\cdot (a^n)^2=a^{2n+1}=a^b$$ La ecuación $\text{POW}(a,n)=a^n$ se mantiene porque $n\le b-1$ . Si b es par, entonces $b=2n$ . Entonces volvemos $$\text{POW}(a)=a\cdot\text{POW}(a,[b/2])^2=\text{POW}(a,n)^2=(a^n)^2=a^{2n}=a^b$$ De nuevo la ecuación $\text{POW}(a,n)=a^n$ se mantiene porque $n\le b-1$ .

---

A versión no recursiva del algoritmo es la siguiente:

function POW(a,b):
    r:=1
    m:=a
    e:=b
    # r*m^e = a^b
    while e>=0:
        if e=0:
            # r*m^e = a^b
            return r
        else if e is odd:
            r:=r*m
            e:=e-1
            # r*m^e = a^b
        else if m is even:
            m:=m^2
            e:=e/2
            # r*m^e = a^b

# es un signo de comentario aquí. r*m^e es el invariante de bucle . Queda a^b después de cada paso (¡compruébelo!). Así, si e=0 y la función devuelve r , r es a^b .