8.1. 패턴 매칭🔗

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

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

이 함수들을 정의하는 데 사용된 등식은 정의에 의해 성립합니다:

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

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

패턴 매칭은 곱 타입이나 옵션 타입 같은 모든 귀납적 타입에 사용할 수 있습니다:

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

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

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

이 모든 예제에서 패턴 매칭은 경우를 한 번만 나누는 데 사용되었습니다. 더 흥미로운 점은, 다음 예제에서처럼 패턴에 중첩된 생성자를 사용할 수 있다는 것입니다.

등식 컴파일러는 먼저 입력이 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에 알려 줄 수 있으며, 다른 방식으로 구성된 타입에도 원소가 존재한다는 것을 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. 구조적 재귀와 귀납법🔗

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

• 구조적 재귀 정의

• 정초 재귀 정의

• 상호 재귀 정의

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

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(이는 succ (succ n)과 정의적으로 같습니다)에서의 fib 함수의 값은 n + 1(이는 succ n과 정의적으로 동치입니다)에서의 값과 n에서의 값의 항으로 정의됩니다. 그러나 이는 피보나치 함수를 계산하는 방법으로서는 비효율적이기로 악명이 높으며, 실행 시간이 n에 대해 지수적으로 증가합니다. 더 나은 방법은 다음과 같습니다:

573147844013817084101

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

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

구조적 재귀를 처리하기 위해 등식 컴파일러는 값 경과 재귀를 사용하며, 이때 각 귀납적으로 정의된 타입과 함께 자동으로 생성되는 상수 below와 brecOn을 사용합니다. 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의 원소로 주어지는 그 함수의 이전 모든 값들에 대한 항으로 정의할 수 있습니다.

값 경과 재귀를 사용하는 것은 등식 컴파일러가 함수가 종료된다는 것을 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. 정초 재귀와 귀납법🔗

구조적 재귀를 사용할 수 없을 때에는 정초 재귀(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는 접근 가능합니다. 임의의 타입 α가 주어지면, α의 접근 가능한 각 원소에 대해 그 모든 선행자에 먼저 값을 할당하는 방식으로 재귀적으로 값을 할당할 수 있어야 합니다.

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

여기에는 등장하는 요소가 많지만, 첫 번째 묶음은 이미 살펴본 것입니다. 타입 α, 관계 r, 그리고 r이 정초적(well-founded)이라는 가정 h입니다. 변수 C는 재귀 정의의 동기(motive)를 나타냅니다. 즉, 각 원소 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가 성립함을 보이는 것으로 충분하다는 뜻입니다.

위 예제에서는 현재 코드 생성기가 WellFounded.fix를 지원하지 않기 때문에 noncomputable 수식어를 사용합니다. 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

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

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

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

div의 정의 방정식은 정의적으로 성립하지 않지만, unfold 택틱을 사용하여 div를 펼칠 수 있습니다. conv를 사용하여 펼치려는 div 적용을 선택합니다.