8.6. 삽입 정렬과 배열 변경
삽입 정렬(insertion sort)은 정렬 알고리즘으로서 최적의 최악 경우 시간 복잡도를 가지지는 않지만, 여전히 여러 유용한 속성을 가지고 있습니다:
-
이는 구현하고 이해하기에 간단하고 직관적입니다
-
이 알고리즘은 실행에 추가 공간이 필요 없는 제자리(in-place) 알고리즘입니다.
-
이는 안정 정렬입니다
-
입력이 이미 거의 정렬되어 있는 경우에는 빠릅니다.
제자리(in-place) 알고리즘은 Lean이 메모리를 관리하는 방식 때문에 특히 유용합니다. 일부 경우에는 일반적으로 배열을 복사하는 연산이 변경(mutation)으로 최적화될 수 있습니다. 이는 배열의 원소를 교환하는 것을 포함합니다.
JavaScript, JVM, .NET을 비롯하여 자동 메모리 관리를 지원하는 대부분의 언어와 런타임 시스템은 추적 가비지 컬렉션(tracing garbage collection)을 사용합니다. 메모리를 회수해야 할 때, 시스템은 여러 개의 root(호출 스택 및 전역 값 등)에서 시작하여 포인터를 재귀적으로 추적함으로써 어떤 값에 도달할 수 있는지를 판단합니다. 도달할 수 없는 값은 모두 할당 해제되어 메모리가 해제됩니다.
참조 카운팅은 추적 가비지 컬렉션의 대안으로, Python, Swift, Lean을 비롯한 여러 언어에서 사용됩니다. 참조 카운팅을 사용하는 시스템에서는 메모리상의 각 객체가 자신을 참조하는 개수를 추적하는 필드를 가지고 있습니다. 새 참조가 생성되면 카운터가 증가합니다. 참조가 더 이상 존재하지 않게 되면, 카운터가 감소합니다. 카운터가 0에 도달하면 해당 객체는 즉시 할당 해제됩니다.
참조 카운팅은 추적 가비지 컬렉터에 비해 한 가지 중요한 단점이 있습니다. 순환 참조가 메모리 누수로 이어질 수 있다는 것입니다. 객체 A가 객체 B를 참조하고, 객체 B가 객체 A를 참조한다면, 프로그램의 다른 어떤 것도 A나 B를 참조하지 않더라도 이들은 결코 할당 해제되지 않습니다. 순환 참조는 통제되지 않은 재귀 또는 가변 참조에서 발생합니다. Lean은 둘 다 지원하지 않으므로, 순환 참조를 구성하는 것은 불가능합니다.
참조 계수는 데이터 구조를 할당하고 해제하는 Lean 런타임 시스템의 프리미티브가 참조 계수가 곧 0이 되려는지 확인하고, 새 객체를 할당하는 대신 기존 객체를 재사용할 수 있음을 의미합니다. 이는 특히 큰 배열을 다룰 때 중요합니다.
Lean 배열을 위한 삽입 정렬 구현은 다음 기준을 만족해야 합니다:
-
Lean은
partial어노테이션 없이도 함수를 받아들여야 합니다 -
다른 참조가 없는 배열이 전달된 경우, 새 배열을 할당하는 대신 해당 배열을 제자리에서 수정해야 합니다
첫 번째 기준은 확인하기 쉽습니다. Lean이 정의를 받아들이면 이 기준은 충족됩니다. 그러나 두 번째는 이를 테스트할 수단이 필요합니다. Lean은 다음과 같은 시그니처를 가진 dbgTraceIfShared라는 내장 함수를 제공합니다:
#check dbgTraceIfShared이 함수는 문자열과 값을 인자로 받으며, 값의 참조가 두 개 이상이면 해당 문자열을 사용한 메시지를 표준 오류로 출력하고, 값을 반환합니다. 엄밀히 말하면 이것은 순수 함수가 아닙니다. 하지만 이는 함수가 메모리를 할당하고 복사하는 대신 실제로 재사용할 수 있는지 확인하기 위해 개발 중에만 사용되도록 의도된 것입니다.
dbgTraceIfShared를 사용하는 방법을 익힐 때, #eval이 컴파일된 코드에서보다 훨씬 더 많은 값이 공유된다고 보고한다는 점을 아는 것이 중요합니다. 이는 혼란스러울 수 있습니다. 편집기에서 실험하기보다는 lake로 실행 파일을 빌드하는 것이 중요합니다.
삽입 정렬은 두 개의 루프로 구성됩니다. 바깥쪽 루프는 정렬할 배열을 가로질러 포인터를 왼쪽에서 오른쪽으로 이동시킵니다. 각 반복이 끝날 때마다 포인터 왼쪽에 있는 배열 영역은 정렬되어 있지만, 오른쪽 영역은 아직 정렬되어 있지 않을 수 있습니다. 내부 루프는 포인터가 가리키는 요소를 가져와 적절한 위치를 찾고 루프 불변식이 복원될 때까지 왼쪽으로 이동시킵니다. 다시 말해, 각 반복마다 배열의 다음 원소를 정렬된 영역의 적절한 위치에 삽입합니다.
8.6.1. 내부 루프
삽입 정렬의 내부 루프는 배열과 삽입 중인 원소의 인덱스를 인수로 받는 꼬리 재귀 함수로 구현할 수 있습니다. 삽입되는 원소는 왼쪽 원소가 더 작거나 배열의 시작에 도달할 때까지 왼쪽 원소와 반복적으로 교환됩니다. 내부 루프는 배열을 인덱싱하는 데 사용되는 Fin 안에 있는 Nat에 대해 구조적으로 재귀적입니다.
def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
match i with
| ⟨0, _⟩ => arr
| ⟨i' + 1, _⟩ =>
match Ord.compare arr[i'] arr[i] with
| .lt | .eq => arr
| .gt =>
insertSorted (arr.swap i' i) ⟨i', α:Type ?u.3inst✝:Ord αarr:Array αi:Fin arr.sizei':NatisLt✝:i' + 1 < arr.size⊢ i' < (arr.swap i' ↑i ⋯ ⋯).size All goals completed! 🐙⟩
인덱스 i가 0이면, 정렬된 영역에 삽입되는 원소가 해당 영역의 시작에 도달한 것이며 가장 작은 원소입니다. 인덱스가 i' + 1이면, i'에 있는 원소를 i에 있는 원소와 비교해야 합니다. i는 Fin arr.size이지만, i'는 i의 val 필드에서 나온 값이기 때문에 그냥 Nat일 뿐이라는 점에 유의하십시오. 그럼에도 불구하고, 배열 인덱스 표기법을 검사하는 데 사용되는 증명 자동화에는 선형 정수 산술 솔버가 포함되어 있으므로, i'는 자동으로 인덱스로 사용할 수 있습니다.
두 원소를 조회하여 비교합니다. 왼쪽 원소가 삽입되는 원소보다 작거나 같으면 루프가 종료되고 불변량이 복원됩니다. 왼쪽 원소가 삽입되는 원소보다 크면 두 원소가 교환되고 내부 루프가 다시 시작됩니다. Array.swap은 두 인덱스 모두를 Nat으로 받으며, 배열 인덱싱과 마찬가지로 뒤에서 동일한 택틱을 사용하여 이들이 범위 내에 있음을 보장합니다.
그럼에도 불구하고, 재귀 호출에 사용되는 Fin에는 두 원소를 교환한 결과에서 i'이(가) 범위 내에 있다는 증명이 필요합니다. grind 택틱의 데이터베이스에는 배열의 두 원소를 맞바꿔도 크기가 변하지 않는다는 사실이 포함되어 있습니다. i' + 1가 원래 배열에서 범위 안에 있다는 사실과 이를 결합하면, grind는 교환 후에 i'가 범위 안에 있다는 것을 결론지을 수 있습니다.
8.6.2. 외부 루프
삽입 정렬의 외부 루프는 포인터를 왼쪽에서 오른쪽으로 이동시키며, 각 반복마다 insertSorted를 호출하여 포인터가 가리키는 원소를 배열 내 올바른 위치에 삽입합니다. 이 루프의 기본 형태는 Array.map의 구현과 유사합니다.
def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
if h : i < arr.size then
insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
else
arr재귀 호출마다 감소하는 인자가 없기 때문에 오류가 발생합니다:
Lean은 각 반복마다 일정한 상한을 향해 증가하는 Nat이 종료하는 함수로 이어짐을 증명할 수 있지만, 이 함수는 각 반복마다 배열이 insertSorted를 호출한 결과로 대체되기 때문에 일정한 상한을 가지지 않습니다.
종료 증명을 구성하기 전에, partial 수정자를 사용해 정의를 테스트하여 예상된 답을 반환하는지 확인하는 것이 편리할 수 있습니다:
partial def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
if h : i < arr.size then
insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
else
arr#eval insertionSortLoop #[5, 17, 3, 8] 0#eval insertionSortLoop #["metamorphic", "igneous", "sedimentary"] 08.6.2.1. 종료
이번에도, 처리 중인 배열의 크기와 인덱스 사이의 차이가 각 재귀 호출마다 감소하기 때문에 이 함수는 종료됩니다. 하지만 이번에는 Lean이 termination_by를 받아들이지 않습니다:
def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
if h : i < arr.size then
insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
else
arr
termination_by arr.size - i
문제는 insertSorted가 전달받은 배열과 동일한 크기의 배열을 반환한다는 것을 Lean이 알 방법이 없다는 점입니다. insertionSortLoop가 종료함을 증명하려면, 먼저 insertSorted가 배열의 크기를 바꾸지 않는다는 것을 증명해야 합니다. 오류 메시지에서 증명되지 않은 종료 조건을 함수로 복사하고 이를 sorry로 “증명”하면 함수가 일시적으로 승인되도록 허용됩니다:
def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
if h : i < arr.size then
have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := α:Type ?u.3inst✝:Ord αarr:Array αi:Nath:i < arr.size⊢ (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i
All goals completed! 🐙
insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
else
arr
termination_by arr.size - i
insertSorted는 삽입할 원소의 인덱스에 대해 구조적으로 재귀적이므로, 증명은 해당 인덱스에 대한 귀납법으로 진행해야 합니다. 기본 경우에는 배열이 변경되지 않은 채로 반환되므로, 그 길이는 확실히 변하지 않습니다. 귀납 단계에서 귀납 가설은 다음으로 작은 인덱스에 대한 재귀 호출이 배열의 길이를 변경하지 않는다는 것입니다. 고려해야 할 경우는 두 가지입니다. 하나는 원소가 정렬된 영역에 완전히 삽입되어 배열이 변경 없이 반환되는 경우로, 이때는 길이 또한 변경되지 않습니다. 다른 하나는 재귀 호출 전에 원소가 다음 원소와 교환되는 경우입니다. 그러나 배열에서 두 원소를 맞바꾸는 것은 배열의 크기를 변경하지 않으며, 귀납 가설은 다음 인덱스로 호출한 재귀 호출이 인자와 같은 크기의 배열을 반환한다고 명시합니다. 따라서 크기는 변하지 않습니다.
이 영어로 된 정리 문장을 Lean으로 번역하고 이 장에서 다룬 기법을 사용하여 진행하면 기저 사례를 증명하고 귀납 단계에서 진전을 이루기에 충분합니다.
theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
(insertSorted arr i).size = arr.size := α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.size⊢ (insertSorted arr i).size = arr.size
match i with
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizej:NatisLt:j < arr.size⊢ (insertSorted arr ⟨j, isLt⟩).size = arr.size
induction j with
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizeisLt:0 < arr.size⊢ (insertSorted arr ⟨0, isLt⟩).size = arr.size All goals completed! 🐙
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizej':Natih:∀ (isLt : j' < arr.size), (insertSorted arr ⟨j', isLt⟩).size = arr.sizeisLt:j' + 1 < arr.size⊢ (insertSorted arr ⟨j' + 1, isLt⟩).size = arr.size
귀납 단계에서 insertSorted를 사용한 단순화는 insertSorted에 있는 패턴 매칭을 드러냈습니다:
if 또는 match를 포함하는 목표(goal)와 마주쳤을 때, split 택틱(병합 정렬 정의에서 사용되는 splitList 함수와 혼동하지 않도록 주의하십시오)은 각 제어 흐름 경로마다 새로운 목표 하나씩으로 목표를 대체합니다:
theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
(insertSorted arr i).size = arr.size := α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.size⊢ (insertSorted arr i).size = arr.size
match i with
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizej:NatisLt:j < arr.size⊢ (insertSorted arr ⟨j, isLt⟩).size = arr.size
induction j with
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizeisLt:0 < arr.size⊢ (insertSorted arr ⟨0, isLt⟩).size = arr.size All goals completed! 🐙
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizej':Natih:∀ (isLt : j' < arr.size), (insertSorted arr ⟨j', isLt⟩).size = arr.sizeisLt:j' + 1 < arr.size⊢ (insertSorted arr ⟨j' + 1, isLt⟩).size = arr.size
어떤 명제가 어떻게 증명되었는지는 보통 중요하지 않고, 오직 증명되었다는 사실만이 중요하기 때문에, Lean의 출력에서 증명은 보통 ⋯로 대체됩니다. 또한 각 새 목표에는 어떤 분기가 그 목표로 이어졌는지를 나타내는 가정이 있으며, 이 경우에는 heq✝라는 이름이 붙습니다:
두 가지 단순한 경우 모두에 대해 증명을 작성하는 대신, split 뒤에 <;> try rfl을 추가하면 단순한 두 경우가 즉시 사라지고 다음과 같이 하나의 목표만 남게 됩니다:
theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
(insertSorted arr i).size = arr.size := α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.size⊢ (insertSorted arr i).size = arr.size
match i with
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizej:NatisLt:j < arr.size⊢ (insertSorted arr ⟨j, isLt⟩).size = arr.size
induction j with
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizeisLt:0 < arr.size⊢ (insertSorted arr ⟨0, isLt⟩).size = arr.size All goals completed! 🐙
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizej':Natih:∀ (isLt : j' < arr.size), (insertSorted arr ⟨j', isLt⟩).size = arr.sizeisLt:j' + 1 < arr.size⊢ (insertSorted arr ⟨j' + 1, isLt⟩).size = arr.size
안타깝게도 귀납 가설이 이 목표를 증명하기에는 충분히 강하지 않습니다. 귀납 가설은 arr에 대해 insertSorted를 호출해도 크기가 변하지 않는다고 말하지만, 증명 목표는 교환 결과에 재귀 호출을 적용해도 크기가 변하지 않음을 보이는 것입니다. 증명을 성공적으로 완료하려면, 더 작은 인덱스와 함께 인자로 insertSorted에 전달되는 어떤 배열에 대해서도 성립하는 귀납 가설이 필요합니다.
induction 택틱에 generalizing 옵션을 사용하면 더 강력한 귀납 가정을 얻을 수 있습니다. 이 옵션은 컨텍스트에 있는 추가 가정들을 기본 사례, 귀납 가설, 그리고 귀납 단계에서 보여야 할 목표를 생성하는 데 사용되는 명제 안으로 가져옵니다. arr에 대해 일반화하면 더 강한 가설로 이어집니다:
theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
(insertSorted arr i).size = arr.size := α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.size⊢ (insertSorted arr i).size = arr.size
match i with
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizej:NatisLt:j < arr.size⊢ (insertSorted arr ⟨j, isLt⟩).size = arr.size
induction j generalizing arr with
α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.sizeisLt:0 < arr.size⊢ (insertSorted arr ⟨0, isLt⟩).size = arr.size All goals completed! 🐙
α:Type u_1inst✝:Ord αj':Natih:∀ (arr : Array α) (i : Fin arr.size) (isLt : j' < arr.size), (insertSorted arr ⟨j', isLt⟩).size = arr.sizearr:Array αi:Fin arr.sizeisLt:j' + 1 < arr.size⊢ (insertSorted arr ⟨j' + 1, isLt⟩).size = arr.size
결과로 생성된 목표에서, arr은 이제 귀납 가설의 “모든 ~에 대해” 문장의 일부가 됩니다.
하지만 이 증명 전체가 점점 다루기 어려워지고 있습니다. 다음 단계는 교환 결과의 길이를 나타내는 변수를 도입하여 이 변수가 arr.size와 같음을 보이고, 그다음 이 변수가 재귀 호출 결과로 얻어지는 배열의 길이와도 같음을 보이는 것입니다. 이러한 등식 문장들은 연쇄적으로 연결되어 목표를 증명하는 데 사용될 수 있습니다. 하지만 함수적 귀납법을 사용하는 것이 훨씬 더 쉽습니다:
theorem insert_sorted_size_eq [Ord α]
(arr : Array α) (i : Fin arr.size) :
(insertSorted arr i).size = arr.size := α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.size⊢ (insertSorted arr i).size = arr.size
fun_induction insertSorted with
α:Type u_1inst✝:Ord αarr✝:Array αarr:Array αisLt✝:0 < arr.size⊢ arr.size = arr.size
α:Type u_1inst✝:Ord αarr✝:Array αarr:Array αi:Natthis:i + 1 < arr.sizeisLt:compare arr[i] arr[⟨i.succ, this⟩] = Ordering.lt⊢ (match compare arr[i] arr[⟨i.succ, this⟩] with
| Ordering.lt => arr
| Ordering.eq => arr
| Ordering.gt => insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size =
arr.size
α:Type u_1inst✝:Ord αarr✝:Array αarr:Array αi:Natthis:i + 1 < arr.sizeisEq:compare arr[i] arr[⟨i.succ, this⟩] = Ordering.eq⊢ (match compare arr[i] arr[⟨i.succ, this⟩] with
| Ordering.lt => arr
| Ordering.eq => arr
| Ordering.gt => insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size =
arr.size
α:Type u_1inst✝:Ord αarr✝:Array αarr:Array αi:Natthis:i + 1 < arr.sizeisGt:compare arr[i] arr[⟨i.succ, this⟩] = Ordering.gtih:(insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size = (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯).size⊢ (match compare arr[i] arr[⟨i.succ, this⟩] with
| Ordering.lt => arr
| Ordering.eq => arr
| Ordering.gt => insertSorted (arr.swap i ↑⟨i.succ, this⟩ ⋯ ⋯) ⟨i, ⋯⟩).size =
arr.size
첫 번째 목표는 인덱스 0에 대한 경우입니다. 여기서는 배열이 수정되지 않으므로, 배열의 크기가 변경되지 않았음을 증명하는 데 복잡한 단계가 필요하지 않습니다:
다음 두 목표는 동일하며, 원소 비교에서 .lt와 .eq 경우를 다룹니다. 로컬 가정 isLt와 isEq는 match의 올바른 분기가 선택되도록 해줍니다:
마지막 경우에서, match가 축약되고 나면 삽입의 다음 단계가 배열의 크기를 보존한다는 것을 증명하기 위해 해야 할 작업이 조금 남아 있습니다. 특히, 귀납 가설은 다음 단계의 크기가 교환 결과의 크기와 같다고 말하지만, 원하는 결론은 그것이 원래 배열의 크기와 같다는 것입니다:
grind 택틱은 네 가지 경우를 모두 처리할 수 있습니다:
theorem insert_sorted_size_eq [Ord α]
(arr : Array α) (i : Fin arr.size) :
(insertSorted arr i).size = arr.size := α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.size⊢ (insertSorted arr i).size = arr.size
α:Type u_1inst✝:Ord αarr:Array αarr✝:Array αisLt✝:0 < arr✝.size⊢ arr✝.size = arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.lt⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt => insertSorted (arr✝.swap i'✝ ↑⟨i'✝.succ, isLt✝⟩ ⋯ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.eq⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt => insertSorted (arr✝.swap i'✝ ↑⟨i'✝.succ, isLt✝⟩ ⋯ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.gtih1✝:(insertSorted (arr✝.swap i'✝ ↑⟨i'✝.succ, isLt✝⟩ ⋯ ⋯) ⟨i'✝, ⋯⟩).size = (arr✝.swap i'✝ ↑⟨i'✝.succ, isLt✝⟩ ⋯ ⋯).size⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt => insertSorted (arr✝.swap i'✝ ↑⟨i'✝.succ, isLt✝⟩ ⋯ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.size α:Type u_1inst✝:Ord αarr:Array αarr✝:Array αisLt✝:0 < arr✝.size⊢ arr✝.size = arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.lt⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt => insertSorted (arr✝.swap i'✝ ↑⟨i'✝.succ, isLt✝⟩ ⋯ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.eq⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt => insertSorted (arr✝.swap i'✝ ↑⟨i'✝.succ, isLt✝⟩ ⋯ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.gtih1✝:(insertSorted (arr✝.swap i'✝ ↑⟨i'✝.succ, isLt✝⟩ ⋯ ⋯) ⟨i'✝, ⋯⟩).size = (arr✝.swap i'✝ ↑⟨i'✝.succ, isLt✝⟩ ⋯ ⋯).size⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt => insertSorted (arr✝.swap i'✝ ↑⟨i'✝.succ, isLt✝⟩ ⋯ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.size All goals completed! 🐙
이제 이 증명을 사용하여 insertionSortLoop의 sorry를 대체할 수 있습니다. 특히, 이 정리는 grind가 성공할 수 있게 해 줍니다:
def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
if h : i < arr.size then
have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := α:Type ?u.3inst✝:Ord αarr:Array αi:Nath:i < arr.size⊢ (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i
All goals completed! 🐙
insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
else
arr
termination_by arr.size - i8.6.3. 드라이버 함수
삽입 정렬 자체는 insertionSortLoop을 호출하며, 배열에서 정렬된 영역과 정렬되지 않은 영역을 구분하는 인덱스를 0으로 초기화합니다:
def insertionSort [Ord α] (arr : Array α) : Array α :=
insertionSortLoop arr 0몇 가지 간단한 테스트를 해보면 이 함수가 적어도 명백히 잘못되지는 않았다는 것을 알 수 있습니다:
#eval insertionSort #[3, 1, 7, 4]#eval insertionSort #[ "quartz", "marble", "granite", "hematite"]8.6.4. 이것이 정말 삽입 정렬인가요?
삽입 정렬은 제자리(in-place) 정렬 알고리즘으로 정의됩니다. 최악의 경우 실행 시간이 이차 함수임에도 불구하고 이 알고리즘이 유용한 이유는, 추가 공간을 할당하지 않는 안정적인(stable) 정렬 알고리즘이면서 거의 정렬된 데이터를 효율적으로 처리하기 때문입니다. 내부 루프의 각 반복마다 새로운 배열을 할당한다면, 그 알고리즘은 실제로는 삽입 정렬이 아닐 것입니다.
Array.set와 Array.swap와 같은 Lean의 배열 연산은 해당 배열의 참조 횟수가 1보다 큰지 확인합니다. 만약 그렇다면, 해당 배열은 코드의 여러 부분에서 볼 수 있으므로 복사되어야 합니다. 그렇지 않다면 Lean은 더 이상 순수 함수형 언어가 아닐 것입니다. 그러나 참조 횟수가 정확히 1일 때는 해당 값을 관찰할 수 있는 다른 잠재적 주체가 존재하지 않습니다. 이러한 경우에는 배열 프리미티브가 배열을 제자리에서 변경합니다. 프로그램의 다른 부분이 모르는 것은 그 부분에 해를 끼칠 수 없습니다.
Lean의 증명 로직은 하부 구현이 아니라 순수 함수형 프로그램 수준에서 작동합니다. 이는 프로그램이 불필요하게 데이터를 복사하는지 알아내는 가장 좋은 방법이 직접 테스트해 보는 것임을 의미합니다. 변경이 필요한 각 지점에 dbgTraceIfShared 호출을 추가하면, 문제의 값이 두 개 이상의 참조를 가지고 있을 때 지정된 메시지가 stderr에 출력됩니다.
삽입 정렬에는 변경(mutating) 대신 복사가 일어날 위험이 있는 지점이 정확히 한 곳 있는데, 바로 Array.swap 호출입니다. arr.swap i' i를 (dbgTraceIfShared "array to swap" arr).swap i' i로 바꾸면 배열을 변경할 수 없을 때마다 프로그램이 shared RC array to swap을 출력하게 됩니다. 하지만 프로그램에 대한 이러한 변경은 증명 또한 변경시키는데, 이제 추가 함수에 대한 호출이 있기 때문입니다. dbgTraceIfShared가 자신의 인자의 길이를 보존한다는 지역 가정을 추가하고, 이를 몇몇 grind 호출에 추가하는 것만으로 프로그램과 증명을 고치기에 충분합니다.
삽입 정렬에 대한 완전한 계측 코드는 다음과 같습니다:
def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
match i with
| ⟨0, _⟩ => arr
| ⟨i' + 1, _⟩ =>
have : i' < arr.size := α:Type ?u.3inst✝:Ord αarr:Array αi:Fin arr.sizei':NatisLt✝:i' + 1 < arr.size⊢ i' < arr.size
All goals completed! 🐙
match Ord.compare arr[i'] arr[i] with
| .lt | .eq => arr
| .gt =>
have : (dbgTraceIfShared "array to swap" arr).size = arr.size := α:Type ?u.3inst✝:Ord αarr:Array αi:Fin arr.sizei':NatisLt✝:i' + 1 < arr.sizethis:i' < arr.size⊢ (dbgTraceIfShared "array to swap" arr).size = arr.size
All goals completed! 🐙
insertSorted
((dbgTraceIfShared "array to swap" arr).swap i' i)
⟨i', α:Type ?u.3inst✝:Ord αarr:Array αi:Fin arr.sizei':NatisLt✝:i' + 1 < arr.sizethis✝:i' < arr.sizethis:(dbgTraceIfShared "array to swap" arr).size = arr.size⊢ i' < ((dbgTraceIfShared "array to swap" arr).swap i' (↑i) this✝ ⋯).size All goals completed! 🐙⟩
theorem insert_sorted_size_eq [Ord α]
(arr : Array α) (i : Fin arr.size) :
(insertSorted arr i).size = arr.size := α:Type u_1inst✝:Ord αarr:Array αi:Fin arr.size⊢ (insertSorted arr i).size = arr.size
α:Type u_1inst✝:Ord αarr:Array αarr✝:Array αisLt✝:0 < arr✝.size⊢ arr✝.size = arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizethis✝:i'✝ < arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.lt⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt =>
have this := ⋯;
insertSorted ((dbgTraceIfShared "array to swap" arr✝).swap i'✝ (↑⟨i'✝.succ, isLt✝⟩) this✝ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizethis✝:i'✝ < arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.eq⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt =>
have this := ⋯;
insertSorted ((dbgTraceIfShared "array to swap" arr✝).swap i'✝ (↑⟨i'✝.succ, isLt✝⟩) this✝ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizethis✝¹:i'✝ < arr✝.sizethis✝:(dbgTraceIfShared "array to swap" arr✝).size = arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.gtih1✝:(insertSorted ((dbgTraceIfShared "array to swap" arr✝).swap i'✝ (↑⟨i'✝.succ, isLt✝⟩) this✝¹ ⋯) ⟨i'✝, ⋯⟩).size =
((dbgTraceIfShared "array to swap" arr✝).swap i'✝ (↑⟨i'✝.succ, isLt✝⟩) this✝¹ ⋯).size⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt =>
have this := ⋯;
insertSorted ((dbgTraceIfShared "array to swap" arr✝).swap i'✝ (↑⟨i'✝.succ, isLt✝⟩) this✝¹ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.size α:Type u_1inst✝:Ord αarr:Array αarr✝:Array αisLt✝:0 < arr✝.size⊢ arr✝.size = arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizethis✝:i'✝ < arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.lt⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt =>
have this := ⋯;
insertSorted ((dbgTraceIfShared "array to swap" arr✝).swap i'✝ (↑⟨i'✝.succ, isLt✝⟩) this✝ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizethis✝:i'✝ < arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.eq⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt =>
have this := ⋯;
insertSorted ((dbgTraceIfShared "array to swap" arr✝).swap i'✝ (↑⟨i'✝.succ, isLt✝⟩) this✝ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.sizeα:Type u_1inst✝:Ord αarr:Array αarr✝:Array αi'✝:NatisLt✝:i'✝ + 1 < arr✝.sizethis✝¹:i'✝ < arr✝.sizethis✝:(dbgTraceIfShared "array to swap" arr✝).size = arr✝.sizex✝:compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] = Ordering.gtih1✝:(insertSorted ((dbgTraceIfShared "array to swap" arr✝).swap i'✝ (↑⟨i'✝.succ, isLt✝⟩) this✝¹ ⋯) ⟨i'✝, ⋯⟩).size =
((dbgTraceIfShared "array to swap" arr✝).swap i'✝ (↑⟨i'✝.succ, isLt✝⟩) this✝¹ ⋯).size⊢ (match compare arr✝[i'✝] arr✝[⟨i'✝.succ, isLt✝⟩] with
| Ordering.lt => arr✝
| Ordering.eq => arr✝
| Ordering.gt =>
have this := ⋯;
insertSorted ((dbgTraceIfShared "array to swap" arr✝).swap i'✝ (↑⟨i'✝.succ, isLt✝⟩) this✝¹ ⋯) ⟨i'✝, ⋯⟩).size =
arr✝.size All goals completed! 🐙
def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
if h : i < arr.size then
have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := α:Type ?u.3inst✝:Ord αarr:Array αi:Nath:i < arr.size⊢ (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i
All goals completed! 🐙
insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
else
arr
termination_by arr.size - i
def insertionSort [Ord α] (arr : Array α) : Array α :=
insertionSortLoop arr 0
이 계측이 실제로 작동하는지 확인하려면 약간의 재치가 필요합니다. 우선, Lean 컴파일러는 함수 호출의 모든 인자가 컴파일 타임에 알려져 있는 경우 함수 호출을 적극적으로 최적화하여 제거합니다. insertionSort를 큰 배열에 적용하는 프로그램을 작성하는 것만으로는 충분하지 않은데, 컴파일된 결과 코드에 정렬된 배열만 상수로 포함될 수 있기 때문입니다. 컴파일러가 정렬 루틴을 최적화하여 제거하지 않도록 보장하는 가장 쉬운 방법은 stdin에서 배열을 읽어오는 것입니다. 둘째, 컴파일러는 죽은 코드 제거(dead code elimination)를 수행합니다. let을 프로그램에 추가로 넣는다고 해서 반드시 실행 중인 코드에서 참조가 더 많아지는 것은 아니며, let으로 바인딩된 변수가 전혀 사용되지 않는 경우에는 더욱 그렇습니다. 추가 참조가 완전히 제거되지 않도록 하려면, 추가 참조가 어떤 식으로든 사용되도록 하는 것이 중요합니다.
계측을 테스트하는 첫 번째 단계는 표준 입력에서 줄들의 배열을 읽어 들이는 getLines를 작성하는 것입니다:
def getLines : IO (Array String) := do
let stdin ← IO.getStdin
let mut lines : Array String := #[]
let mut currLine ← stdin.getLine
while !currLine.isEmpty do
-- Drop trailing newline:
lines := lines.push (currLine.dropEnd 1).copy
currLine ← stdin.getLine
pure lines
IO.FS.Stream.getLine은 줄 끝의 개행 문자를 포함하여 완전한 한 줄의 텍스트를 반환합니다. 파일 끝 표시(end-of-file marker)에 도달하면 ""를 반환합니다.
다음으로, 서로 다른 두 개의 main 루틴이 필요합니다. 두 코드 모두 정렬할 배열을 표준 입력에서 읽어들이며, 이를 통해 insertionSort 호출이 컴파일 시점에 반환값으로 대체되지 않도록 보장합니다. 그런 다음 두 코드 모두 콘솔에 출력하여, insertionSort 호출이 완전히 최적화되어 사라지지 않도록 보장합니다. 그중 하나는 정렬된 배열만 출력하고, 다른 하나는 정렬된 배열과 원래 배열을 모두 출력합니다. 두 번째 함수는 Array.swap이 새 배열을 할당해야 했다는 경고를 발생시켜야 합니다:
def mainUnique : IO Unit := do
let lines ← getLines
for line in insertionSort lines do
IO.println line
def : IO Unit := do
let lines ← getLines
IO.println "--- Sorted lines: ---"
for line in insertionSort lines do
IO.println line
IO.println ""
IO.println "--- Original data: ---"
for line in lines do
IO.println line
실제 main은 제공된 명령줄 인자에 따라 두 가지 주요 동작 중 하나를 단순히 선택합니다:
def main (args : List String) : IO UInt32 := do
match args with
| ["--shared"] => mainShared; pure 0
| ["--unique"] => mainUnique; pure 0
| _ =>
IO.println "Expected either \"--shared\" or \"--unique\""
pure 1인자 없이 실행하면 예상되는 사용법 정보가 출력됩니다:
sort
Expected either "--shared" or "--unique"
test-data 파일에는 다음과 같은 암석들이 들어 있습니다:
test-dataschistfeldspardioritepumiceobsidianshalegneissmarbleflint이 암석들에 계측된(instrumented) 삽입 정렬을 사용하면 알파벳 순서로 출력됩니다:
sort --unique < test-datadiorite
feldspar
flint
gneiss
marble
obsidian
pumice
schist
shale
하지만 원본 배열에 대한 참조가 유지되는 버전에서는 첫 번째 Array.swap 호출부터 stderr에 알림(즉, shared RC array to swap)이 출력되는 결과가 나타납니다:
sort --shared < test-data--- Sorted lines: ---
diorite
feldspar
flint
gneiss
marble
obsidian
pumice
schist
shale
--- Original data: ---
schist
feldspar
diorite
pumice
obsidian
shale
gneiss
marble
flint
shared RC array to swap
shared RC 알림이 단 한 번만 나타난다는 사실은 배열이 단 한 번만 복사됨을 의미합니다. 이는 Array.swap 호출로 생성된 사본 자체가 고유하므로, 추가로 복사할 필요가 없기 때문입니다. 명령형 언어에서는 배열을 참조로 전달하기 전에 명시적으로 복사하는 것을 잊으면 미묘한 버그가 발생할 수 있습니다. sort --shared를 실행할 때, 배열은 Lean 프로그램의 순수 함수형 의미를 보존하기 위해 필요한 만큼만 복사되며, 그 이상은 복사되지 않습니다.
8.6.5. 변경을 위한 다른 기회
참조가 유일할 때 복사 대신 변형을 사용하는 방식은 배열 갱신 연산자에만 한정되지 않습니다. Lean은 참조 횟수가 0으로 떨어지려는 생성자를 "재활용"하려고도 시도하여, 새 데이터를 할당하는 대신 이를 재사용합니다. 예를 들어, 이는 List.map이 아무도 알아챌 수 없는 경우에 한해서는 연결 리스트를 제자리에서 변경한다는 것을 의미합니다. Lean 코드에서 핫 루프를 최적화하는 데 있어 가장 중요한 단계 중 하나는 수정 중인 데이터가 여러 위치에서 참조되지 않도록 하는 것입니다.
8.6.6. 연습문제
-
배열을 뒤집는 함수를 작성하십시오. 입력 배열의 참조 카운트가 1인 경우, 해당 함수가 새로운 배열을 할당하지 않는지 테스트하십시오.
-
배열에 대해 병합 정렬 또는 퀵 정렬을 구현하십시오. 여러분의 구현이 종료함을 증명하고, 예상보다 더 많은 배열을 할당하지 않는지 테스트하십시오. 이는 도전적인 연습 문제입니다!