Lean으로 배우는 함수형 프로그래밍

막간: 명제, 증명, 인덱싱🔗

많은 언어와 마찬가지로 Lean은 배열과 리스트의 인덱싱에 대괄호를 사용합니다. 예를 들어 woodlandCritters가 다음과 같이 정의되어 있다고 합시다:

def woodlandCritters : List String := ["hedgehog", "deer", "snail"]

그러면 개별 구성 요소를 꺼낼 수 있습니다:

def hedgehog := woodlandCritters[0] def deer := woodlandCritters[1] def snail := woodlandCritters[2]

하지만 네 번째 원소를 추출하려고 하면 런타임 오류가 아니라 컴파일 타임 오류가 발생합니다:

def oops := failed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid ⊢ 3 < woodlandCritters.lengthwoodlandCritters[3]
failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ 3 < woodlandCritters.length

이 오류 메시지는 Lean이 3 < woodlandCritters.length(즉, 3 < List.length woodlandCritters)를 자동으로 수학적으로 증명하려 했지만 증명하지 못했다는 뜻입니다. 이것이 증명되었다면 이 조회가 안전하다는 의미였을 것입니다. 범위 초과 오류는 흔한 유형의 버그이며, Lean은 프로그래밍 언어이자 정리 증명기라는 이중적 성격을 활용하여 이러한 오류를 가능한 한 많이 배제합니다.

이것이 어떻게 동작하는지 이해하려면 명제, 증명, 택틱이라는 세 가지 핵심 개념을 이해해야 합니다.

명제와 증명🔗

명제는 참이거나 거짓일 수 있는 진술입니다. 다음 영어 문장은 모두 명제입니다:

  • 1 + 1 = 2

  • 덧셈은 교환 법칙을 만족합니다.

  • 소수는 무한히 많습니다.

  • 1 + 1 = 15

  • 파리는 프랑스의 수도입니다.

  • 부에노스아이레스는 대한민국의 수도입니다.

  • 모든 새는 날 수 있습니다.

반면에 무의미한 진술은 명제가 아닙니다. 다음 문장들은 문법적으로는 올바르지만, 어느 것도 명제가 아닙니다:

  • 1 + 초록 = 아이스크림

  • 모든 수도는 소수입니다.

  • 적어도 하나의 gorg는 fleep입니다.

명제에는 두 가지 종류가 있습니다. 하나는 개념에 대한 우리의 정의에만 의존하는 순수하게 수학적인 명제이고, 다른 하나는 세계에 관한 사실인 명제입니다. Lean과 같은 정리 증명기는 전자의 범주를 다루며, 펭귄의 비행 능력이나 도시의 법적 지위에 대해서는 아무것도 말하지 않습니다.

증명은 명제가 참이라는 것을 납득시키는 인자입니다. 수학적 명제의 경우, 이러한 인자는 관련된 개념의 정의뿐만 아니라 논리적 인자 전개의 규칙도 활용합니다. 대부분의 증명은 사람이 이해할 수 있도록 작성되며, 지루한 세부 사항을 많이 생략합니다. Lean과 같은 컴퓨터 보조 정리 증명기는 수학자가 많은 세부 사항을 생략한 채 증명을 작성할 수 있도록 설계되었으며, 누락된 명시적 단계를 채워 넣는 일은 소프트웨어가 책임집니다. 이러한 단계는 기계적으로 검사할 수 있습니다. 이를 통해 간과나 실수가 발생할 가능성이 줄어듭니다.

Lean에서 프로그램의 타입은 그 프로그램과 상호작용할 수 있는 방식을 기술합니다. 예를 들어, Nat → List String 타입의 프로그램은 Nat 인자를 받아 문자열 리스트를 만들어 내는 함수입니다. 다시 말해, 각 타입은 무엇을 그 타입의 프로그램으로 인정하는지를 규정합니다.

Lean에서 명제는 사실 타입입니다. 명제는 해당 진술이 참이라는 증거로 무엇이 인정되는지를 규정합니다. 명제는 이 증거를 제시함으로써 증명되며, 그 증거는 Lean이 검사합니다. 반면에 명제가 거짓이라면 이러한 증거를 구성하는 것은 불가능합니다.

예를 들어, 명제 1 + 1 = 2는 Lean에서 직접 작성할 수 있습니다. 이 명제의 증거는 생성자 rfl이며, 이는 reflexivity(반사성)의 줄임말입니다. 수학에서 관계는 모든 원소가 자기 자신과 관계되어 있을 때 반사적이라고 합니다. 이는 합리적인 동등성 개념을 갖추기 위한 기본 요건입니다. 1 + 1은 2로 계산되므로, 둘은 실제로 같은 것입니다:

Definition `onePlusOneIsTwo` is a proposition; use `theorem` instead of `def` Note: This linter can be disabled with `set_option linter.defProp false`def onePlusOneIsTwo : 1 + 1 = 2 := rfl

반면에 rfl은 거짓 명제 1 + 1 = 15를 증명하지 못합니다:

def Not a definitional equality: the left-hand side 1 + 1 is not definitionally equal to the right-hand side 15onePlusOneIsFifteen : 1 + 1 = 15 := Type mismatch rfl has type ?m.16 = ?m.16 but is expected to have type 1 + 1 = 15rfl
Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  1 + 1 = 15

이 오류 메시지는 등식 명제의 양변이 이미 같은 수일 때 rfl이 두 표현식이 같음을 증명할 수 있음을 나타냅니다. 1 + 1은 곧바로 2로 평가되므로 둘은 같은 것으로 간주되며, 그 덕분에 onePlusOneIsTwo가 받아들여집니다. Type이 자료 구조와 함수를 나타내는 Nat, String, List (Nat × String × (Int → Float)) 같은 타입을 기술하듯이, Prop은 명제를 기술합니다.

명제가 증명되면 이를 정리라고 합니다. Lean에서는 정리를 선언할 때 def 대신 theorem 키워드를 사용하는 것이 관례입니다. 이렇게 하면 어떤 선언이 수학적 증명으로 읽히도록 의도되었고 어떤 선언이 정의인지 독자가 쉽게 구분할 수 있습니다. 일반적으로 증명에서 중요한 것은 명제가 참이라는 근거가 존재한다는 사실이며, 어떤 근거가 제시되었는지는 그다지 중요하지 않습니다. 반면 정의에서는 구체적으로 어떤 값이 선택되는지가 매우 중요합니다. 항상 0을 반환하는 덧셈의 정의는 분명히 잘못된 것이기 때문입니다. 증명의 세부 사항은 이후의 증명에서 중요하지 않으므로, theorem 키워드를 사용하면 Lean 컴파일러가 더 많은 작업을 병렬로 처리할 수 있습니다.

앞의 예제는 다음과 같이 다시 작성할 수 있습니다:

def OnePlusOneIsTwo : Prop := 1 + 1 = 2 theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl

택틱🔗

증명은 보통 증거를 직접 제시하기보다는 택틱을 사용하여 작성합니다. 택틱은 명제에 대한 증거를 구성하는 작은 프로그램입니다. 이러한 프로그램은 증명 상태에서 실행되며, 증명 상태는 증명해야 할 명제(목표라고 합니다)와 이를 증명하는 데 사용할 수 있는 가정을 함께 추적합니다. 목표에 택틱을 실행하면 새로운 목표를 포함하는 새로운 증명 상태가 만들어집니다. 모든 목표가 증명되면 증명이 완료됩니다.

택틱으로 증명을 작성하려면 정의를 by로 시작하십시오. by를 쓰면 Lean은 다음 들여쓰기 블록이 끝날 때까지 택틱 모드로 전환됩니다. 택틱 모드에 있는 동안 Lean은 현재 증명 상태에 대한 피드백을 계속 제공합니다. 택틱으로 작성해도 onePlusOneIsTwo는 여전히 꽤 짧습니다:

theorem onePlusOneIsTwo : 1 + 1 = 2 := ⊢ 1 + 1 = 2 All goals completed! 🐙

decide 택틱은 결정 절차를 호출합니다. 결정 절차는 어떤 명제가 참인지 거짓인지 검사할 수 있는 프로그램이며, 어느 경우든 그에 맞는 증명을 반환합니다. 이 택틱은 주로 1이나 2처럼 구체적인 값을 다룰 때 사용합니다. 이 책에서 다루는 그 밖의 중요한 택틱으로는 “simplify”의 줄임말인 simp와 많은 정리를 자동으로 증명할 수 있는 grind가 있습니다.

택틱은 여러 가지 이유로 유용합니다:

  1. 많은 증명은 아주 작은 세부 사항까지 모두 적으면 복잡하고 지루해지는데, 택틱을 사용하면 이런 흥미롭지 않은 부분을 자동화할 수 있습니다.

  2. 택틱으로 작성한 증명은 유연한 자동화가 정의의 사소한 변경을 흡수해 줄 수 있기 때문에 시간이 지나도 유지보수하기가 더 쉽습니다.

  3. 하나의 택틱으로 여러 가지 정리를 증명할 수 있기 때문에, Lean은 보이지 않는 곳에서 택틱을 사용하여 사용자가 증명을 직접 작성하지 않아도 되게 할 수 있습니다. 예를 들어, 배열 조회에는 인덱스가 범위 안에 있다는 증명이 필요한데, 보통은 택틱이 그 증명을 구성할 수 있으므로 사용자가 이를 신경 쓸 필요가 없습니다.

내부적으로 인덱싱 표기법은 택틱을 사용하여 사용자의 조회 연산이 안전함을 증명합니다. 이 택틱은 산술에 관한 여러 사실을 고려하며, 이를 지역적으로 알려진 사실들과 결합하여 인덱스가 범위 안에 있음을 증명하려고 시도합니다.

simp 택틱은 Lean 증명에서 가장 많이 쓰이는 핵심 도구입니다. 이 택틱은 목표를 가능한 한 단순한 형태로 다시 씁니다. 많은 경우 이렇게 다시 쓰면 명제가 매우 단순해져서 자동으로 증명될 수 있습니다. 내부적으로는 상세한 형식적 증명이 구성되지만, simp를 사용하면 이러한 복잡함이 드러나지 않습니다.

decide와 마찬가지로 grind 택틱은 증명을 마무리하는 데 사용됩니다. 이 택틱은 SMT 솔버에서 가져온 여러 기법을 활용하여 매우 다양한 정리를 증명할 수 있습니다. simp와 달리 grind는 증명을 완전히 끝내지 않고서는 증명을 조금도 진척시킬 수 없습니다. 즉, 완전히 성공하거나 실패하거나 둘 중 하나입니다. grind 택틱은 매우 강력하며 사용자 정의와 확장이 가능합니다. 이러한 강력함과 유연성 때문에, 정리 증명에 실패했을 때의 출력에는 숙련된 Lean 사용자가 실패 원인을 진단하는 데 도움이 되는 정보가 많이 담겨 있습니다. 처음에는 이 정보가 부담스러울 수 있으므로, 이 장에서는 decide와 simp만 사용합니다.

논리 연결사🔗

“그리고”, “또는”, “참”, “거짓”, “아님”과 같은 논리의 기본 구성 요소를 논리 연결사라고 합니다. 각 연결사는 무엇이 그 연결사가 참이라는 증거로 인정되는지를 정의합니다. 예를 들어, “A 그리고 B”라는 진술을 증명하려면 A와 B를 모두 증명해야 합니다. 이는 “A 그리고 B”에 대한 증거가 A에 대한 증거와 B에 대한 증거를 모두 담고 있는 쌍이라는 뜻입니다. 마찬가지로, “A 또는 B”에 대한 증거는 A에 대한 증거나 B에 대한 증거 중 하나로 이루어집니다.

특히 이러한 연결사 대부분은 데이터 타입처럼 정의되며, 생성자를 가지고 있습니다. A와 B가 명제라면, “A 그리고 B”(A ∧ B로 표기합니다)도 명제입니다. A ∧ B에 대한 증거는 생성자 And.intro로 이루어지며, 이 생성자의 타입은 A → B → A ∧ B입니다. A와 B를 구체적인 명제로 바꾸면, And.intro rfl rfl로 1 + 1 = 2 ∧ "Str".append "ing" = "String"을 증명할 수 있습니다. 물론 decide도 이 증명을 찾아낼 만큼 충분히 강력합니다:

theorem addAndAppend : 1 + 1 = 2 ∧ "Str".append "ing" = "String" := ⊢ 1 + 1 = 2 ∧ "Str".append "ing" = "String" All goals completed! 🐙

마찬가지로 “A 또는 B”(A ∨ B로 씁니다)에는 생성자가 두 개 있습니다. “A 또는 B”를 증명하려면 두 기저 명제 중 하나만 참이면 되기 때문입니다. 생성자는 두 개입니다. 타입이 A → A ∨ B인 Or.inl과 타입이 B → A ∨ B인 Or.inr입니다.

함의(만약 A이면 B)는 함수를 사용하여 표현됩니다. 특히, A에 대한 증거를 B에 대한 증거로 변환하는 함수는 그 자체로 A가 B를 함의한다는 증거입니다. 이는 A → B를 ¬A ∨ B의 약칭으로 보는 일반적인 함의 설명과는 다르지만, 두 정식화는 동치입니다.

"그리고"에 대한 증거는 생성자이므로 패턴 매칭에 사용할 수 있습니다. 예를 들어, A 그리고 B가 A 또는 B를 함의한다는 증명은, A 그리고 B에 대한 증거에서 A의 증거(또는 B의 증거)를 꺼낸 다음, 이 증거를 사용하여 A 또는 B의 증거를 만들어 내는 함수입니다:

theorem andImpliesOr : A ∧ B → A ∨ B := fun andEvidence => match andEvidence with | And.intro a b => Or.inl a

연결사

Lean 문법

증거

True

True

True.intro : True

False

False

증거 없음

A와 B

A ∧ B

And.intro : A → B → A ∧ B

A 또는 B

A ∨ B

Or.inl : A → A ∨ B 또는 Or.inr : B → A ∨ B 중 하나

A는 B를 함의합니다

A → B

A의 증거를 B의 증거로 변환하는 함수

A가 아님

¬A

A의 증거를 False의 증거로 변환하는 함수

decide 택틱은 이러한 연결사를 사용하는 정리를 증명할 수 있습니다. 예를 들면 다음과 같습니다.

theorem onePlusOneOrLessThan : 1 + 1 = 2 ∨ 3 < 5 := ⊢ 1 + 1 = 2 ∨ 3 < 5 All goals completed! 🐙 theorem notTwoEqualFive : ¬(1 + 1 = 5) := ⊢ ¬1 + 1 = 5 All goals completed! 🐙 theorem trueIsTrue : True := ⊢ True All goals completed! 🐙 theorem trueOrFalse : True ∨ False := ⊢ True ∨ False All goals completed! 🐙 theorem falseImpliesTrue : False → True := ⊢ False → True All goals completed! 🐙

인자로서의 증거🔗

어떤 경우에는 리스트를 안전하게 인덱싱하려면 리스트가 일정한 최소 크기를 가져야 하지만, 리스트 자체는 구체적인 값이 아니라 변수입니다. 이 조회가 안전하려면 리스트가 충분히 길다는 증거가 있어야 합니다. 인덱싱을 안전하게 만드는 가장 쉬운 방법 중 하나는 자료 구조에서 조회를 수행하는 함수가 안전성에 필요한 증거를 인자로 받도록 하는 것입니다. 예를 들어, 리스트의 세 번째 항목을 반환하는 함수는 일반적으로 안전하지 않습니다. 리스트에는 항목이 0개, 1개 또는 2개만 들어 있을 수도 있기 때문입니다:

def third (xs : List α) : α := failed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid α:Type ?u.3xs:List α⊢ 2 < xs.lengthxs[2]
failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α:Type ?u.3xs:List α⊢ 2 < xs.length

그러나 인덱싱 연산이 안전하다는 증거로 이루어진 인자를 추가하면, 리스트에 항목이 적어도 세 개 있음을 보여야 하는 의무를 호출자에게 부과할 수 있습니다:

def third (xs : List α) (ok : xs.length > 2) : α := xs[2]

이 예제에서 xs.length > 2는 xs의 항목이 2개보다 많은지 여부를 검사하는 프로그램이 아닙니다. 이것은 참일 수도 있고 거짓일 수도 있는 명제이며, 인자 ok는 그 명제가 참이라는 증거여야 합니다.

함수를 구체적인 리스트에 대해 호출하면 그 리스트의 길이를 알 수 있습니다. 이런 경우에는 by decide가 증거를 자동으로 구성할 수 있습니다:

"snail"#eval third woodlandCritters (⊢ woodlandCritters.length > 2 All goals completed! 🐙)
"snail"

증거 없이 인덱싱하기🔗

인덱싱 연산이 범위 안에 있음을 증명하기가 현실적이지 않은 경우에는 다른 대안이 있습니다. 물음표를 붙이면 결과는 Option이 되며, 인덱스가 범위 안에 있으면 결과는 some이고 그렇지 않으면 none입니다. 예를 들면 다음과 같습니다.

def thirdOption (xs : List α) : Option α := xs[2]?some "snail"#eval thirdOption woodlandCritters
some "snail"
none#eval thirdOption ["only", "two"]
none

인덱스가 범위를 벗어났을 때 Option을 반환하는 대신 프로그램을 비정상 종료시키는 버전도 있습니다:

"deer"#eval woodlandCritters[1]!
"deer"

마주칠 수 있는 메시지🔗

decide 택틱은 명제가 참임을 증명할 수 있을 뿐 아니라 거짓임도 증명할 수 있습니다. 원소가 하나뿐인 리스트가 원소를 두 개보다 많이 가진다는 것을 증명하라고 하면, 이 택틱은 해당 명제가 실제로 거짓임을 나타내는 오류를 반환합니다:

#eval third ["rabbit"] (⊢ ["rabbit"].length > 2 Tactic `decide` proved that the proposition ["rabbit"].length > 2 is false⊢ ["rabbit"].length > 2)
Tactic `decide` proved that the proposition
  ["rabbit"].length > 2
is false

simp 택틱과 decide 택틱은 def로 작성한 정의를 자동으로 펼치지 않습니다. simp를 사용해 OnePlusOneIsTwo를 증명하려고 하면 실패합니다:

theorem onePlusOneIsStillTwo : OnePlusOneIsTwo := ⊢ OnePlusOneIsTwo `simp` made no progress⊢ OnePlusOneIsTwo

오류 메시지는 단지 아무것도 할 수 없었다고만 알립니다. OnePlusOneIsTwo를 펼치지 않고서는 아무런 진전도 이룰 수 없기 때문입니다:

`simp` made no progress

decide를 사용해도 실패합니다:

theorem onePlusOneIsStillTwo : OnePlusOneIsTwo := ⊢ OnePlusOneIsTwo failed to synthesize Decidable OnePlusOneIsTwo Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.⊢ OnePlusOneIsTwo

이 역시 OnePlusOneIsTwo를 펼치지 않기 때문입니다:

failed to synthesize
  Decidable OnePlusOneIsTwo

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

OnePlusOneIsTwo를 abbrev로 정의하면 문제가 해결됩니다. 이렇게 하면 해당 정의가 펼쳐지도록 표시되기 때문입니다.

인덱싱 연산이 안전하다는 컴파일 타임 증거를 Lean이 찾지 못할 때 발생하는 오류 외에도, 안전하지 않은 인덱싱을 사용하는 다형 함수에서는 다음과 같은 메시지가 나타날 수 있습니다:

def unsafeThird (xs : List α) : α := failed to synthesize instance of type class Inhabited α Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.xs[2]!
failed to synthesize instance of type class
  Inhabited α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

이는 Lean을 정리 증명을 위한 논리 체계이자 프로그래밍 언어로 모두 쓸 수 있도록 유지하기 위한 기술적 제약 때문입니다. 구체적으로 말하면, 타입에 값이 하나 이상 있는 프로그램만 크래시할 수 있습니다. 이는 Lean에서 명제가 그 명제가 참이라는 증거를 분류하는 일종의 타입이기 때문입니다. 거짓 명제에는 그러한 증거가 없습니다. 빈 타입을 가진 프로그램이 크래시할 수 있다면, 그 크래시하는 프로그램을 거짓 명제에 대한 일종의 가짜 증거로 사용할 수 있게 됩니다.

Lean은 내부적으로 값이 적어도 하나 있다고 알려진 타입들의 표를 가지고 있습니다. 이 오류는 어떤 임의의 타입 α가 그 표에 반드시 들어 있는 것은 아니라는 뜻입니다. 다음 장에서는 이 표에 타입을 추가하는 방법과 unsafeThird 같은 함수를 문제없이 작성하는 방법을 설명합니다.

리스트와 조회에 사용하는 대괄호 사이에 공백을 넣으면 또 다른 메시지가 나타날 수 있습니다:

#eval Function expected at woodlandCritters but this term has type List String Note: Expected a function because this term is being applied to the argument [1]woodlandCritters [1]
Function expected at
  woodlandCritters
but this term has type
  List String

Note: Expected a function because this term is being applied to the argument
  [1]

공백을 추가하면 Lean은 이 표현식을 함수 적용으로 취급하고, 인덱스는 숫자 하나를 담은 리스트로 취급합니다. 이 오류 메시지는 Lean이 woodlandCritters를 함수로 취급하려고 시도했기 때문에 발생합니다.

연습 문제🔗

  • rfl을 사용해 다음 정리들을 증명하십시오: 2 + 3 = 5, 15 - 8 = 7, "Hello, ".append "world" = "Hello, world". rfl로 5 < 18을 증명하려고 하면 어떻게 됩니까? 왜 그렇습니까?

  • by decide를 사용하여 다음 정리들을 증명하십시오: 2 + 3 = 5, 15 - 8 = 7, "Hello, ".append "world" = "Hello, world", 5 < 18.

  • 리스트의 다섯 번째 항목을 조회하는 함수를 작성하십시오. 이 조회가 안전하다는 증거를 함수의 인자로 전달하십시오.