소개
어느 저녁, 누군가 어떤 아이디어를 집요하게 좇고 있었던 것처럼, 알쏭달쏭한 낙서로 가득한 낡은 공책을 우연히 발견했어요.
한 페이지에는 질문 하나가 눈에 띄었어요: 모든 수는 1까지 갈 수 있을까?
그것은 콜라츠 추측이라는 것과 연결되어 있었어요. 수십 년째 수많은 사람을 골머리 앓게 한 수수께끼였죠.
규칙은 보기보다 단순했어요.
아무 양의 정수나 하나 골라요.
- 짝수라면, 2로 나눠요.
- 홀수라면, 3을 곱하고 1을 더해요.
그런 다음, 그 결과로 이 단계들을 끝없이 반복해요.
궁금해진 나머지, 시험 삼아 12를 골라 여정을 시작했어요:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
두 번째 수(6)부터 세면 1에 도달하기까지 9단계가 걸렸고, 규칙이 반복될 때마다 수는 계속 바뀌었어요.
처음에는 수열이 예측할 수 없어 보였어요. 위로, 아래로, 사방으로 마구 튀는 것처럼요.
그런데도 이 추측은 시작하는 수가 무엇이든 항상 1에서 끝난다고 말해요.
흥미롭기도 했지만, 동시에 알쏭달쏭했어요.
왜 이게 항상 통하는 걸까요?
이 과정이 무너져서 영원히 반복되거나 무한으로 빠져나가는 수가 있을까요?
공책은 이걸 풀어내면 뭔가 심오한 것을 밝혀낼 수 있다고 암시했어요. 그리고 그와 함께 명성과 재산, 역사에 남을 자리가 그 비밀을 풀어내는 사람을 기다리고 있죠.
지침
양의 정수가 주어지면, 콜라츠 추측의 규칙에 따라 1에 도달할 때까지 걸리는 단계 수를 반환해요.
Subtype
이 연습 문제는 0보다 큰 모든 자연수를 위한 Positive라는 Subtype을 정의해요.
Subtype은 ⟨x, h⟩라는 쌍으로 생각할 수 있는데, 여기서 x는 값이고 h는 그 값이 유효하다는 증명이에요.
Subtype 안의 값(여기서는 x)은 .val을 사용해 접근할 수 있어요. 예를 들어 x.val처럼요.
그 증명은 .property를 사용해 접근할 수 있어요. 예를 들어 x.property처럼요.
둘 다 평소처럼 패턴 매칭으로도 접근할 수 있어요.
Subtype의 값을 만들려면 그 값의 유효성, 즉 이 경우에는 수가 0보다 크다는 것을 증명해야 해요.
Lean에는 이 증명의 출발점이 될 수 있는 보조정리와 정리가 여러 개 있어요.
예를 들어 Nat.zero_lt_succ는 모든 자연수 n에 대해 0 < n + 1임을 주장하는 보조정리예요.
Lean에서 정리를 증명하는 데 참고할 만한 좋은 자료는 핵심 문서에서 찾을 수 있어요.
종료 증명
Lean에서 재귀 함수는 자신이 종료된다는 것을 증명해야 해요.
이 증명은 때로는 함수의 구조에서 자연스럽게 따라 나오는 간단한 것이기도 하고, 다른 경우에는 명시적으로 밝혀야 하기도 해요.
이 연습 문제에서 함수의 종료는 바로 collatz conjecture, 즉 아직 해결되지 않은 수학 문제예요.
다음 방법 중 하나를 써 보는 것도 좋아요:
- 함수 선언 앞에
partial 키워드를 붙이면 종료 검사를 끄고 (잠재적으로 안전하지 않은) 재귀 호출을 허용해요.
- 모나드 코드에서 허용되는 명령형 구조, 예를 들어
while은 내부적으로 부분 재귀를 사용해 구현되므로, 종료가 강제되지 않는 곳이라면 어디서든 쓸 수 있어요.
Id 모나드를 사용하면 겉보기에는 순수해 보이는 코드에서 추가적인 효과를 들이지 않고 이런 구조를 쓸 수 있는 편리한 방법이 돼요.
- 최대 재귀 호출 횟수를 위한 추가 매개변수를 가진 도우미 함수를 정의하면 종료를 보장할 수 있어요.
