Вступ
Одного вечора ми натрапили на старий зошит, сповнений загадкових карлючок, ніби хтось одержимо гнався за якоюсь ідеєю.
На одній сторінці виділялося єдине питання: Чи може кожне число знайти свій шлях до 1?
Воно було повʼязане з чимось, що зветься гіпотеза Коллатца, головоломкою, яка спантеличує мислителів уже десятиліттями.
Правила були оманливо простими.
Візьмімо будь-яке додатне ціле число.
- Якщо воно парне, поділімо його на 2.
- Якщо непарне, помножмо його на 3 і додаймо 1.
Потім повторімо ці кроки з результатом і так до нескінченності.
Зацікавившись, ми взяли число 12 для перевірки й почали подорож:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
Рахуючи від другого числа (6), знадобилося 9 кроків, щоб дістатися до 1, і щоразу, коли правила повторювалися, число продовжувало змінюватися.
Спершу послідовність здавалася непередбачуваною, вона стрибала вгору, вниз і в різні боки.
І все ж гіпотеза стверджує, що хоч би яким було початкове число, ми завжди закінчимо на 1.
Це було захопливо, але й загадково.
Чому це завжди, здається, працює?
Чи існує число, на якому процес ламається, зациклюється назавжди або тікає в нескінченність?
Зошит натякав, що розвʼязання цього може відкрити щось глибоке, а разом із ним на того, хто зможе розкрити його таємниці, чекають слава, багатство і місце в історії.
Вказівки
Дано додатне ціле число. Поверніть кількість кроків, потрібних для досягнення 1 за правилами гіпотези Коллатца.
Підтипи
Ця вправа визначає підтип Positive для всіх натуральних чисел, більших за 0.
Підтип можна уявити як пару ⟨x, h⟩, де x - значення, а h - доведення того, що воно задовольняє умову.
До значення всередині підтипу (у цьому випадку x) можна дістатися за допомогою .val, наприклад x.val.
До його доведення можна дістатися за допомогою .property, наприклад x.property.
До обох також можна дістатися за допомогою зіставлення зі зразком, як завжди.
Щоб побудувати значення підтипу, потрібно довести, що воно задовольняє умову, а в цьому випадку - що число більше за 0.
У Lean є чимало лем і теорем, які можуть стати відправною точкою для цього доведення.
Наприклад, лема Nat.zero_lt_succ стверджує, що для будь-якого натурального числа n: 0 < n + 1.
Гарний довідник із доведення теорем у Lean можна знайти в основній документації.
Доведення завершуваності
У Lean рекурсивні функції повинні доводити свою завершуваність.
Іноді це доведення очевидне і неявно випливає зі структури функції.
В інших випадках його потрібно зробити явним.
У цій вправі завершуваність функції - це саме collatz conjecture, яка є відкритою математичною проблемою.
Розгляньмо один із таких варіантів:
- Якщо додати ключове слово
partial перед оголошенням функції, це вимикає перевірку завершуваності та дозволяє (потенційно небезпечні) рекурсивні виклики.
- Імперативні конструкції, дозволені в монадному коді, як-от
while, усередині реалізовано через часткову рекурсію, тож їх можна використовувати завжди, коли завершуваність не вимагається.
Використання монади Id - зручний спосіб увімкнути ці конструкції в коді, який інакше має вигляд чистого, не додаючи жодних додаткових ефектів.
- Якщо визначити допоміжну функцію з додатковим параметром для максимальної кількості рекурсивних викликів, це забезпечить завершуваність.
