Haskell Hero

Haskell Hero es un manual interactivo del lenguaje Haskell para principiantes.

Prueba de inducción

<= Funciones con booleanos lección anterior lección siguiente Entrada y salida I =>

¿Por qué la prueba de inducción?

¿De qué trata esta lección?

A primera vista esta lección puede parecer muy larga. Para que se comprenda mejor, en los primeros párrafos trato de explicar porque necesitamos la inducción. Empezando con un método ingenuo hasta la inducción en el tercer método. El que no se interesa por esta parte de motivación, puede omitirla y empezar leyendo el párrafo Empezamos.

Asignación

Probad que la función fact

fact   ::  Int -> Integer
fact 0  =  1
fact n  =  n * fact (n - 1)

calcula el factorial de números no negativos, es decir, que la expresión fact n se evalua a n!.

El primer método

Demostramos que nuestra definición es correcta mostrando que la función calcula lo que debe para todos parámetros. El método ingenuo podría ser el siguiente:

Queremos demostrar que fact 0 ~>* 0!
fact 0 se evalúa según la primera ecuación a 1, lo que es 0!. La función fact está entonces correctamente definida para n = 0.
Queremos demostrar que fact 1 ~>* 1!
fact 1 se evalúa de manera siguiente:
```
fact 1 ~> 1 * fact 0 ~> 1 * 1 ~> 1
```
lo que es 1! La función fact está entonces correctamente definida para n = 1.
Queremos demostrar que fact 2 ~>* 2!
fact 2 se evalúa de manera siguiente:
```
fact 2 ~> 2 * fact 1 ~> 2 * 1 * fact 0 ~> 2 * 1 * 1 ~>* 2
```
lo que es 2! La función fact está entonces correctamente definida para n = 2.
Queremos demostrar que fact 3 ~>* 3!
fact 3 se evalúa de manera siguiente:
```
   fact 3
~> 3 * fact 2
~> 3 * 2 * fact 1
~> 3 * 2 * 1 * fact 0
~> 3 * 2 * 1 * 1
~>* 6
```
lo que es 3! La función fact está entonces correctamente definida para n = 3.
Queremos demostrar que fact 4 ~>* 4!
fact 4 se evalúa de manera siguiente:
```
   fact 4
~> 4 * fact 3
~> 4 * 3 * fact 2
~> 4 * 3 * 2 * fact 1
~> 4 * 3 * 2 * 1 * fact 0
~> 4 * 3 * 2 * 1 * 1
~>* 24
```
lo que es 4! La función fact está entonces correctamente definida para n = 4.
Queremos demostrar que fact 5 ~>* 5!
...
...

De esta manera podríamos seguir indefinidamente y siempre habría alguien que encontrara un número para que no habíamos demostrado que la función es correcta.

El segundo método

Tenemos que demostrar que fact n se evalúa a n!, esto es lo mismo. Sin embargo, lo vamos a hacer de otra manera.

Demostramos que fact 0 ~>* 0!
fact 0 se evalúa según la primera ecuación a 1, lo que es 0!. La función fact está entonces correctamente definida para n = 0.
Demostramos que fact 1 ~>* 1!
fact 1 se evalúa de manera siguiente:
```
fact 1 ~> 1 * fact 0
```
Ya que sabemos que fact 0 se evalúa a 0!, podemos decir que fact 1 ~> 1 * 0!, lo que es 1! La función fact está entonces correctamente definida para n = 1.
Demostramos que fact 2 ~>* 2!
fact 2 se evalúa de manera siguiente:
```
fact 2 ~> 2 * fact 1
```
Ya que sabemos que fact 1 se evalúa a 1!, podemos decir que fact 2 ~> 2 * 1!, lo que es 2! La función fact está entonces correctamente definida para n = 2.
Demostramos que fact 3 ~>* 3!
fact 3 se evalúa de manera siguiente:
```
fact 3 ~> 3 * fact 2
```
Ya que sabemos que fact 2 se evalúa a 2!, podemos decir que fact 3 ~> 3 * 2!, lo que es 3! La función fact está entonces correctamente definida para n = 3.
Demostramos que fact 4 ~>* 4!
fact 4 se evalúa de manera siguiente:
```
fact 4 ~> 4 * fact 3
```
Ya que sabemos que fact 3 se evalúa a 3!, podemos decir que fact 4 ~> 4 * 3!, lo que es 4! La función fact está entonces correctamente definida para n = 4.
Demostramos que fact 5 ~>* 5!
...
...

Como podemos ver, la longitud de la prueba ya no se aumenta con el parámetro creciente pero de todos modos tendríamos que escribir esta prueba para todos números naturales incluso cero.

El tercer método

En el segundo método hemos demostrado:

la función fact n está correctamente definida para n = 0
la función fact n está correctamente definida para n = 1 en el supuesto de que esté correctamente definida para n = 0
la función fact n está correctamente definida para n = 2 en el supuesto de que esté correctamente definida para n = 1
la función fact n está correctamente definida para n = 3 en el supuesto de que esté correctamente definida para n = 2
la función fact n está correctamente definida para n = 4 en el supuesto de que esté correctamente definida para n = 3
...

Ya que el hecho de que la función fact n es correcta, demostramos por medio de la proposición que la función está correcta para el predecesor, podemos generalizar la prueba anterior para todos números naturales:

Demostramos que fact 0 se evalúa a 0!.
Demostramos que fact (k + 1) se evalúa a (k + 1)! en el supuesto de que fact k! se evalue a k!.

Después, si alguien llega y dice:

"¡Demuéstrame que fact 0 calcula 0! !"

Nosotros podemos decir:

"Mira, fact 0 ~> 1, lo que es 0! ."

Hemos contestado a su pregunta, entonces él tiene que decir:

"Vale, te creo."

Sin embargo, sigue preguntando:

¿Cómo sabes que fact 1 calcula 1! ?
- Porque fact 1 ~> 1 * fact 0 y fact 0 ~>* 0! . Entonces fact 1 ~>* 1 * 0! , lo que es 1! .
Vale, pero ¿cómo sabes que fact 0 calcula 0! ?
- Te lo puedo demostrar: fact 0 ~> 1, lo que es 0! .
Vale, te creo.

Y sigue preguntando:

¿Cómo sabes que fact 2 calcula 2! ?
- Porque fact 2 ~> 2 * fact 1 y fact 1 ~>* 1! . Entonces fact 2 ~>* 2 * 1! , lo que es 2! .
Vale, pero ¿cómo sabes que fact 1 calcula 1! ?
- Porque fact 1 ~> 1 * fact 0 y fact 0 ~>* 0! . Entonces fact 1 ~>* 1 * 0! , lo que es 1! .
Vale, pero ¿cómo sabes que fact 0 calcula 0! ?
- Te lo puedo demostrar: fact 0 ~> 1, lo que es 0! .
Vale, te creo.

Y sigue preguntando:

¿Cómo sabes que fact 3 calcula 3! ?
- Porque fact 3 ~> 3 * fact 2 y fact 2 ~>* 2! . Entonces fact 3 ~>* 3 * 2! , lo que es 3! .
Vale, pero ¿cómo sabes que fact 2 calcula 2! ?
- Porque fact 2 ~> 2 * fact 1 y fact 1 ~>* 1! . Entonces fact 2 ~>* 2 * 1! , lo que es 2! .
Vale, pero ¿cómo sabes que fact 1 calcula 1! ?
- Porque fact 1 ~> 1 * fact 0 y fact 0 ~>* 0! . Entonces fact 1 ~>* 1 * 0! , lo que es 1! .
Vale, pero ¿cómo sabes que fact 0 calcula 0! ?
- Te lo puedo demostrar: fact 0 ~> 1, lo que es 0! .
Vale, te creo.

...
Y sigue preguntando:
...

¿Cómo sabes que fact 100 calcula 100! ?
- Porque fact 100 ~> 100 * fact 99 y fact 99 ~>* 99! . Entonces fact 100 ~>* 100 * 99! , lo que es 100! .
Vale, pero ¿cómo sabes que fact 99 calcula 99! ?
- Porque fact 99 ~> 99 * fact 98 y fact 98 ~>* 98! . Entonces fact 99 ~>* 99 * 98! , lo que es 99! .
...
Vale, pero ¿cómo sabes que fact 0 calcula 0! ?
- Te lo puedo demostrar: fact 0 ~> 1, lo que es 0! .
Vale, te creo.

Ya que vemos que podemos hacer la prueba de nuestra definición en el tiempo finito para todos números naturales, podemos incluir esta técnica de prueba a nuestra teoría y la llamaremos la inducción matemática.

Empezamos

Primero tenemos que elegir el elemento con el que vamos a demostrar que la función es correcta. En este caso tenemos la función unaria fact n, entonces es fácil - vamos a hacer la inducción según el parámetro n.

La base de inducción

Primero demostramos que la función es correcta para el valor mínimo del parámetro. En nuestro caso demostramos que la función fact n es correcta para n = 0, es decir, fact 0 se evalúa a 0! .

fact 0 se evalúa según la primera ecuación a 1, lo que es 0! .

Hemos demostrado la base de inducción.

La proposición de inducción

El hecho de que fact 0 se cumple está demostrado en la base.
El hecho de que fact 1 se cumple lo vamos a demostrar con la proposición que fact 0 calcula 0! .
El hecho de que fact 2 se cumple lo vamos a demostrar con la proposición que fact 1 calcula 1!
El hecho de que fact 3 se cumple lo vamos a demostrar con la proposición que fact 2 calcula 2!
...

Ahora tenemos que escribir la proposición. Se podría hacer de manera siguiente:

Supongamos que la función fact n se cumple para un número entero positivo k. En otras palabras, supongamos que fact k se evalúa a k! .

Paso inductivo

El hecho de que fact 0 se cumple está demostrado en la base.
El hecho de que fact 1 se cumple lo vamos a demostrar con la proposición que fact 0 calcula 0! .
El hecho de que fact 2 se cumple lo vamos a demostrar con la proposición que fact 1 calcula 1! .
El hecho de que fact 3 se cumple lo vamos a demostrar con la proposición que fact 2 calcula 2! .
...

En general queremos mostrar que la expresión fact (k + 1) se evalúa a (k + 1)! con la proposición que fact k se evalúa a k! . Entonces demostremos. Vamos a evaluar poco a poco la expresión fact (k + 1).

fact (k + 1)  ~>  (k + 1) * fact k

En este momento vamos a usar la proposición de inducción. Sabemos que fact k se evalúa a k! . Seguimos evaluando con la proposición.

~>  (k + 1) * k!

lo que es (k + 1)! .

Hemos demostrado que la expresión fact (k + 1) se evalúa a (k + 1)! . La prueba está hecha.

La inducción con listas

Ejemplo

length       ::  [a] -> Int
length []     =  0
length (x:s)  =  1 + length s

Demostrad que la expresión length s evalúa al número de elementos de la lista s.

La prueba de inducción de la función fact n la hemos hecho según n. La inducción con listas se hace en la mayoría de casos según la longitud de una lista. También aquí vamos a demostrar que la función length s es correcta según la longitud de la lista s.

La base de inducción

Queremos mostrar que la función length está correctamente definida para el parámetro mínimo. En este caso el parámetro mínimo es la lista vacía. Mostramos entonces que length [] se evalúa a la longitud de la lista vacía, lo que es cero.

length []  ~>  0

La base se cumple entonces.

La proposición de inducción

Supongamos que la función es correcta para todas las listas s que tienen la longitud k. Esto significa que length s se evalúa a k.

El paso inductivo

En la prueba de la función fact estábamos demonstrando que estaba correctamente definida para k + 1. Entonces aquí ahora necesitamos una lista que tenga la longitud de la lista s más uno. Añadamos entonces cualquier elemento x a la lista s y demostremos que length (x:s) se evalúa a k + 1.

length (x:s)  ~>  1 + length s

Sabemos que proposición de length s se evalúa a k. La evaluación seguirá de manera siguiente:

~>  1 + k

Y esto es lo que queríamos demostrar. La prueba está hecha.

Nota

En el primer ejemplo suponemos que el parámetro de la función fact es finito. En el segundo ejemplo también suponemos que hacemos la prueba de la función length para una lista finita.

<= Funciones con booleanos lección anterior lección siguiente Entrada y salida I =>