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를 사용하여 새로운 데이터 타입을 만들 수 있는 것처럼, 새로운 명제도 만들 수 있습니다. 인자를 받는 명제는 술어라고 부르며, 술어는 가능한 인자 중 일부에 대해서는 참이지만 모든 인자에 대해 참이지는 않을 수 있습니다. 여러 개의 인자를 받는 명제는 관계라고 부릅니다.
귀납적으로 정의된 명제의 각 생성자는 그 명제를 증명하는 하나의 방법입니다. 다시 말해, 명제의 선언은 그 명제가 참임을 보여 주는 여러 형태의 증거를 기술합니다. 인자가 없고 생성자가 하나뿐인 명제는 증명하기가 상당히 쉬울 수 있습니다:
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 생성자를 Nat.le.step의 인스턴스 d개로 감싼 것으로 이루어집니다. 각 step 생성자는 자신의 인덱스 인자에 1을 더하므로, step 생성자 d개는 더 큰 수에 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. 종료 증명
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이 받아들이도록 추가 증명이 필요하기도 합니다.