8.6. Insertion Sort and Array Mutation
삽입 정렬은 정렬 알고리즘으로서 최적의 최악 시간 복잡도를 갖지는 않지만, 여전히 유용한 성질이 많다.
-
구현하고 이해하기가 간단하고 직관적이다.
-
제자리 알고리즘이므로 실행에 추가 공간이 필요하지 않다.
-
안정 정렬이다.
-
입력이 이미 거의 정렬되어 있으면 빠르다.
제자리 알고리즘은 Lean의 메모리 관리 방식 때문에 특히 유용하다. 어떤 경우에는 원래 배열을 복사할 연산을 변이 연산으로 최적화할 수 있다. 배열 원소 교환도 여기에 포함된다.
JavaScript, JVM, .NET을 비롯한 자동 메모리 관리 언어와 런타임 시스템 대부분은 추적 가비지 컬렉션을 사용한다. 메모리를 회수해야 할 때 시스템은 호출 스택과 전역 값 같은 여러 루트에서 시작해 포인터를 재귀적으로 따라가 도달할 수 있는 값을 판별한다. 도달할 수 없는 값은 모두 할당 해제되어 메모리가 해제된다.
참조 횟수 세기는 추적 가비지 컬렉션의 대안이며 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. The Inner Loop
삽입 정렬의 안쪽 루프는 배열과 삽입할 원소의 인덱스를 인자로 받는 꼬리 재귀 함수로 구현할 수 있다.
삽입할 원소는 왼쪽 원소가 더 작아지거나 배열의 시작에 도달할 때까지 왼쪽 원소와 반복해서 교환한다.
안쪽 루프는 배열 인덱싱에 사용하는 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. The Outer Loop
삽입 정렬의 바깥 루프는 포인터를 왼쪽에서 오른쪽으로 옮기며 매 반복에 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. Termination
이번에도 처리 중인 배열의 크기와 인덱스의 차이가 각 재귀 호출에서 감소하므로 함수가 종료한다.
그러나 이번에는 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가 포함된 목표를 만나면 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. The Driver Function
삽입 정렬 자체는 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. Is This Really Insertion Sort?
삽입 정렬은 정의상 제자리 정렬 알고리즘이다. 최악 실행 시간이 이차적임에도 유용한 이유는 안정 정렬이고 추가 공간을 할당하지 않으며 거의 정렬된 데이터를 효율적으로 처리하기 때문이다. 안쪽 루프의 각 반복이 새 배열을 할당한다면 그 알고리즘은 진정한 삽입 정렬이 아니다.
Array.set과 Array.swap 같은 Lean의 배열 연산은 해당 배열의 참조 횟수가 1보다 큰지 검사한다.
그렇다면 배열이 코드의 여러 부분에 보이므로 복사해야 한다.
그렇지 않으면 Lean은 더 이상 순수 함수형 언어가 아니다.
반면 참조 횟수가 정확히 1이면 값을 볼 수 있는 다른 주체가 없다.
이 경우 배열 기본 연산은 배열을 제자리에서 변이한다.
프로그램의 다른 부분이 모르는 것은 그 부분에 해를 끼치지 않는다.
Lean의 증명 논리는 실제 구현이 아니라 순수 함수형 프로그램 수준에서 작동한다.
따라서 프로그램이 불필요하게 데이터를 복사하는지 알아보는 가장 좋은 방법은 시험하는 것이다.
변이를 원하는 각 지점에 dbgTraceIfShared 호출을 추가하면 해당 값의 참조가 둘 이상일 때 주어진 메시지가 stderr에 출력된다.
삽입 정렬에서 변이 대신 복사할 위험이 있는 곳은 정확히 하나, 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에서 배열을 읽는 것이다.
둘째, 컴파일러는 죽은 코드 제거를 수행한다.
프로그램에 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
-- 뒤따르는 줄바꿈을 제거한다:
lines := lines.push (currLine.dropEnd 1).copy
currLine ← stdin.getLine
pure lines
IO.FS.Stream.getLine은 뒤따르는 줄바꿈을 포함한 완전한 텍스트 한 줄을 반환한다.
파일 끝 표시에 도달하면 ""을 반환한다.
다음으로 별도의 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이 암석에 계측된 삽입 정렬을 적용하면 알파벳순으로 출력된다.
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. Other Opportunities for Mutation
참조가 유일할 때 복사 대신 변이를 사용하는 것은 배열 갱신 연산자에만 국한되지 않는다.
Lean은 참조 횟수가 곧 0이 될 생성자를 “재활용”해 새 데이터를 할당하는 대신 재사용하려고도 한다.
예를 들어 아무도 알아차릴 수 없는 경우에는 List.map이 연결 리스트를 제자리에서 변이한다.
Lean 코드의 자주 실행되는 루프를 최적화할 때 가장 중요한 단계 중 하나는 수정하는 데이터를 여러 위치에서 참조하지 않는지 확인하는 것이다.
8.6.6. Exercises
-
배열을 뒤집는 함수를 작성하라. 입력 배열의 참조 횟수가 1일 때 새 배열을 할당하지 않는지 시험하라.
-
배열에 병합 정렬 또는 퀵 정렬을 구현하라. 구현이 종료함을 증명하고 예상보다 많은 배열을 할당하지 않는지 시험하라. 어려운 연습문제다!