Introducción
Una tarde, te topaste con un viejo cuaderno lleno de garabatos crípticos, como si alguien hubiera estado persiguiendo una idea de forma obsesiva.
En una de sus páginas, destacaba una sola pregunta: ¿Puede todo número encontrar su camino hasta el 1?
Estaba ligada a algo llamado la conjetura de Collatz, un rompecabezas que ha desconcertado a los pensadores durante décadas.
Las reglas eran engañosamente sencillas.
Elige cualquier número entero positivo.
- Si es par, divídelo entre 2.
- Si es impar, multiplícalo por 3 y súmale 1.
Después, repite estos pasos con el resultado, y continúa así indefinidamente.
Con curiosidad, elegiste el número 12 para probarlo y comenzaste el viaje:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
Contando desde el segundo número (6), hicieron falta 9 pasos para llegar a 1, y cada vez que se repetían las reglas, el número no dejaba de cambiar.
Al principio, la secuencia parecía impredecible: subía, bajaba y saltaba de un lado para otro.
Sin embargo, la conjetura afirma que, sea cual sea el número de partida, siempre acabaremos en 1.
Era fascinante, pero también desconcertante.
¿Por qué parece funcionar siempre?
¿Podría existir algún número en el que el proceso se rompa, entrando en un bucle infinito o escapando hacia el infinito?
El cuaderno daba a entender que resolver esto podría revelar algo profundo, y que, con ello, la fama, la fortuna y un lugar en la historia esperan a quien sea capaz de desvelar sus secretos.
Instrucciones
Dado un número entero positivo, devuelve el número de pasos que se necesitan para llegar a 1 según las reglas de la conjetura de Collatz.
Subtipos
Este ejercicio define un subtipo llamado Positive, para todos los números naturales mayores que 0.
Un subtipo se puede entender como un par ⟨x, h⟩, donde x es el valor y h es la demostración de su validez.
Al valor que hay dentro de un subtipo (x, en este caso) se puede acceder mediante .val; por ejemplo, x.val.
A su demostración se puede acceder mediante .property; por ejemplo, x.property.
También se puede acceder a ambos con la coincidencia de patrones, como de costumbre.
Para construir un valor de un subtipo es necesario demostrar su validez; en este caso, que el número es mayor que 0.
En Lean hay varios lemas y teoremas que pueden servir como punto de partida para esta demostración.
Por ejemplo, Nat.zero_lt_succ es un lema que afirma que, para cualquier número natural n: 0 < n + 1.
Puedes encontrar una buena referencia sobre la demostración de teoremas en Lean en la documentación principal.
Demostración de terminación
En Lean, las funciones recursivas deben demostrar su terminación.
A veces esta demostración es sencilla, pues se deduce implícitamente de la estructura de la función.
En otros casos, hay que hacerla explícita.
En este ejercicio, la terminación de la función es precisamente la collatz conjecture, que es un problema matemático abierto.
Considera usar una de las siguientes opciones:
- Añadir la palabra clave
partial antes de la declaración de una función desactiva la comprobación de terminación y permite llamadas recursivas (potencialmente inseguras).
- Las construcciones imperativas permitidas en código monádico, como
while, se implementan internamente con recursión parcial, así que se pueden usar siempre que no se exija la terminación.
Usar la mónada Id es una forma cómoda de habilitar estas construcciones en código que por lo demás parece puro, sin introducir efectos adicionales.
- Definir una función auxiliar con un parámetro extra para el número máximo de llamadas recursivas garantiza la terminación.
