8.8.1. Tail Recursion🔗

꼬리 재귀는 재귀 호출의 결과를 다른 방식으로 사용하지 않고 즉시 반환하는 재귀다. 이런 재귀 호출을 꼬리 호출이라고 한다. 꼬리 호출은 호출 명령 대신 점프 명령으로 컴파일할 수 있고 새 스택 프레임을 쌓는 대신 현재 프레임을 재사용할 수 있다는 점에서 중요하다. 즉 꼬리 재귀 함수는 실제로 루프다.

재귀 함수를 빠르게 만드는 흔한 방법은 누산기 전달 방식으로 다시 쓰는 것이다. 재귀 호출 결과에 할 일을 호출 스택에 기억하는 대신, 누산기라는 추가 인자로 이 정보를 모은다. 예를 들어 리스트를 뒤집는 꼬리 재귀 함수의 누산기에는 이미 본 리스트 원소가 역순으로 들어 있다.

Lean에서는 자기 자신에 대한 꼬리 호출만 루프로 최적화된다. 즉 서로에게 꼬리 호출을 하는 두 함수는 최적화되지 않는다.

8.8.2. Reference Counting and In-Place Updates🔗

Java, C#, 대부분의 JavaScript 구현처럼 추적 가비지 컬렉터를 사용하는 대신 Lean은 메모리 관리를 위해 참조 횟수를 사용한다. 메모리의 각 값에 자신을 가리키는 다른 값의 수를 기록하는 필드가 있고, 실행 시스템은 참조가 생기거나 사라질 때 이 수를 유지한다. 참조 횟수는 Python, PHP, Swift에서도 사용한다.

새 객체를 할당하라는 요청을 받으면 Lean 실행 시스템은 참조 횟수가 0으로 내려가는 기존 객체를 재활용할 수 있다. 또한 Array.set과 Array.swap 같은 배열 연산은 참조 횟수가 1이면 수정된 복사본을 할당하는 대신 배열을 변이한다. Array.swap이 배열에 대한 유일한 참조를 보유한다면 프로그램의 다른 부분은 복사된 것이 아니라 변이된 것인지 알 수 없다.

Lean에서 효율적인 코드를 작성하려면 꼬리 재귀를 사용하고 큰 배열이 유일하게 사용되는지 주의해야 한다. 함수 정의를 보면 꼬리 호출을 찾을 수 있지만 값이 유일하게 참조되는지는 프로그램 전체를 읽어야 알 수 있다. 디버깅 도우미 dbgTraceIfShared를 프로그램의 핵심 위치에서 사용하여 값이 공유되지 않는지 확인할 수 있다.

8.8.3. Proving Programs Correct🔗

프로그램을 누산기 전달 방식으로 다시 쓰거나 빠르게 만드는 변환을 하면 이해하기 어려워질 수 있다. 더 명확하게 올바른 원래 프로그램을 보존하고 최적화 버전의 실행 가능한 명세로 사용하면 유용하다. 단위 테스트 같은 기법은 다른 언어와 마찬가지로 Lean에서도 잘 작동하지만, Lean은 두 함수 버전이 모든 가능한 입력에 대해 같은 결과를 반환함을 완전히 보장하는 수학적 증명도 사용할 수 있게 한다.

보통 두 함수가 같음을 증명할 때는 함수 외연성(funext 전술)을 사용한다. 이는 모든 입력에 같은 값을 반환하면 두 함수가 같다는 원리다. 함수가 재귀적이라면 출력이 같음을 보이는 데 귀납법이 좋은 방법이다. 대개 함수의 재귀 정의는 특정 인자에 대해 재귀 호출을 하므로 그 인자를 귀납에 사용하기 좋다. 어떤 경우에는 귀납 가설이 충분히 강하지 않다. 이 문제를 고치려면 충분히 강한 귀납 가설을 제공하는 더 일반적인 정리 진술을 어떻게 구성할지 생각해야 한다. 특히 함수가 누산기 전달 버전과 동치임을 증명하려면 임의의 초기 누산기 값과 원래 함수의 최종 결과를 연결하는 정리 진술이 필요하다.

8.8.4. Safe Array Indices🔗

Fin n 타입은 n보다 엄격히 작은 자연수를 나타낸다. Fin은 “finite”의 줄임말이다. 서브타입과 마찬가지로 Fin n은 Nat과 그 Nat이 n보다 작다는 증명을 포함하는 구조체다. Fin 0 타입의 값은 없다.

arr가 Array α라면 Fin arr.size에는 항상 arr에 사용할 수 있는 인덱스가 들어 있다.

Lean은 Fin에 유용한 수치 타입 클래스 대부분의 인스턴스를 제공한다. Fin의 OfNat 인스턴스는 주어진 수가 Fin이 받아들일 수 있는 범위보다 클 때 컴파일 시점에 실패하는 대신 모듈러 산술을 수행한다.

8.8.5. Provisional Proofs🔗

때로는 실제로 증명하지 않고 명제가 증명되었다고 가장하는 것이 유용하다. 이는 다른 증명에서 다시 쓰기에 적합한지, 배열 접근이 안전한지, 재귀 호출이 원래 인자보다 더 작은 값에서 이루어지는지를 확인하는 데 유용하다. 무언가를 증명하는 데 시간을 쓴 뒤 다른 증명이 더 유용했음을 알게 되면 매우 답답하다.

sorry 전술은 실제 증명인 것처럼 명제를 임시로 받아들이게 한다. 이는 C#에서 NotImplementedException을 던지는 스텁 메서드와 비슷하다. sorry에 의존하는 모든 증명에는 Lean의 경고가 포함된다.

주의하라! sorry 전술은 거짓 명제를 포함한 어떤 명제도 증명할 수 있다. 3 < 2를 증명하면 범위를 벗어난 배열 접근이 실행 시점까지 남아 프로그램이 예기치 않게 충돌할 수 있다. 개발 중에는 sorry가 편리하지만 코드에 남겨 두는 것은 위험하다.

8.8.6. Proving Termination🔗

재귀 함수가 구조적 재귀를 사용하지 않으면 Lean은 자동으로 종료 여부를 결정할 수 없다. 이런 상황에서는 함수에 partial을 표시할 수 있다. 하지만 함수가 종료한다는 증명을 제공할 수도 있다.

부분 함수에는 중요한 단점이 있다. 타입 검사나 증명 중에 전개할 수 없다. 따라서 대화형 정리 증명기로서 Lean의 장점을 적용할 수 없다. 또한 종료해야 하는 함수가 실제로 항상 종료함을 보이면 잠재적인 버그 원인을 하나 더 없앨 수 있다.

함수 끝에 허용되는 termination_by 절을 사용하여 재귀 함수가 종료하는 이유를 지정할 수 있다. 이 절은 함수 인자를 각 재귀 호출에서 더 작아질 것으로 예상되는 표현식에 대응시킨다. 감소할 수 있는 표현식의 예로는 증가하는 배열 인덱스와 배열 크기의 차이, 재귀 호출마다 절반으로 잘리는 리스트의 길이, 재귀 호출마다 정확히 하나가 줄어드는 리스트 두 개의 쌍이 있다.

Lean에는 일부 표현식이 호출마다 줄어드는지 자동으로 결정하는 증명 자동화가 있지만, 흥미로운 프로그램 대부분에는 수동 증명이 필요하다. 이 증명은 값 대신 지역 증명을 제공하도록 설계된 let의 변형인 have로 제공할 수 있다.

재귀 함수를 작성할 때는 먼저 partial로 선언하고 올바른 답을 반환할 때까지 테스트로 디버깅하는 것이 좋다. 그런 다음 partial을 제거하고 termination_by 절로 바꾼다. Lean은 증명이 필요한 각 재귀 호출에 필요한 명제를 오류로 강조한다. 각 명제를 have에 넣고 증명은 sorry로 둘 수 있다. Lean이 프로그램을 받아들이고 테스트도 통과하면 마지막으로 Lean이 받아들일 수 있게 하는 정리를 실제로 증명한다. 이 방법은 버그가 있는 프로그램의 종료를 증명하느라 시간을 낭비하는 일을 막는다.