8.6. 삽입 정렬과 배열 변경
삽입 정렬은 정렬 알고리즘으로서 최적의 최악 시간 복잡도를 갖지는 않지만, 그래도 여러 가지 유용한 성질을 갖습니다.
-
구현하기도 이해하기도 간단하고 명료합니다
-
이 알고리즘은 실행에 추가 공간이 필요하지 않은 제자리(in-place) 알고리즘입니다
-
이는 안정 정렬입니다
-
입력이 이미 거의 정렬되어 있으면 빠릅니다
제자리(in-place) 알고리즘은 Lean이 메모리를 관리하는 방식 덕분에 Lean에서 특히 유용합니다. 경우에 따라서는 보통 배열을 복사하게 되는 연산이 변경(mutation)으로 최적화될 수 있습니다. 배열의 원소를 서로 맞바꾸는 연산도 여기에 포함됩니다.
JavaScript, JVM, .NET을 비롯해 자동 메모리 관리 기능을 갖춘 대부분의 언어와 런타임 시스템은 추적 가비지 컬렉션(tracing garbage collection)을 사용합니다. 메모리를 회수해야 할 때 시스템은 여러 루트(호출 스택과 전역 값 등)에서 출발하여 포인터를 재귀적으로 따라가면서 어떤 값에 도달할 수 있는지 판별합니다. 도달할 수 없는 값은 모두 할당 해제되고, 그만큼 메모리가 확보됩니다.
참조 카운팅은 추적 방식 가비지 컬렉션의 대안으로, 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가 포함된 목표를 마주했을 때, 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보다 큰지를 확인합니다. 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에서 배열을 읽어 들이는 것입니다. 둘째로, 컴파일러는 죽은 코드 제거(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은 끝의 줄바꿈을 포함하여 텍스트 한 줄 전체를 반환합니다. 파일 끝 표시에 도달하면 ""을 반환합니다.
다음으로, 서로 별개인 두 개의 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. 변경 가능성을 활용할 수 있는 다른 경우
참조가 유일할 때 복사 대신 변경을 사용하는 방식은 배열 갱신 연산자에만 국한되지 않습니다. Lean은 또한 참조 카운트가 곧 0으로 떨어질 생성자를 “재활용”하려고 시도하며, 새 데이터를 할당하는 대신 해당 생성자를 재사용합니다. 예를 들어 이는 적어도 아무도 알아챌 수 없는 경우에는 List.map이 연결 리스트를 제자리에서 변경한다는 뜻입니다. Lean 코드에서 핫 루프를 최적화할 때 가장 중요한 단계 중 하나는 수정되는 데이터가 여러 위치에서 참조되지 않도록 하는 것입니다.
8.6.6. 연습 문제
-
배열을 뒤집는 함수를 작성하십시오. 입력 배열의 참조 카운트가 1이면 함수가 새 배열을 할당하지 않는지 테스트하십시오.
-
배열에 대한 병합 정렬이나 퀵 정렬 중 하나를 구현하십시오. 구현이 종료됨을 증명하고, 예상보다 많은 배열을 할당하지 않는지 테스트하십시오. 이것은 꽤 어려운 연습 문제입니다!