Eso es simple y complejo al mismo tiempo.
Primero tratemos de entender lo que significa “correcto”, mirando uno de los ejemplos más simples de correcto: solo devuelve algo del tipo correcto .
¿Cómo saber si una función devuelve algo del tipo correcto? Observa todas las declaraciones de retorno y verifica que la expresión escrita allí tenga el tipo correcto. Pero, ¿qué pasa si estas expresiones incluyen una llamada recursiva?
- Soy completamente nuevo en algoritmos. ¿Cuál es el mejor libro / curso / método para realmente entrar en ellos?
- ¿Qué son los patrones de búsqueda?
- ¿Cuáles son algunos algoritmos fáciles de implementar para la localización basada en características o puntos de referencia de robots móviles 2-D?
- Cómo escribir un algoritmo para un programa complicado que tiene muchos bucles, conmutadores y otros procesos dentro de una instrucción if
- ¿Cómo escribo un algoritmo para el problema de las 100 puertas?
Lo mejor que puede hacer es decir que suponiendo que las llamadas recursivas solo devuelvan algo del tipo correcto, podemos garantizarle que también solo devolvemos algo del tipo correcto. En resumen, su código nunca hace que el tipo de retorno sea incorrecto (aunque puede transmitir algo incorrecto que obtuvo de una llamada de función recursiva).
Pero si puede garantizar esto, ¿cómo puede la función devolver algo del tipo incorrecto? Imagine que la función vuelve después de las llamadas recursivas [math] x [/ math] y el tipo es incorrecto. Como su código nunca hace que el tipo sea incorrecto, ya después de las llamadas recursivas [math] x-1 [/ math] devolvió el tipo incorrecto. Y así, después de [matemáticas] x-2 [/ matemáticas], y [matemáticas] x-3 [/ matemáticas] … Puede continuar con esto hasta [matemáticas] 0 [/ matemáticas] llamadas recursivas y un tipo de retorno incorrecto. Pero esto no es posible, porque la única forma de obtener un tipo incorrecto es desde una llamada de función recursiva.
Ahora, si observa nociones más complejas de corrección (que en algunos lenguajes geniales se pueden codificar en el tipo de retorno :)), notará que el mismo patrón se cumple aquí: para que su función sea incorrecta, tiene que haber algún código que hace que el valor de retorno (o efecto en el estado) sea incorrecto. Por lo tanto, siempre que su código nunca haga que el efecto de la función sea incorrecto, la función no puede volverse incorrecta.
Por cierto, el principio matemático detrás de este tipo de razonamiento se llama inducción y vale la pena aprenderlo.
