Bevezetés
Egy este egy régi füzetre bukkantál, amely tele volt rejtélyes firkákkal, mintha valaki megszállottan üldözött volna egy ötletet.
Az egyik oldalon egyetlen kérdés tűnt ki: Vajon minden szám megtalálja az útját az 1-ig?
A kérdés valamihez kapcsolódott, amit Collatz-sejtésnek neveznek: egy rejtvényhez, amely évtizedek óta zavarba hozza a gondolkodókat.
A szabályok megtévesztően egyszerűek voltak.
Válassz egy tetszőleges pozitív egész számot.
- Ha páros, oszd el 2-vel.
- Ha páratlan, szorozd meg 3-mal, és adj hozzá 1-et.
Ezután ismételd meg ezeket a lépéseket az eredménnyel, és folytasd így a végtelenségig.
Kíváncsian a 12-es számot választottad ki próbaként, és elkezdted az utat:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
A második számtól (6) számolva 9 lépés kellett az 1 eléréséhez, és valahányszor újra alkalmaztad a szabályokat, a szám folyton változott.
Eleinte a sorozat kiszámíthatatlannak tűnt, fel-le és mindenfelé ugrált.
A sejtés mégis azt állítja, hogy bármelyik számmal is kezded, mindig az 1-nél kötsz ki.
Lenyűgöző volt, ugyanakkor zavarba ejtő is.
Miért tűnik úgy, hogy ez mindig működik?
Lehet olyan szám, ahol a folyamat megakad, örökké ismétlődik, vagy a végtelenbe szökik?
A füzet azt sugallta, hogy ennek megoldása valami mélyreható dologra világíthat rá, és ezzel együtt hírnév, vagyon és hely a történelemben vár arra, aki fel tudja oldani a titkait.
Utasítások
Adott egy pozitív egész szám, add vissza az 1 eléréséhez szükséges lépések számát a Collatz-sejtés szabályai szerint.
Subtype-ok
Ez a feladat definiál egy Positive nevű Subtype-ot, a 0-nál nagyobb természetes számokra. A Subtype felfogható egy ⟨x, h⟩ párként, ahol x az érték, h pedig az érvényességének a bizonyítéka.
A Subtype belsejében lévő érték (jelen esetben x) a .val használatával érhető el, például x.val. A bizonyítéka a .property használatával érhető el, például x.property. Mindkettő elérhető mintaillesztéssel is, ahogy az megszokott.
Ahhoz, hogy értéket hozz létre egy Subtype-hoz, be kell bizonyítanod az érvényességét, jelen esetben azt, hogy a szám nagyobb 0-nál.
A Leanben számos lemma és tétel szolgálhat kiindulópontként ehhez a bizonyításhoz. Például a Nat.zero_lt_succ egy olyan lemma, amely azt állítja, hogy bármely n természetes számra: 0 < n + 1.
A Leanbeli tételbizonyításhoz jó referencia az alapdokumentáció.
A terminálás bizonyítása
A Leanben a rekurzív függvényeknek bizonyítaniuk kell a terminálásukat. Ez a bizonyítás néha egyszerű, és implicit módon következik a függvény szerkezetéből. Más esetekben viszont explicit módon meg kell adni.
Ebben a feladatban a függvény terminálása éppen a collatz conjecture, ami egy nyitott matematikai probléma.
Fontold meg az alábbi lehetőségek valamelyikét:
- Ha a
partial kulcsszót egy függvény deklarációja elé teszed, az letiltja a terminálás ellenőrzését, és lehetővé teszi a (potenciálisan nem biztonságos) rekurzív hívásokat.
- A monádikus kódban engedélyezett imperatív szerkezetek, például a
while, a háttérben részleges rekurzióval vannak megvalósítva, így akkor használhatók, amikor a terminálást nem kényszerítjük ki.
Az Id monád kényelmes módja annak, hogy ezeket a szerkezeteket egyébként tisztának tűnő kódban is engedélyezd, anélkül hogy további mellékhatásokat vezetnél be.
- Egy segédfüggvény definiálása egy plusz paraméterrel a rekurzív hívások maximális számára garantálja a terminálást.
