Introduzione
Una sera ti è capitato tra le mani un vecchio quaderno pieno di scarabocchi criptici, come se qualcuno stesse inseguendo un'idea in modo ossessivo.
Su una pagina spiccava una sola domanda: Ogni numero può trovare la strada verso 1?
Era legata a qualcosa chiamato Congettura di Collatz, un enigma che ha lasciato perplessi i pensatori per decenni.
Le regole erano ingannevolmente semplici.
Scegli un numero intero positivo.
- Se è pari, dividilo per 2.
- Se è dispari, moltiplicalo per 3 e aggiungi 1.
Poi ripeti questi passaggi con il risultato, continuando all'infinito.
La curiosità ti ha spinto a scegliere il numero 12 per provarlo, e così hai iniziato il viaggio:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
Partendo dal secondo numero (6), ci sono voluti 9 passaggi per arrivare a 1, e ogni volta che le regole si ripetevano il numero continuava a cambiare.
All'inizio la sequenza sembrava imprevedibile: saltava su, giù, dappertutto.
Eppure la congettura afferma che, qualunque sia il numero di partenza, si finisce sempre a 1.
Era affascinante, ma anche sconcertante.
Perché sembra funzionare sempre?
Potrebbe esistere un numero in cui il processo si rompe, ripetendosi all'infinito o fuggendo verso l'infinito?
Il quaderno suggeriva che risolverlo avrebbe potuto rivelare qualcosa di profondo: e con esso attendono fama, fortuna e un posto nella storia chiunque riesca a svelarne i segreti.
Istruzioni
Dato un numero intero positivo, restituisci il numero di passi necessari per arrivare a 1 secondo le regole della congettura di Collatz.
Subtype
Questo esercizio definisce un Subtype chiamato Positive, per tutti i numeri naturali maggiori di 0.
Un Subtype può essere pensato come una coppia ⟨x, h⟩, dove x è il valore e h è la dimostrazione della sua validità.
Il valore contenuto in un Subtype (x, in questo caso) è accessibile tramite .val, per esempio x.val.
La sua dimostrazione è accessibile tramite .property, per esempio x.property.
Entrambi sono accessibili anche tramite pattern matching, come al solito.
Per costruire un valore per un Subtype, è necessario dimostrarne la validità, in questo caso, che il numero sia maggiore di 0.
Ci sono diversi lemmi e teoremi in Lean che possono servire come punto di partenza per questa dimostrazione.
Per esempio, Nat.zero_lt_succ è un lemma che afferma che per ogni numero naturale n: 0 < n + 1.
Un buon riferimento per la dimostrazione di teoremi in Lean si trova nella documentazione principale.
Dimostrazione della terminazione
In Lean, le funzioni ricorsive devono dimostrare la propria terminazione.
Questa dimostrazione a volte è immediata, perché segue implicitamente dalla struttura di una funzione.
In altri casi, deve essere resa esplicita.
In questo esercizio, la terminazione della funzione è esattamente la collatz conjecture, che è un problema matematico aperto.
Considera di usare una delle seguenti opzioni:
- Aggiungere la parola chiave
partial prima della dichiarazione di una funzione disattiva il controllo di terminazione e consente chiamate ricorsive (potenzialmente non sicure).
- I costrutti imperativi ammessi nel codice monadico, come
while, sono implementati internamente tramite ricorsione parziale, quindi possono essere usati ogni volta che la terminazione non è imposta.
Usare la monade Id è un modo comodo per abilitare questi costrutti in codice dall'aspetto altrimenti puro, senza introdurre effetti aggiuntivi.
- Definire una funzione ausiliaria con un parametro aggiuntivo per il numero massimo di chiamate ricorsive garantisce la terminazione.
