8.3. 배열과 종료
효율적인 코드를 작성하려면 적절한 자료 구조를 선택하는 것이 중요합니다. 연결 리스트도 나름의 쓰임새가 있습니다. 일부 응용에서는 리스트의 꼬리 부분을 공유할 수 있는 능력이 매우 중요합니다. 그러나 가변 길이의 순차적 데이터 컬렉션에 대한 대부분의 사용 사례는 배열을 사용하는 편이 더 낫습니다. 배열은 메모리 오버헤드가 더 적고 지역성도 더 우수합니다.
하지만 배열은 리스트에 비해 두 가지 단점이 있습니다:
-
배열은 패턴 매칭이 아니라 인덱싱을 통해 접근하며, 이는 안전성을 유지하기 위해 증명 의무를 부과합니다.
-
배열 전체를 왼쪽에서 오른쪽으로 처리하는 루프는 꼬리 재귀 함수이지만, 호출할 때마다 감소하는 인자를 가지지는 않습니다.
배열을 효과적으로 사용하려면 배열 인덱스가 범위 내에 있음을 Lean에 증명하는 방법과, 배열 크기에 근접하는 배열 인덱스가 프로그램을 종료시키기도 한다는 것을 증명하는 방법을 알아야 합니다. 이 둘은 모두 명제적 동등성이 아니라 부등식 명제를 사용하여 표현됩니다.
8.3.1. 부등식
서로 다른 타입은 서로 다른 순서 개념을 가지므로, 부등호는 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. 귀납적으로 정의된 명제, 술어, 관계
Nat.le는 귀납적으로 정의된 관계입니다. inductive를 사용해 새로운 데이터 타입을 만들 수 있는 것처럼, 이를 사용해 새로운 명제를 만들 수도 있습니다. 명제가 인자를 받으면 이를 predicate(술어)라고 부르며, 이는 잠재적 인자들 중 일부에 대해서는 참일 수 있지만 전부에 대해서는 참이 아닐 수도 있습니다. 여러 인자를 받는 명제를 관계라고 합니다.
귀납적으로 정의된 명제의 각 생성자는 이를 증명하는 하나의 방법입니다. 다시 말해, 명제의 선언은 그것이 참임을 나타내는 서로 다른 형태의 증거들을 기술합니다. 생성자가 하나이고 인자가 없는 명제는 증명하기가 상당히 쉬울 수 있습니다:
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를 사용하여 인자를 가정으로 변환할 수 있습니다. intro가 Not 자체의 정의를 펼칠 수 있으므로, unfold를 유지할 필요가 없습니다:
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에 대한 경우 분석 증명도 isThree에 대한 경우를 포함할 필요가 없습니다.
8.3.1.2. 자연수의 부등식
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 생성자는 두 수가 같을 때 사용되며, step 생성자는 인덱스가 n보다 클 때 사용됩니다.
증거의 관점에서, n \leq k라는 증명은 n + d = m을 만족하는 어떤 수 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))엄격한 미만(strict less-than) 관계는 왼쪽 숫자에 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. 종료성 증명
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을 향해 감소합니다.
각 재귀 호출마다 감소하는 값을 측정값이라고 부릅니다. 정의 끝에 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이 추가적인 증명을 요구하기도 합니다.