8.8.1. 꼬리 재귀🔗

꼬리 재귀는 재귀 호출의 결과가 다른 방식으로 사용되지 않고 즉시 반환되는 재귀입니다. 이러한 재귀 호출을 꼬리 호출이라고 합니다. 꼬리 호출은 호출 명령어 대신 점프 명령어로 컴파일될 수 있고, 새 프레임을 푸시하는 대신 현재 스택 프레임을 재사용할 수 있다는 점에서 흥미롭습니다. 다시 말해, 꼬리 재귀 함수는 실제로는 루프입니다.

재귀 함수를 더 빠르게 만드는 일반적인 방법은 이를 누산기 전달 방식(accumulator-passing style)으로 다시 작성하는 것입니다. 재귀 호출의 결과로 무엇을 해야 하는지 기억하기 위해 콜 스택을 사용하는 대신, 누산기라고 불리는 추가 인자를 사용하여 이 정보를 수집합니다. 예를 들어, 리스트를 뒤집는 꼬리 재귀 함수의 누산기는 이미 살펴본 리스트 항목들을 역순으로 담고 있습니다.

Lean에서는 자기 자신에 대한 꼬리 호출만 루프로 최적화됩니다. 다시 말해, 서로를 꼬리 호출로 끝맺는 두 함수는 최적화되지 않습니다.

8.8.2. 참조 카운팅과 제자리 갱신🔗

Java, C#, 대부분의 JavaScript 구현체에서 사용하는 것과 같은 추적 가비지 컬렉터를 사용하는 대신, Lean은 메모리 관리를 위해 참조 계수(reference counting)를 사용합니다. 이는 메모리 내의 각 값이 다른 값들이 자신을 얼마나 참조하고 있는지 추적하는 필드를 포함하며, 런타임 시스템이 참조가 생성되거나 소멸될 때마다 이 개수를 관리한다는 것을 의미합니다. 참조 계수는 Python, PHP, Swift에서도 사용됩니다.

새 객체를 할당하라는 요청을 받으면, Lean의 런타임 시스템은 참조 카운트가 0으로 떨어지는 기존 객체를 재활용할 수 있습니다. 또한 Array.set이나 Array.swap과 같은 배열 연산은 참조 카운트가 1일 경우 수정된 복사본을 할당하는 대신 배열을 직접 변경합니다. 만약 Array.swap이 배열에 대한 유일한 참조를 가지고 있다면, 프로그램의 다른 어떤 부분도 그 배열이 복사된 것이 아니라 변이된 것임을 알아챌 수 없습니다.

Lean에서 효율적인 코드를 작성하려면 꼬리 재귀를 사용해야 하며, 큰 배열이 고유하게 사용되도록 주의를 기울여야 합니다. 꼬리 호출은 함수의 정의를 살펴봄으로써 식별할 수 있지만, 어떤 값이 고유하게 참조되는지 이해하려면 프로그램 전체를 읽어야 할 수도 있습니다. 디버깅 도우미 dbgTraceIfShared는 프로그램의 핵심 위치에서 값이 공유되지 않았는지 확인하는 데 사용할 수 있습니다.

8.8.3. 프로그램 정확성 증명하기🔗

프로그램을 누산기 전달 방식으로 다시 작성하거나 더 빠르게 실행되도록 다른 변환을 가하는 것은 프로그램을 이해하기 더 어렵게 만들 수도 있습니다. 더 명확하게 올바른 원본 버전의 프로그램을 그대로 유지한 다음, 이를 최적화된 버전을 위한 실행 가능한 명세로 사용하는 것이 유용할 수 있습니다. 단위 테스트와 같은 기법이 다른 언어에서와 마찬가지로 Lean에서도 잘 작동하지만, Lean은 또한 함수의 두 버전이 가능한 모든 입력에 대해 동일한 결과를 반환함을 완전히 보장하는 수학적 증명을 사용할 수 있게 합니다.

일반적으로, 두 함수가 같음을 증명하는 것은 함수 외연성(function extensionality, funext 택틱)을 사용하여 이루어지는데, 이는 두 함수가 모든 입력에 대해 같은 값을 반환하면 같다는 원리입니다. 함수가 재귀적이라면, 귀납법은 대개 두 함수의 출력이 같음을 증명하는 좋은 방법입니다. 일반적으로 함수의 재귀적 정의는 특정 인자에 대해 재귀 호출을 수행하는데, 이 인자가 귀납법에 적합한 선택입니다. 어떤 경우에는 귀납 가설이 충분히 강력하지 않습니다. 이 문제를 해결하려면 보통 충분히 강력한 귀납 가설을 제공하는, 더 일반화된 버전의 정리 명제를 어떻게 구성할지에 대한 고민이 필요합니다. 특히, 어떤 함수가 누산기를 전달하는 버전과 동등함을 증명하려면 임의의 초기 누산기 값과 원래 함수의 최종 결과를 관계짓는 정리 명제가 필요합니다.

8.8.4. 안전한 배열 인덱스🔗

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. 잠정 증명🔗

때로는 어떤 명제를 실제로 증명하는 작업을 하지 않고도 증명된 것처럼 가장하는 것이 유용할 수 있습니다. 이는 어떤 명제의 증명이 다른 증명에서의 재작성, 배열 접근이 안전함을 판별하는 것, 재귀 호출이 원래 인자보다 작은 값에 대해 이루어짐을 보이는 것과 같은 특정 작업에 적합한지 확인할 때 유용할 수 있습니다. 무언가를 증명하는 데 시간을 들였는데, 나중에서야 다른 증명이 더 유용했을 것임을 알게 되면 매우 답답한 일입니다.

sorry 택틱은 Lean이 어떤 명제를 실제 증명인 것처럼 잠정적으로 받아들이게 합니다. 이는 C#에서 NotImplementedException을 던지는 스텁 메서드와 유사하다고 볼 수 있습니다. sorry에 의존하는 증명에는 Lean에서 경고가 포함됩니다.

주의하십시오! sorry 택틱은 거짓 명제를 포함하여 어떤 명제든 증명할 수 있습니다. 3 < 2임을 증명하면 배열 범위를 벗어난 접근이 런타임까지 남아 있게 되어 예기치 않게 프로그램이 충돌할 수 있습니다. sorry를 사용하는 것은 개발 중에는 편리하지만, 이를 코드에 남겨두는 것은 위험합니다.

8.8.6. 종료성 증명🔗

재귀 함수가 구조적 재귀를 사용하지 않는 경우, Lean은 해당 함수가 종료됨을 자동으로 판단할 수 없습니다. 이런 상황에서는 함수를 그냥 partial로 표시해도 됩니다. 하지만 함수가 종료함을 증명으로 제공하는 것도 가능합니다.

부분 함수에는 중요한 단점이 있습니다: 타입 검사 중이나 증명에서 펼쳐질(unfold) 수 없다는 것입니다. 이는 대화형 정리 증명기로서 Lean이 지니는 가치를 이들에게 적용할 수 없다는 것을 의미합니다. 또한, 종료될 것으로 예상되는 함수가 실제로 항상 종료됨을 보이는 것은 잠재적인 버그의 원인을 하나 더 제거해 줍니다.

함수 끝에 사용할 수 있는 termination_by 절은 재귀 함수가 종료하는 이유를 명시하는 데 사용할 수 있습니다. 이 절은 함수의 인자를 각 재귀 호출마다 더 작아질 것으로 예상되는 표현식에 대응시킵니다. 감소할 수 있는 표현식의 예로는 배열에 대해 증가하는 인덱스와 배열 크기의 차이, 각 재귀 호출마다 절반으로 줄어드는 리스트의 길이, 혹은 재귀 호출마다 정확히 하나씩만 줄어드는 리스트 쌍 등이 있습니다.

Lean에는 일부 표현식이 호출마다 감소함을 자동으로 판별할 수 있는 증명 자동화 기능이 포함되어 있지만, 흥미로운 프로그램 중 상당수는 수동 증명이 필요합니다. 이러한 증명은 have를 사용하여 제공할 수 있는데, 이는 값이 아니라 증명을 지역적으로 제공하기 위한 let의 한 형태입니다.

재귀 함수를 작성하는 좋은 방법은 우선 partial로 선언한 뒤, 테스트를 통해 올바른 결과를 반환할 때까지 디버깅하는 것입니다. 그런 다음, partial을 제거하고 termination_by 절로 대체할 수 있습니다. Lean은 증명이 필요한 각 재귀 호출에 오류 강조 표시를 배치하며, 이때 증명해야 할 명제가 그 안에 포함됩니다. 이 문장들은 각각 have에 배치할 수 있으며, 증명은 sorry로 둘 수 있습니다. Lean이 프로그램을 받아들이고 여전히 테스트를 통과한다면, 마지막 단계는 Lean이 이를 받아들일 수 있게 하는 정리들을 실제로 증명하는 것입니다. 이 접근 방식은 버그가 있는 프로그램이 종료함을 증명하는 데 시간을 낭비하는 것을 방지할 수 있습니다.