Lean은 재귀 def를 정의로 받아들이기 전에 그것이 끝난다는 것을 알아야 한다. 구조적 재귀는 알아서 찾는다. 아니면 정초 재귀를 시도하고, 사람은 termination_by로 측도를 지정하고 decreasing_by로 호출마다 그 값이 줄어든다는 것을 증명해서 돕는다.
콜라츠 단계 수에는 알려진 측도가 없다. 모든 입력에서 끝난다는 것을 증명한 사람이 없다. 그래서 partial def로 쓴다. Lean은 이것을 컴파일하고 실행한다. 반환 타입에 값이 존재해야 한다는 조건이 붙고, 증명 안에서는 정의가 불투명하다. 계산은 된다. 펼쳐서 추론하는 것은 안 된다.
나는 이 거래가 마음에 든다. 여기서 키워드는 사실을 말하는 사양이다. 전체 함수인 def는 모든 입력에서 반환한다고 말하고, 검사기는 그 말에 책임을 지운다. partial은 그런 말을 하지 않는다.
항상 답을 내는 검사기라면 실제로 끝나는 함수 일부도 거절할 수밖에 없다. 괜찮다. 그 거절의 비용은 정직한 키워드 하나이고, 프로그램은 여전히 돈다.
