8.3. Arrays and Termination
효율적인 코드를 작성하려면 적절한 자료구조를 선택하는 것이 중요하다. 연결 리스트가 유용한 경우도 있다. 어떤 응용에서는 리스트의 꼬리를 공유하는 능력이 매우 중요하다. 그러나 길이가 변하는 순차 데이터 컬렉션의 대부분의 사용 사례에는 배열이 더 적합하다. 배열은 메모리 오버헤드가 더 작고 지역성도 더 좋다.
그러나 배열에는 리스트에 비해 두 가지 단점이 있다.
-
배열은 패턴 매칭이 아니라 인덱싱으로 접근하므로 안전성을 유지하려면 증명 의무가 생긴다.
-
배열 전체를 왼쪽에서 오른쪽으로 처리하는 루프는 꼬리 재귀 함수이지만, 호출마다 감소하는 인자를 갖지 않는다.
배열을 효과적으로 사용하려면 배열 인덱스가 범위 안에 있음을 Lean에 증명하는 방법과, 배열 크기에 가까워지는 배열 인덱스가 프로그램을 종료하게 함을 증명하는 방법을 알아야 한다. 이 두 가지는 모두 명제적 동등성이 아니라 부등식 명제로 표현한다.
8.3.1. Inequality
타입마다 순서의 개념이 다르므로 부등식은 LE와 LT라는 두 타입 클래스로 다룬다.
표준 타입 클래스 절의 표는 이 클래스들이 구문과 어떻게 연결되는지 설명한다.
표현식 | 구문 해석 | 클래스 이름 |
|---|---|---|
|
| |
|
| |
|
| |
|
|
다시 말해 타입은 < 및 ≤ 연산자의 의미를 사용자 정의할 수 있고, > 및 ≥는 < 및 ≤에서 의미를 이끌어 낸다.
LT와 LE 클래스의 메서드는 Bool이 아니라 명제를 반환한다.
class LE (α : Type u) where
le : α → α → Prop
class LT (α : Type u) where
lt : α → α → Prop
Nat에 대한 LE 인스턴스는 Nat.le에 처리를 위임한다.
instance : LE Nat where
le := Nat.le
Nat.le을 정의하려면 아직 소개하지 않은 Lean의 기능이 필요하다. 이는 귀납적으로 정의된 관계다.
8.3.1.1. Inductively-Defined Propositions, Predicates, and Relations
Nat.le은 귀납적으로 정의된 관계다.
inductive로 새 데이터 타입을 만들 수 있듯이 새 명제도 만들 수 있다.
명제가 인자를 받으면 가능한 인자 중 일부에 대해서는 참일 수 있지만 모두에 대해서는 그렇지 않을 수 있는 술어라고 한다.
여러 인자를 받는 명제를 관계라고 한다.
귀납적으로 정의된 명제의 각 생성자는 그 명제를 증명하는 방법이다. 다시 말해 명제의 선언은 명제가 참이라는 여러 형태의 증거를 기술한다. 인자가 없고 생성자가 하나인 명제는 매우 쉽게 증명할 수 있다.
inductive EasyToProve : Prop where
| heresTheProof : EasyToProve증명은 그 생성자를 사용하는 것으로 이루어진다.
theorem fairlyEasy : EasyToProve := ⊢ EasyToProve
All goals completed! 🐙
실제로 항상 쉽게 증명할 수 있어야 하는 명제 True도 EasyToProve와 같은 방식으로 정의되어 있다.
inductive True : Prop where
| intro : True
인자를 받지 않는 귀납적으로 정의된 명제는 귀납적으로 정의된 데이터 타입만큼 흥미롭지 않다.
데이터는 그 자체로 흥미롭기 때문이다. 자연수 3은 35와 다르며, 피자 3개를 주문한 사람의 집에 30분 뒤 35개가 도착하면 당황할 것이다.
명제의 생성자는 명제가 참일 수 있는 방법을 기술하지만, 명제를 증명하고 나면 어떤 생성자를 사용했는지는 알 필요가 없다.
그래서 Prop 유니버스의 흥미로운 귀납 타입 대부분은 인자를 받는다.
귀납적으로 정의된 술어 IsThree는 인자가 3이라고 말한다.
inductive IsThree : Nat → Prop where
| isThree : IsThree 3
여기서 사용한 메커니즘은 HasCol 같은 인덱스 패밀리와 같지만, 결과 타입이 사용할 수 있는 데이터가 아니라 증명할 수 있는 명제라는 점이 다르다.
이 술어를 사용하면 3이 실제로 3임을 증명할 수 있다.
theorem three_is_three : IsThree 3 := ⊢ IsThree 3
All goals completed! 🐙
마찬가지로 IsFive는 인자가 5라고 말하는 술어다.
inductive IsFive : Nat → Prop where
| isFive : IsFive 5어떤 수가 3이면 거기에 2를 더한 결과는 5여야 한다. 이를 정리의 명제로 표현할 수 있다.
theorem three_plus_two_five : IsThree n → IsFive (n + 2) := n:Nat⊢ IsThree n → IsFive (n + 2)
n:Nat⊢ IsThree n → IsFive (n + 2)그 결과 나온 목표는 함수 타입이다.
따라서 intro 전술을 사용해 인자를 가정으로 바꿀 수 있다.
theorem three_plus_two_five : IsThree n → IsFive (n + 2) := n:Nat⊢ IsThree n → IsFive (n + 2)
n:Natthree:IsThree n⊢ IsFive (n + 2)
n이 3이라는 가정이 있으므로 IsFive의 생성자를 사용해 증명을 완성할 수 있을 것 같다.
theorem three_plus_two_five : IsThree n → IsFive (n + 2) := n:Nat⊢ IsThree n → IsFive (n + 2)
n:Natthree:IsThree n⊢ IsFive (n + 2)
n:Natthree:IsThree n⊢ IsFive (n + 2)그러나 이렇게 하면 오류가 발생한다.
이 오류는 n + 2가 5와 정의적으로 동등하지 않기 때문에 발생한다.
일반 함수 정의에서는 가정 three에 종속 패턴 매칭을 적용해 n을 3으로 정제할 수 있다.
종속 패턴 매칭에 해당하는 전술은 cases이며, induction과 비슷한 구문을 사용한다.
theorem three_plus_two_five : IsThree n → IsFive (n + 2) := n:Nat⊢ IsThree n → IsFive (n + 2)
n:Natthree:IsThree n⊢ IsFive (n + 2)
cases three with
⊢ IsFive (3 + 2)
남은 경우에는 n이 3으로 정제되었다.
3 + 2가 5와 정의적으로 동등하므로 이제 생성자를 적용할 수 있다.
theorem three_plus_two_five : IsThree n → IsFive (n + 2) := n:Nat⊢ IsThree n → IsFive (n + 2)
n:Natthree:IsThree n⊢ IsFive (n + 2)
cases three with
⊢ IsFive (3 + 2) All goals completed! 🐙
표준 거짓 명제 False에는 생성자가 없으므로 직접 증거를 제공할 수 없다.
False의 증거를 제공하는 유일한 방법은 가정 자체가 불가능한 경우다. 이는 타입 시스템이 도달 불가능하다고 판단하는 코드를 nomatch로 표시하는 방식과 비슷하다.
증명에 관한 첫 막간에서 설명했듯이 부정 Not A는 A → False의 줄임말이다.
Not A는 ¬A로도 쓸 수 있다.
4가 3인 것은 아니다.
theorem four_is_not_three : ¬ IsThree 4 := ⊢ ¬IsThree 4
⊢ ¬IsThree 4
처음 증명 목표에는 Not이 들어 있다.
실제로 함수 타입이라는 사실은 unfold로 드러낼 수 있다.
theorem four_is_not_three : ¬ IsThree 4 := ⊢ ¬IsThree 4
⊢ IsThree 4 → False
목표가 함수 타입이므로 intro를 사용해 인자를 가정으로 바꿀 수 있다.
unfold를 계속 사용할 필요는 없다. intro가 Not의 정의 자체를 펼칠 수 있기 때문이다.
theorem four_is_not_three : ¬ IsThree 4 := ⊢ ¬IsThree 4
h:IsThree 4⊢ False
이 증명에서는 cases 전술이 즉시 목표를 해결한다.
theorem four_is_not_three : ¬ IsThree 4 := ⊢ ¬IsThree 4
h:IsThree 4⊢ False
All goals completed! 🐙
Vect String 2에 패턴 매칭할 때 Vect.nil 경우를 넣을 필요가 없는 것처럼, IsThree 4에 대한 cases 증명에도 isThree 경우를 넣을 필요가 없다.
8.3.1.2. Inequality of Natural Numbers
Nat.le의 정의에는 매개변수와 인덱스가 있다.
inductive Nat.le (n : Nat) : Nat → Prop
| refl : Nat.le n n
| step : Nat.le n m → Nat.le n (m + 1)
매개변수 n은 더 작아야 하는 수이고, 인덱스는 n 이상이어야 하는 수다.
두 수가 같을 때는 refl 생성자를 사용하고, 인덱스가 n보다 클 때는 step 생성자를 사용한다.
증명의 관점에서 n \leq k의 증명은 n + d = k가 되도록 어떤 수 d를 찾는 것이다.
Lean에서 증명은 Nat.le.refl 생성자를 d개의 Nat.le.step으로 감싼 형태다.
각 step 생성자는 인덱스 인자에 1을 더하므로 d개의 step 생성자는 큰 수에 d를 더한다.
예를 들어 4가 7 이하라는 증거는 refl을 세 개의 step으로 감싼 것이다.
theorem four_le_seven : 4 ≤ 7 :=
open Nat.le in
step (step (step refl))엄격한 미만 관계는 왼쪽 수에 1을 더해 정의한다.
def Nat.lt (n m : Nat) : Prop :=
Nat.le (n + 1) m
instance : LT Nat where
lt := Nat.lt
4가 7보다 엄격히 작다는 증거는 refl을 두 개의 step으로 감싼 것이다.
theorem four_lt_seven : 4 < 7 :=
open Nat.le in
step (step refl)
이는 4 < 7이 5 ≤ 7과 동등하기 때문이다.
8.3.2. Proving Termination
Array.map 함수는 함수로 배열을 변환하고, 입력 배열의 각 원소에 함수를 적용한 결과를 담은 새 배열을 반환한다.
이를 꼬리 재귀 함수로 작성할 때는 출력 배열을 누산기로 전달하는 함수에 위임하는 일반적인 패턴을 따른다.
누산기는 빈 배열로 초기화한다.
누산기를 전달하는 도우미 함수는 배열의 현재 인덱스를 추적하는 인자도 받으며, 이 인덱스는 0에서 시작한다.
def Array.map (f : α → β) (arr : Array α) : Array β :=
arrayMapHelper f arr Array.empty 0
도우미 함수는 매 반복에서 인덱스가 여전히 범위 안에 있는지 검사해야 한다.
범위 안에 있으면 변환한 원소를 누산기 끝에 추가하고 인덱스를 1 증가시켜 다시 반복해야 한다.
그렇지 않으면 종료하고 누산기를 반환해야 한다.
이 코드의 초기 구현은 배열 인덱스가 유효함을 Lean이 증명하지 못하므로 실패한다.
def arrayMapHelper (f : α → β) (arr : Array α)
(soFar : Array β) (i : Nat) : Array β :=
if i < arr.size then
arrayMapHelper f arr (soFar.push (f arr[i])) (i + 1)
else soFar
그러나 조건 표현식은 배열 인덱스의 유효성에 필요한 정확한 조건, 즉 i < arr.size를 이미 검사한다.
if에 이름을 붙이면 배열 인덱싱 전술이 사용할 수 있는 가정이 추가되므로 문제가 해결된다.
def arrayMapHelper (f : α → β) (arr : Array α)
(soFar : Array β) (i : Nat) : Array β :=
if inBounds : i < arr.size then
arrayMapHelper f arr (soFar.push (f arr[i])) (i + 1)
else soFar재귀 호출이 입력 생성자의 인자 중 하나에 대해 이루어지지 않는데도 Lean은 수정된 프로그램을 받아들인다. 실제로 누산기와 인덱스는 줄어들지 않고 모두 커진다.
내부적으로 Lean의 증명 자동화가 종료 증명을 구성한다. 이 증명을 다시 구성해 보면 Lean이 자동으로 인식하지 못하는 경우를 더 쉽게 이해할 수 있다.
arrayMapHelper는 왜 종료하는가?
매 반복에서 인덱스 i가 배열 arr의 범위 안에 있는지 검사한다.
범위 안에 있으면 i를 증가시키고 루프를 반복한다.
그렇지 않으면 프로그램이 종료한다.
arr.size는 유한한 수이므로 i도 유한한 횟수만 증가할 수 있다.
호출마다 함수의 인자가 감소하지 않더라도 arr.size - i는 0을 향해 감소한다.
각 재귀 호출에서 감소하는 값을 측정값(measure)이라고 한다.
정의 끝에 termination_by 절을 제공하면 Lean에게 특정 표현식을 종료 측정값으로 사용하라고 지시할 수 있다.
arrayMapHelper의 명시적 측정값은 다음과 같다.
def arrayMapHelper (f : α → β) (arr : Array α)
(soFar : Array β) (i : Nat) : Array β :=
if inBounds : i < arr.size then
arrayMapHelper f arr (soFar.push (f arr[i])) (i + 1)
else soFar
termination_by arr.size - i
비슷한 종료 증명을 사용해 Array.find를 작성할 수 있다. 이 함수는 불리언 함수를 만족하는 배열의 첫 원소를 찾아 원소와 인덱스를 함께 반환한다.
def Array.find (arr : Array α) (p : α → Bool) :
Option (Nat × α) :=
findHelper arr p 0
이번에도 i가 증가할 때 arr.size - i가 감소하므로 도우미 함수가 종료한다.
def findHelper (arr : Array α) (p : α → Bool)
(i : Nat) : Option (Nat × α) :=
if h : i < arr.size then
let x := arr[i]
if p x then
some (i, x)
else findHelper arr p (i + 1)
else none
termination_by에 물음표를 추가해 termination_by?로 쓰면 Lean이 선택한 측정값을 명시적으로 제안한다.
[apply]를 클릭하면 termination_by?가 제안된 측정값으로 바뀐다.
def findHelper (arr : Array α) (p : α → Bool)
(i : Nat) : Option (Nat × α) :=
if h : i < arr.size then
let x := arr[i]
if p x then
some (i, x)
else findHelper arr p (i + 1)
else none
termination_by?모든 종료 논증이 이만큼 간단한 것은 아니다. 그러나 함수의 인자를 바탕으로 호출마다 감소할 표현식을 식별한다는 기본 구조는 모든 종료 증명에 나타난다. 때로는 함수가 왜 종료하는지 알아내기 위해 창의성이 필요하고, 때로는 측정값이 실제로 감소한다는 것을 받아들이도록 Lean에 추가 증명을 제공해야 한다.