8.1. 패턴 매칭🔗

스키마 패턴의 해석은 컴파일 과정의 첫 단계입니다. 귀납적으로 정의된 타입에 관련된 생성자에 따라, casesOn 재귀자를 사용하여 함수를 정의하고 경우를 나누어 정리를 증명할 수 있음을 살펴보았습니다. 하지만 복잡한 정의는 여러 개의 중첩된 casesOn 적용을 사용할 수 있으며, 읽고 이해하기 어려울 수 있습니다. 패턴 매칭은 더 편리하고, 함수형 프로그래밍 언어 사용자에게 익숙한 접근 방식을 제공합니다.

귀납적으로 정의된 자연수 타입을 생각해 봅시다. 모든 자연수는 zero 이거나 succ x 이므로, 각 경우에 대한 값을 지정함으로써 자연수에서 임의의 타입으로 가는 함수를 정의할 수 있습니다.

이 함수들을 정의하는 데 사용된 방정식들은 정의적으로 성립합니다:

zero와 succ 대신, 더 익숙한 표기법을 사용할 수 있습니다:

덧셈과 0 표기법에는 [match_pattern] 속성이 부여되어 있으므로, 이들은 패턴 매칭에 사용될 수 있습니다. Lean은 생성자 zero와 succ가 드러날 때까지 이러한 표현식을 단순히 정규화합니다.

패턴 매칭은 곱 타입이나 option 타입과 같이 모든 귀납적 타입에서 작동합니다:

여기서는 이를 함수를 정의하는 데 사용할 뿐만 아니라, 경우를 나누는 증명을 수행하는 데에도 사용합니다:

패턴 매칭은 귀납적으로 정의된 명제를 해체하는 데에도 사용할 수 있습니다:

이는 논리 결합자를 사용하는 가정을 간결하게 풀어내는 방법을 제공합니다.

이 모든 예시에서, 패턴 매칭은 단일한 경우 구분을 수행하는 데 사용되었습니다. 더 흥미로운 점은, 다음 예시들에서처럼 패턴이 중첩된 생성자를 포함할 수 있다는 것입니다.

방정식 컴파일러는 먼저 입력이 zero인지 succ x 형태인지에 따라 경우를 나눕니다. 그런 다음 x가 zero 형태인지 succ x 형태인지에 따라 경우 분할을 수행합니다. 컴파일러는 제시된 패턴들로부터 필요한 경우 분할을 결정하며, 패턴이 모든 경우를 다 포괄하지 못하면 오류를 발생시킵니다. 이번에도 아래 버전에서처럼 산술 표기법을 사용할 수 있습니다. 두 경우 모두 정의 방정식은 정의적으로 성립합니다.

def sub2 : Nat → Nat := fun x => match x with | 0 => 0 | 1 => 0 | x.succ.succ => x#print sub2를 작성하면 이 함수가 어떻게 재귀자로 컴파일되었는지 확인할 수 있습니다. (Lean은 sub2가 내부 보조 함수인 sub2.match_1을 통해 정의되었다고 알려주는데, 이 함수 역시 출력해 볼 수 있습니다.) Lean은 이러한 보조 함수를 사용하여 match 표현식을 컴파일합니다. 사실 위의 정의는 다음과 같이 확장됩니다

다음은 중첩된 패턴 매칭의 몇 가지 추가 예시입니다:

방정식 컴파일러는 여러 인자를 순차적으로 처리할 수 있습니다. 예를 들어, 이전 예제를 두 개의 인자를 받는 함수로 정의하는 것이 더 자연스러울 것입니다.

또 다른 예를 살펴보겠습니다:

패턴은 쉼표로 구분된다는 점에 유의하십시오.

다음 각 예제에서, 나머지 인자들도 패턴 목록에 포함되어 있지만, 분할은 첫 번째 인자에 대해서만 일어납니다.

또한 정의에서 인자의 값이 필요하지 않을 때는 밑줄을 대신 사용할 수 있다는 점에 유의하십시오. 이 밑줄은 와일드카드 패턴, 또는 익명 변수라고 알려져 있습니다. 방정식 컴파일러 밖에서의 사용과 달리, 여기서 밑줄은 암시적 인자를 나타내지 않습니다. 와일드카드를 위해 밑줄을 사용하는 것은 함수형 프로그래밍 언어에서 흔한 일이며, Lean도 그 표기법을 채택하고 있습니다. 와일드카드와 겹치는 패턴에 관한 절에서는 와일드카드의 개념을 더 자세히 다루며, 접근할 수 없는 패턴에 대한 설명에서는 패턴에서도 암시적 인자를 사용하는 방법을 설명합니다.

귀납적 타입에서 설명한 대로, 귀납적 데이터 타입은 매개변수에 의존할 수 있습니다. 다음 예제는 패턴 매칭을 사용하여 tail 함수를 정의합니다. 인자 α : Type u는 매개변수이며, 패턴 매칭에 참여하지 않음을 나타내기 위해 콜론 앞에 위치합니다. Lean은 매개변수가 : 뒤에 오는 것도 허용하지만, 그 경우 패턴 매칭을 하려면 명시적인 match가 필요합니다.

이 두 예제에서 매개변수 α의 배치는 다르지만, 두 경우 모두 케이스 분할에 관여하지 않는다는 점에서 동일한 방식으로 처리됩니다.

Lean은 더 복잡한 형태의 패턴 매칭도 처리할 수 있는데, 이러한 경우에는 의존 타입의 인자가 각 경우에 추가적인 제약을 가합니다. 이러한 의존 패턴 매칭의 예시는 의존 패턴 매칭 절에서 다룹니다.

8.2. 와일드카드와 중복 패턴🔗

이전 절의 예제 중 하나를 살펴봅시다:

대안적인 표현은 다음과 같습니다:

두 번째 표현에서는 패턴이 겹칩니다. 예를 들어 인자 쌍 0, 0은 세 경우 모두와 매칭됩니다. 하지만 Lean은 적용 가능한 첫 번째 방정식을 사용하여 이 모호함을 처리하므로, 이 예제에서 최종 결과는 동일합니다. 특히 다음 방정식들은 정의적으로 성립합니다:

m과 n의 값이 필요하지 않으므로, 와일드카드 패턴을 대신 사용해도 무방합니다.

foo의 이 정의가 이전과 동일한 정의적 항등성을 만족한다는 것을 확인할 수 있습니다.

일부 함수형 프로그래밍 언어는 불완전한 패턴을 지원합니다. 이러한 언어에서는 인터프리터가 불완전한 경우에 대해 예외를 발생시키거나 임의의 값을 반환합니다. Inhabited 타입 클래스를 사용하여 임의의 값을 반환하는 방식을 흉내 낼 수 있습니다. 대략적으로 말하면, Inhabited α의 원소는 α에 원소가 존재한다는 사실의 증거입니다. 타입 클래스에 관한 장에서 보게 되겠지만, Lean에게 적절한 기본 타입에 원소가 있음을 알려줄 수 있고, 다른 구성된 타입에 원소가 있음을 자동으로 추론하게 할 수도 있습니다. 이를 바탕으로, 표준 라이브러리는 원소가 있는 모든 타입에 대해 기본 원소인 default를 제공합니다.

Option α 타입을 사용하여 불완전한 패턴을 시뮬레이션할 수도 있습니다. 아이디어는 제공된 패턴에 대해서는 some a를 반환하고, 불완전한 경우에는 none을 사용하는 것입니다. 다음 예제는 두 방식을 모두 보여 줍니다.

이퀘이션 컴파일러는 영리합니다. 다음 정의에서 케이스 중 하나라도 빠뜨리면, 오류 메시지가 무엇이 다루어지지 않았는지 알려줄 것입니다.

또한 적절한 상황에서는 casesOn 대신 if ... then ... else를 사용합니다.

@[instance_reducible] def foo.match_1.{u_1} : (motive : Char → Sort u_1) →
  (x : Char) → (Unit → motive 'A') → (Unit → motive 'B') → ((x : Char) → motive x) → motive x :=
fun motive x h_1 h_2 h_3 =>
  dite (x = 'A') (Eq.ndrec_symm (h_1 ())) fun h_1 => dite (x = 'B') (Eq.ndrec_symm (h_2 ())) fun h_2 => h_3 x

8.3. 구조적 재귀와 귀납법🔗

방정식 컴파일러를 강력하게 만드는 것은 재귀적 정의도 지원한다는 점입니다. 다음 세 절에서는 각각 다음을 설명합니다:

• 구조적 재귀 정의

• 정초된(well-founded) 재귀적 정의

• 상호 재귀적 정의

일반적으로 방정식 컴파일러는 다음과 같은 형태의 입력을 처리합니다.

def foo (a : α) : (b : β) → γ
  | [patterns₁] => t₁
  ...
  | [patternsₙ] => tₙ

여기서 (a : α)는 매개변수들의 나열이고, (b : β)는 패턴 매칭이 이루어지는 인자들의 나열이며, γ는 a와 b에 의존할 수 있는 임의의 타입입니다. 각 줄은 β의 각 원소마다 하나씩, 동일한 개수의 패턴을 포함해야 합니다. 지금까지 살펴보았듯이, 패턴은 변수이거나, 다른 패턴들에 적용된 생성자이거나, 혹은 그러한 형태로 정규화되는 식(이때 생성자가 아닌 것은 [match_pattern] 속성으로 표시됩니다)입니다. 생성자의 출현은 경우 분리를 유발하며, 생성자에 대한 인자는 주어진 변수로 표현됩니다. 의존 패턴 매칭에 관한 절에서, 패턴 매칭에서 아무런 역할을 하지 않음에도 불구하고 식이 타입 검사를 통과하도록 만들기 위해 패턴 안의 일부 명시적 항이 특정한 형태로 강제되는 것을 보게 될 것입니다. 바로 이런 이유로 이러한 것들을 “접근 불가능한 패턴”이라고 부릅니다. 하지만 의존 패턴 매칭을 다루기 전까지는 이러한 접근 불가능한 패턴을 사용할 필요가 없을 것입니다.

지난 절에서 살펴보았듯이, 항 t₁, ..., tₙ은 매개변수 a 중 어느 것이든, 그리고 해당 패턴에서 도입된 변수 중 어느 것이든 사용할 수 있습니다. 재귀와 귀납법을 가능하게 하는 것은 이들이 foo에 대한 재귀 호출도 포함할 수 있다는 점입니다. 이 절에서는 구조적 재귀를 다룰 것인데, 이는 =>의 오른쪽에 나타나는 foo의 인자들이 왼쪽 패턴들의 부분항인 경우입니다. 그 발상은 이들이 구조적으로 더 작으므로 귀납적 타입에서 더 이른 단계에 나타난다는 것입니다. 다음은 지난 장에서 다룬 구조적 재귀의 예시들로, 이제 등식 컴파일러를 사용하여 정의된 것입니다:

zero_add의 증명을 보면 귀납법에 의한 증명이 실제로는 Lean에서 재귀의 한 형태임이 분명해집니다.

위의 예시는 add의 정의 방정식이 정의적으로 성립함을 보여주며, mul도 마찬가지입니다. 방정식 컴파일러는 단순한 구조적 귀납법의 경우처럼, 가능한 한 이것이 성립하도록 보장하고자 합니다. 그러나 다른 상황에서는 축소가 오직 명제적으로만 성립하는데, 이는 곧 명시적으로 적용해야 하는 방정식 정리라는 뜻입니다. 방정식 컴파일러는 이러한 정리를 내부적으로 생성합니다. 이는 사용자가 직접 사용하도록 의도된 것이 아니며, 대신 simp 택틱이 필요할 때 이를 사용하도록 설정되어 있습니다. zero_add의 다음 증명이 이러한 방식으로 작동합니다.

패턴 매칭에 의한 정의와 마찬가지로, 구조적 재귀나 귀납법에 대한 매개변수는 콜론 앞에 나타날 수 있습니다. 이러한 매개변수는 정의가 처리되기 전에 단순히 지역 컨텍스트에 추가됩니다. 예를 들어, 덧셈의 정의는 다음과 같이 작성될 수도 있습니다.

위의 예제는 match를 사용해서 작성할 수도 있습니다.

구조적 재귀의 더 흥미로운 예시는 피보나치 함수 fib에서 볼 수 있습니다.

여기서 n + 2에서의 fib 함수 값(이는 succ (succ n)과 정의적으로 같습니다)은 n + 1에서의 값(이는 succ n과 정의적으로 동등합니다)과 n에서의 값을 이용하여 정의됩니다. 그러나 이는 피보나치 함수를 계산하는 데 있어 악명 높게 비효율적인 방법으로, 실행 시간이 n에 대해 지수적으로 증가합니다. 더 나은 방법은 다음과 같습니다:

573147844013817084101

다음은 where 대신 let rec을 사용한 동일한 정의입니다.

두 경우 모두, Lean은 보조 함수 fibFast.loop를 생성합니다.

구조적 재귀를 처리하기 위해, 방정식 컴파일러는 각 귀납적으로 정의된 타입마다 자동으로 생성되는 상수 below와 brecOn을 사용하여 course-of-values 재귀를 사용합니다. Nat.below와 Nat.brecOn의 타입을 살펴보면 이것이 어떻게 작동하는지 감을 잡을 수 있습니다:

Nat.below : Nat → Type u

Nat.below 3

Nat.brecOn : (t : Nat) → ((t : Nat) → Nat.below t → C t) → C t

@Nat.below C (3 : Nat) 타입은 C 0, C 1, C 2의 원소들을 저장하는 데이터 구조입니다. 코스-오브-밸류 재귀(course-of-values recursion)는 Nat.brecOn에 의해 구현됩니다. 이를 통해 (n : Nat) → C n 타입의 의존 함수의 값을 특정 입력 n에 대해, @Nat.below C n의 원소로 표현되는 함수의 모든 이전 값들을 이용해 정의할 수 있습니다.

코스-오브-밸류즈 재귀(course-of-values recursion)의 사용은 방정식 컴파일러가 Lean 커널에게 함수가 종료됨을 정당화하기 위해 사용하는 기법 중 하나입니다. 이는 다른 함수형 프로그래밍 언어 컴파일러와 마찬가지로 재귀 함수를 컴파일하는 코드 생성기에는 영향을 미치지 않습니다. #eval fib <n>이 <n>에 대해 지수적임을 상기하십시오. 반면, #reduce fib <n>은 brecOn 구성에 기반하여 커널로 전송된 정의를 사용하기 때문에 효율적입니다.

20365011074

def fib : Nat → Nat :=
fun x => Nat.brecOn x fib._f

재귀적 정의의 또 다른 좋은 예시는 리스트 append 함수입니다.

또 다른 예시가 있습니다: 이 함수는 두 목록 중 하나가 소진될 때까지 첫 번째 목록의 원소와 두 번째 목록의 원소를 더합니다.

[5, 7, 9]

아래 연습 문제에서 유사한 예제들을 직접 실험해 보시기를 권장합니다.

8.4. 지역 재귀 선언🔗

let rec 키워드를 사용하여 지역 재귀적 선언을 정의할 수 있습니다.

@replicate.loop : {α : Type u_1} → α → Nat → List α → List α

Lean은 각 let rec에 대해 보조 선언을 생성합니다. 위 예제에서는 replicate에서 나타나는 let rec loop에 대해 replicate.loop 선언을 생성했습니다. 참고로, Lean은 let rec 선언 안에 나타나는 지역 변수를 추가 매개변수로 덧붙여 해당 선언을 “닫습니다”. 예를 들어, 지역 변수 a는 let rec loop에서 나타납니다.

택틱 모드와 귀납법을 통한 증명을 작성할 때도 let rec을 사용할 수 있습니다.

정의 뒤에 where 절을 사용하여 보조 재귀 선언을 도입할 수도 있습니다. Lean은 이를 let rec으로 변환합니다.

8.5. 정초 재귀법과 귀납법🔗

구조적 재귀법을 사용할 수 없는 경우, 정지성(termination)을 정초 재귀법(well-founded recursion)을 사용하여 증명할 수 있습니다. 정초 관계(well-founded relation)와 각 재귀 호출이 이 관계에 대해 감소함을 보이는 증명이 필요합니다. 의존 타입 이론은 정초 재귀법을 인코딩하고 정당화하기에 충분히 강력합니다. 정초 재귀법이 어떻게 작동하는지 이해하는 데 필요한 논리적 배경부터 시작합시다.

Lean의 표준 라이브러리는 두 가지 술어인 Acc r a와 WellFounded r을 정의하는데, 여기서 r은 타입 α에 대한 이항 관계이고, a는 타입 α의 원소입니다.

Acc r : α → Prop

WellFounded r : Prop

첫 번째인 Acc는 귀납적으로 정의된 술어입니다. 그 정의에 따르면, Acc r x는 ∀ y, r y x → Acc r y와 동치입니다. r y x를 일종의 순서 관계 y ≺ x를 나타내는 것으로 생각한다면, Acc r x는 모든 선행자가 접근 가능하다는 의미에서 x가 아래로부터 접근 가능하다는 것을 말합니다. 특히, x에 선행 원소가 없다면 그것은 접근 가능합니다. 임의의 타입 α가 주어졌을 때, 우리는 모든 선행 원소에 먼저 값을 할당함으로써 재귀적으로 α의 각 접근 가능한 원소에 값을 할당할 수 있어야 합니다.

r이 정초적(well-founded)이라는 명제, 즉 WellFounded r로 표기되는 명제는, 정확히 해당 타입의 모든 원소가 접근 가능하다는 명제입니다. 위의 고찰에 따르면, r이 타입 α에 대한 정초적 관계라면, 관계 r에 대해 α에 대한 정초적 재귀의 원리가 존재해야 합니다. 그리고 실제로 그러합니다: 표준 라이브러리는 정확히 그러한 목적을 위해 WellFounded.fix를 정의합니다.

여기에는 등장하는 요소가 많지만, 첫 번째 묶음은 이미 살펴본 바 있습니다: 타입 α, 관계 r, 그리고 r이 정초적임을 나타내는 가정 h입니다. 변수 C는 재귀적 정의의 동기를 나타냅니다: 각 원소 x : α에 대해, C x의 원소를 구성하고자 합니다. 함수 F는 이를 위한 귀납적 방법을 제공합니다: x의 각 선행 원소 y에 대한 C y의 원소들이 주어졌을 때, C x의 원소를 어떻게 구성하는지 알려줍니다.

WellFounded.fix가 귀납법 원리로서도 동일하게 작동한다는 점에 유의하십시오. 이는 ≺가 정초적(well-founded)이고 ∀ x, C x를 증명하고자 할 때, 임의의 x에 대해 ∀ y, r y x → C y가 성립한다고 가정하면 C x가 성립함을 보이는 것으로 충분하다는 것을 의미합니다.

위 예제에서 noncomputable 수식어를 사용한 이유는 코드 생성기가 현재 WellFounded.fix를 지원하지 않기 때문입니다. WellFounded.fix 함수는 Lean이 함수의 종료를 정당화하는 데 사용하는 또 다른 도구입니다.

Lean은 자연수에 대한 일반적인 순서 <가 정초적(well founded)임을 알고 있습니다. 또한 Lean은 사전식 순서를 사용하는 것과 같이, 기존의 정초적 순서로부터 새로운 정초적 순서를 구성하는 여러 방법도 알고 있습니다.

다음은 표준 라이브러리에서 찾을 수 있는 자연수 나눗셈 정의를 본질적으로 담은 것입니다.

이 정의는 다소 이해하기 어렵습니다. 여기서 재귀는 x에 대해 이루어지며, div.F x f : Nat → Nat는 그 고정된 x에 대해 “y로 나누기” 함수를 반환합니다. div.F의 두 번째 인자, 즉 재귀를 위한 레시피는 x보다 작은 모든 값 x₁에 대해 y로 나누기 함수를 반환해야 하는 함수라는 점을 기억해야 합니다.

읽기 어렵다는 점 외에도, div에 대한 이 정의는 div 8 2가 4와 정의적으로 같아지도록 이끌지 않습니다.

Tactic `rfl` failed: The left-hand side
  div 8 2
is not definitionally equal to the right-hand side
  4

⊢ div 8 2 = 4

대신, 이 방정식은 명제적으로만 성립하며, 접근 가능한 관계에 관한 표준 라이브러리 정리를 사용하여 증명해야 합니다:

정교화기는 이와 같은 정의를 더 편리하게 만들도록 설계되었습니다. 다음을 받아들입니다.

Lean이 재귀적 정의를 만나면, 먼저 구조적 재귀를 시도하고, 그것이 실패할 때만 정초 재귀(well-founded recursion)로 대체합니다. Lean은 재귀적 적용이 더 작다는 것을 보이기 위해 택틱 decreasing_tactic을 사용합니다. 위 예제의 보조 명제 x - y < x는 이 택틱을 위한 힌트로 간주되어야 합니다. 정교화기는 또한 재귀적 정의에 대한 일련의 등식 보조정리들을 증명하여, 접근 가능한 관계에 대한 저수준 보조정리에 의존하지 않고도 이를 다룰 수 있게 합니다.

div에 대한 정의 방정식은 정의적으로 성립하지 않지만, unfold 택틱을 사용하여 div를 펼칠 수 있습니다. 어떤 div 적용을 펼칠지 선택하기 위해 conv를 사용합니다.