7. 귀납적 타입
우리는 Lean의 형식적 기반에 기본 타입인 Prop, Type 0, Type 1, Type 2, ...가 포함되어 있으며, 의존 함수 타입 (x : α) → β를 구성할 수 있다는 것을 살펴보았습니다. 예제에서는 Bool, Nat, Int와 같은 추가 타입과, List와 같은 타입 생성자, 그리고 곱 ×도 사용했습니다. 사실 Lean의 라이브러리에서 유니버스를 제외한 모든 구체적인 타입과 의존 화살표를 제외한 모든 타입 생성자는 귀납적 타입이라고 불리는 일반적인 타입 구성 계열의 인스턴스입니다. 타입 유니버스, 의존 화살표 타입, 귀납적 타입만을 기반으로 상당한 규모의 수학 체계를 구축할 수 있다는 것은 주목할 만합니다. 그 밖의 모든 것은 이것들로부터 따라 나옵니다.
직관적으로 말하면, 귀납적 타입은 지정된 생성자 목록으로부터 구성됩니다. Lean에서 이러한 타입을 지정하는 구문은 다음과 같습니다:
inductive Foo where | constructor₁ : ... → Foo | constructor₂ : ... → Foo ... | constructorₙ : ... → Foo
기본 발상은 각 생성자가 Foo의 새 객체를 만드는 방법을 하나씩 지정한다는 것이며, 이때 이미 만들어진 값을 재료로 쓸 수도 있습니다. Foo 타입은 이런 방식으로 만들어진 객체로만 이루어지며, 그 밖의 것은 포함하지 않습니다.
아래에서 살펴보겠지만, 생성자의 인자에는 Foo 타입의 객체가 포함될 수 있습니다. 다만 특정한 “양성(positivity)” 제약을 따라야 하며, 이 제약은 Foo의 원소가 아래에서부터 위로 구성됨을 보장합니다. 대략적으로 말하면, 각 ...는 Foo와 이전에 정의된 타입들로 구성된 어떤 화살표 타입이든 될 수 있습니다. 이때 Foo는 등장하더라도 의존 화살표 타입의 “대상(target)”으로만 등장합니다.
귀납적 타입의 예시를 여럿 제시하겠습니다. 또한 위 도식을 약간 일반화하여 상호 정의된 귀납적 타입과 이른바 귀납적 족도 살펴보겠습니다.
논리 연결사와 마찬가지로, 모든 귀납적 타입에는 그 타입의 원소를 구성하는 방법을 보여 주는 도입 규칙과, 그 타입의 원소를 다른 구성에서 “사용”하는 방법을 보여 주는 제거 규칙이 함께 주어집니다. 논리 연결사와 이렇게 닮았다는 것은 놀라운 일이 아닙니다. 아래에서 보겠지만, 논리 연결사 역시 귀납적 타입 구성의 예이기 때문입니다. 귀납적 타입의 도입 규칙은 이미 살펴보았습니다. 도입 규칙은 바로 해당 타입의 정의에 명시된 생성자들입니다. 제거 규칙은 그 타입에 대한 재귀의 원리를 제공하며, 여기에는 특수한 경우로서 귀납법의 원리도 포함됩니다.
다음 장에서는 Lean의 함수 정의 패키지를 설명합니다. 이 패키지를 사용하면 귀납적 타입 위에서 함수를 정의하고 귀납적 증명을 수행하기가 훨씬 더 편리해집니다. 하지만 귀납적 타입이라는 개념은 매우 근본적이므로, 저수준에서 직접 다루어 보며 이해하는 것부터 시작하는 것이 중요하다고 생각합니다. 먼저 귀납적 타입의 기본적인 예제 몇 가지로 시작하여, 점차 더 정교하고 복잡한 예제로 나아가겠습니다.
7.1. 열거형
가장 단순한 종류의 귀납적 타입은 원소들이 유한하게 열거된 목록으로 주어지는 타입입니다.
inductive Weekday where
| sunday : Weekday
| monday : Weekday
| tuesday : Weekday
| wednesday : Weekday
| thursday : Weekday
| friday : Weekday
| saturday : Weekday
inductive 명령은 새로운 타입 Weekday를 만듭니다. 생성자는 모두 Weekday 네임스페이스에 속합니다.
inductive Weekday where
| sunday : Weekday
| monday : Weekday
| tuesday : Weekday
| wednesday : Weekday
| thursday : Weekday
| friday : Weekday
| saturday : Weekday
#check Weekday.sunday
#check Weekday.monday
open Weekday
#check sunday
#check monday
Weekday 귀납적 타입을 선언할 때 : Weekday는 생략할 수 있습니다.
inductive Weekday where
| sunday
| monday
| tuesday
| wednesday
| thursday
| friday
| saturday
sunday, monday, ... , saturday를 Weekday의 서로 다른 원소로 생각하십시오. 이들 사이에는 그 밖에 구별되는 성질이 없습니다. 제거 원리 Weekday.rec은 타입 Weekday 및 그 생성자들과 함께 정의됩니다. 이것은 재귀자라고도 하며, 타입을 “귀납적”으로 만드는 것이 바로 이것입니다. 재귀자를 사용하면 각 생성자에 대응하는 값을 지정하여 Weekday 위의 함수를 정의할 수 있습니다. 직관적으로 말하면, 귀납적 타입은 생성자들에 의해 빠짐없이 생성되며 생성자들이 만들어 내는 것 외에는 다른 원소를 갖지 않습니다.
Weekday.rec.{u} {motive : Weekday → Sort u}
(sunday : motive Weekday.sunday)
(monday : motive Weekday.monday)
(tuesday : motive Weekday.tuesday)
(wednesday : motive Weekday.wednesday)
(thursday : motive Weekday.thursday)
(friday : motive Weekday.friday)
(saturday : motive Weekday.saturday)
(t : Weekday) :
motive t
match 표현식을 사용하여 Weekday에서 자연수로 가는 함수를 정의하겠습니다:
inductive Weekday where
| sunday : Weekday
| monday : Weekday
| tuesday : Weekday
| wednesday : Weekday
| thursday : Weekday
| friday : Weekday
| saturday : Weekday
open Weekday
def numberOfDay (d : Weekday) : Nat :=
match d with
| sunday => 1
| monday => 2
| tuesday => 3
| wednesday => 4
| thursday => 5
| friday => 6
| saturday => 7
#eval numberOfDay Weekday.sunday
#eval numberOfDay Weekday.monday
#eval numberOfDay Weekday.tuesday
Lean의 논리를 사용할 때 match 표현식은 귀납적 타입을 선언할 때 생성되는 재귀자인 Weekday.rec를 사용하여 컴파일됩니다. 이를 통해 결과 항이 타입 이론 안에서 잘 정의됨이 보장됩니다. 컴파일된 코드에서는 match가 다른 함수형 프로그래밍 언어에서와 같은 방식으로 컴파일됩니다.
inductive Weekday where
| sunday : Weekday
| monday : Weekday
| tuesday : Weekday
| wednesday : Weekday
| thursday : Weekday
| friday : Weekday
| saturday : Weekday
open Weekday
def numberOfDay (d : Weekday) : Nat :=
match d with
| sunday => 1
| monday => 2
| tuesday => 3
| wednesday => 4
| thursday => 5
| friday => 6
| saturday => 7
set_option pp.all true
#print numberOfDay
#print numberOfDay.match_1
#print Weekday.casesOn
#check @Weekday.rec
귀납적 데이터 타입을 선언할 때 deriving Repr를 사용하면 Weekday 객체를 텍스트로 변환하는 함수를 생성하도록 Lean에 지시할 수 있습니다. 이 함수는 #eval 명령이 Weekday 객체를 표시할 때 사용됩니다. Repr가 없으면 #eval은 그 자리에서 하나를 유도하려고 시도합니다.
inductive Weekday where
| sunday
| monday
| tuesday
| wednesday
| thursday
| friday
| saturday
deriving Repr
open Weekday
#eval tuesday
어떤 구조체와 관련된 정의와 정리를 그 구조체와 같은 이름의 네임스페이스에 모아 두면 유용한 경우가 많습니다. 예를 들어, numberOfDay 함수를 Weekday 네임스페이스에 넣을 수 있습니다. 그러면 해당 네임스페이스를 열었을 때 더 짧은 이름을 사용할 수 있습니다.
Weekday에서 Weekday로 가는 함수를 정의할 수 있습니다:
inductive Weekday where
| sunday : Weekday
| monday : Weekday
| tuesday : Weekday
| wednesday : Weekday
| thursday : Weekday
| friday : Weekday
| saturday : Weekday
deriving Repr
namespace Weekday
def next (d : Weekday) : Weekday :=
match d with
| sunday => monday
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => saturday
| saturday => sunday
def previous (d : Weekday) : Weekday :=
match d with
| sunday => saturday
| monday => sunday
| tuesday => monday
| wednesday => tuesday
| thursday => wednesday
| friday => thursday
| saturday => friday
#eval next (next tuesday)
#eval next (previous tuesday)
example : next (previous tuesday) = tuesday :=
rfl
end Weekday
임의의 Weekday d에 대해 next (previous d) = d라는 일반적인 정리를 어떻게 증명할 수 있습니까? match를 사용하면 각 생성자마다 주장에 대한 증명을 제공할 수 있습니다:
inductive Weekday where
| sunday : Weekday
| monday : Weekday
| tuesday : Weekday
| wednesday : Weekday
| thursday : Weekday
| friday : Weekday
| saturday : Weekday
deriving Repr
namespace Weekday
def next (d : Weekday) : Weekday :=
match d with
| sunday => monday
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => saturday
| saturday => sunday
def previous (d : Weekday) : Weekday :=
match d with
| sunday => saturday
| monday => sunday
| tuesday => monday
| wednesday => tuesday
| thursday => wednesday
| friday => thursday
| saturday => friday
theorem next_previous (d : Weekday) : next (previous d) = d :=
match d with
| sunday => rfl
| monday => rfl
| tuesday => rfl
| wednesday => rfl
| thursday => rfl
| friday => rfl
| saturday => rfl
택틱 증명을 사용하면 훨씬 더 간결하게 작성할 수 있습니다:
inductive Weekday where
| sunday : Weekday
| monday : Weekday
| tuesday : Weekday
| wednesday : Weekday
| thursday : Weekday
| friday : Weekday
| saturday : Weekday
deriving Repr
namespace Weekday
def next (d : Weekday) : Weekday :=
match d with
| sunday => monday
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => saturday
| saturday => sunday
def previous (d : Weekday) : Weekday :=
match d with
| sunday => saturday
| monday => sunday
| tuesday => monday
| wednesday => tuesday
| thursday => wednesday
| friday => thursday
| saturday => friday
theorem next_previous (d : Weekday) : next (previous d) = d := d:Weekday⊢ d.previous.next = d
⊢ sunday.previous.next = sunday⊢ monday.previous.next = monday⊢ tuesday.previous.next = tuesday⊢ wednesday.previous.next = wednesday⊢ thursday.previous.next = thursday⊢ friday.previous.next = friday⊢ saturday.previous.next = saturday ⊢ sunday.previous.next = sunday⊢ monday.previous.next = monday⊢ tuesday.previous.next = tuesday⊢ wednesday.previous.next = wednesday⊢ thursday.previous.next = thursday⊢ friday.previous.next = friday⊢ saturday.previous.next = saturday All goals completed! 🐙
아래의 귀납적 타입을 위한 택틱에서는 귀납적 타입을 활용하도록 특별히 설계된 추가 택틱들을 소개합니다.
명제-타입 대응 아래에서는 match를 사용하여 함수를 정의할 수 있을 뿐만 아니라 정리를 증명할 수도 있다는 점에 주목하십시오. 다시 말해, 명제-타입 대응 아래에서 경우에 따른 증명은 경우에 따른 정의의 일종이며, 여기서 “정의”되는 대상은 데이터 조각이 아니라 증명입니다.
Lean 라이브러리의 Bool 타입은 열거 타입의 한 예입니다.
(이 예제들을 실행하기 위해 예제들을 Hidden이라는 네임스페이스에 넣어, Bool 같은 이름이 표준 라이브러리의 Bool과 충돌하지 않게 합니다. 이러한 타입들은 시스템이 시작될 때 자동으로 임포트되는 Lean “프렐류드(prelude)”의 일부이기 때문에 이렇게 해야 합니다.)
연습 문제로, 이 타입들의 도입 규칙과 제거 규칙이 무엇을 하는지 생각해 보십시오. 추가 연습 문제로, Bool 타입에 불리언 연산 and, or, not을 정의하고 일반적인 항등식을 검증해 보기를 권합니다. and와 같은 이항 연산은 match를 사용하여 정의할 수 있다는 점에 유의하십시오:
namespace Hidden
def and (a b : Bool) : Bool :=
match a with
| true => b
| false => false
end Hidden
마찬가지로, 대부분의 항등식은 적절한 match를 도입한 다음 rfl을 사용하여 증명할 수 있습니다.
7.2. 인자를 받는 생성자
열거 타입은 귀납적 타입의 매우 특수한 경우로, 생성자가 인수를 전혀 받지 않습니다. 일반적으로 “구성”은 데이터에 의존할 수 있으며, 그 데이터는 구성된 인수 안에 표현됩니다. 라이브러리에 있는 곱 타입과 합 타입의 정의를 살펴봅시다.
namespace Hidden
inductive Prod (α : Type u) (β : Type v)
| mk : α → β → Prod α β
inductive Sum (α : Type u) (β : Type v) where
| inl : α → Sum α β
| inr : β → Sum α β
end Hidden
이 예제들에서 무슨 일이 일어나고 있는지 생각해 보십시오. 곱 타입에는 두 개의 인자를 받는 생성자 Prod.mk 하나가 있습니다. Prod α β 위의 함수를 정의할 때는 입력이 Prod.mk a b 꼴이라고 가정할 수 있으며, 출력은 a와 b로 이루어진 항으로 지정해야 합니다. 이를 사용하여 Prod의 두 사영(projection)을 정의할 수 있습니다. 표준 라이브러리는 Prod α β에 대해 α × β 표기법을, Prod.mk a b에 대해 (a, b) 표기법을 정의한다는 점을 기억하십시오.
namespace Hidden
inductive Prod (α : Type u) (β : Type v)
| mk : α → β → Prod α β
def fst {α : Type u} {β : Type v} (p : Prod α β) : α :=
match p with
| Prod.mk a b => a
def snd {α : Type u} {β : Type v} (p : Prod α β) : β :=
match p with
| Prod.mk a b => b
end Hidden
함수 fst는 순서쌍 p를 인자로 받습니다. match는 p를 순서쌍 Prod.mk a b로 해석합니다. 또한 의존 타입 이론에서 다루었듯이, 이 정의들을 최대한 일반적으로 만들기 위해 타입 α와 β가 임의의 유니버스에 속할 수 있도록 허용한다는 점을 상기하십시오.
다음은 match 대신 재귀자 Prod.casesOn을 사용하는 또 다른 예입니다.
def prod_example (p : Bool × Nat) : Nat :=
Prod.casesOn (motive := fun _ => Nat) p
(fun b n => cond b (2 * n) (2 * n + 1))
#eval prod_example (true, 3)
#eval prod_example (false, 3)
인자 motive는 구성하려는 객체의 타입을 지정하는 데 사용되며, 쌍에 의존할 수 있기 때문에 함수입니다. cond 함수는 불리언 조건문입니다. cond b t1 t2는 b가 참이면 t1을, 그렇지 않으면 t2를 반환합니다. 함수 prod_example은 불리언 b와 수 n으로 이루어진 쌍을 받아, b가 참인지 거짓인지에 따라 2 * n 또는 2 * n + 1을 반환합니다.
반면에 합 타입에는 inl과 inr(각각 “왼쪽에 삽입(insert left)”과 “오른쪽에 삽입(insert right)”을 뜻합니다)이라는 두 개의 생성자가 있으며, 각 생성자는 하나의 (명시적) 인수를 받습니다. Sum α β에 대한 함수를 정의하려면 두 가지 경우를 처리해야 합니다. 입력이 inl a 형태라면 a를 사용하는 항으로 출력값을 지정해야 하고, 입력이 inr b 형태라면 b를 사용하는 항으로 출력값을 지정해야 합니다.
def sum_example (s : Sum Nat Nat) : Nat :=
Sum.casesOn (motive := fun _ => Nat) s
(fun n => 2 * n)
(fun n => 2 * n + 1)
#eval sum_example (Sum.inl 3)
#eval sum_example (Sum.inr 3)
이 예제는 앞의 예제와 비슷하지만, 이번에는 sum_example의 입력이 암묵적으로 inl n 또는 inr n 형태 중 하나입니다. 첫 번째 경우 함수는 2 * n을 반환하고, 두 번째 경우에는 2 * n + 1을 반환합니다.
곱 타입이 매개변수 α β : Type에 의존한다는 점에 주목하십시오. 이 매개변수들은 Prod뿐만 아니라 생성자의 인자이기도 합니다. Lean은 이러한 인자를 생성자의 뒤쪽 인자나 반환 타입으로부터 추론할 수 있는 경우를 감지하고, 그러한 경우에는 해당 인자를 암시적 인자로 만듭니다.
자연수 정의하기에서는 귀납적 타입의 생성자가 그 귀납적 타입 자체를 인자로 받을 때 어떤 일이 일어나는지 살펴보겠습니다. 이 절에서 다루는 예제들의 특징은 각 생성자가 앞서 지정된 타입에만 의존한다는 점입니다.
생성자가 여러 개인 타입은 선언적(disjunctive)이라는 점에 유의하십시오. Sum α β의 원소는 inl a 형태 또는 inl b 형태 중 하나입니다. 인자가 여러 개인 생성자는 연언적(conjunctive) 정보를 도입합니다. Prod α β의 원소 Prod.mk a b로부터 a 그리고 b를 추출할 수 있습니다. 임의의 귀납적 타입은 생성자를 몇 개든 가질 수 있고 각 생성자가 인자를 몇 개든 받을 수 있으므로, 두 특징을 모두 포함할 수 있습니다.
함수 정의와 마찬가지로, Lean의 귀납적 정의 구문에서는 생성자에 대한 이름 있는 인자를 콜론 앞에 둘 수 있습니다:
namespace Hidden
inductive Prod (α : Type u) (β : Type v) where
| mk (fst : α) (snd : β) : Prod α β
inductive Sum (α : Type u) (β : Type v) where
| inl (a : α) : Sum α β
| inr (b : β) : Sum α β
end Hidden
이 정의들의 결과는 이 절의 앞부분에서 제시한 정의들의 결과와 본질적으로 같습니다.
Prod처럼 생성자가 하나뿐인 타입은 순수하게 연언적입니다. 생성자는 인자 목록을 하나의 데이터로 묶을 뿐이며, 이는 본질적으로 뒤따르는 인자의 타입이 첫 번째 인자의 타입에 의존할 수 있는 튜플입니다. 이러한 타입을 “레코드” 또는 “구조체”로 생각할 수도 있습니다. Lean에서는 structure 키워드를 사용하여 이러한 귀납적 타입과 그 사영(projection)을 동시에 정의할 수 있습니다.
이 예제는 귀납적 타입 Prod, 그 생성자 mk, 통상적인 제거자(rec와 recOn), 그리고 위에서 정의한 것과 같은 사영 fst와 snd를 동시에 도입합니다.
생성자의 이름을 지정하지 않으면 Lean은 기본값으로 mk를 사용합니다. 예를 들어, 다음은 색상을 RGB 값의 세 쌍으로 저장하는 레코드를 정의합니다.
structure Color where
red : Nat
green : Nat
blue : Nat
deriving Repr
def yellow := Color.mk 255 255 0
#eval Color.red yellow
yellow의 정의는 표시된 세 값으로 레코드를 구성하며, 사영 Color.red는 빨간색 성분을 반환합니다.
structure 명령은 대수적 구조를 정의할 때 특히 유용하며, Lean은 이러한 구조를 다루는 데 필요한 기반 기능을 폭넓게 제공합니다. 예를 들어, 반군(semigroup)은 다음과 같이 정의합니다:
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)
더 많은 예제는 구조체와 레코드를 다루는 장에서 살펴보겠습니다.
의존 곱 타입 Sigma는 이미 살펴본 바 있습니다:
namespace Hidden
inductive Sigma {α : Type u} (β : α → Type v) where
| mk : (a : α) → β a → Sigma β
end Hidden
라이브러리에 있는 귀납적 타입의 예를 두 가지 더 들면 다음과 같습니다.
namespace Hidden
inductive Option (α : Type u) where
| none : Option α
| some : α → Option α
inductive Inhabited (α : Type u) where
| mk : α → Inhabited α
end Hidden
의존 타입 이론의 의미론에는 부분 함수라는 개념이 기본적으로 내장되어 있지 않습니다. 함수 타입 α → β나 의존 함수 타입 (a : α) → β의 모든 원소는 모든 입력에 대해 값을 갖는다고 가정됩니다. Option 타입은 부분 함수를 표현하는 방법을 제공합니다. Option β의 원소는 none이거나, 어떤 값 b : β에 대해 some b 형태입니다. 따라서 타입 α → Option β의 원소 f를 α에서 β로 가는 부분 함수로 생각할 수 있습니다. 즉, 모든 a : α에 대해 f a는 f a가 “정의되지 않음”을 나타내는 none을 반환하거나, some b를 반환합니다.
Inhabited α의 원소는 단순히 α의 원소가 존재한다는 사실에 대한 증거입니다. 나중에 Inhabited가 Lean에서 타입 클래스의 한 예라는 것을 보게 될 것입니다. Lean에게 적절한 기본 타입들이 원소를 가진다는 것을 알려 줄 수 있으며, Lean은 이를 바탕으로 다른 구성된 타입들도 원소를 가진다는 것을 자동으로 추론할 수 있습니다.
연습 문제로 α에서 β로 가는 부분 함수와 β에서 γ로 가는 부분 함수의 합성 개념을 정의하고, 이것이 예상대로 동작함을 보여 보시기를 권합니다. 또한 Bool과 Nat이 거주된(inhabited) 타입임을, 거주된 두 타입의 곱도 거주된 타입임을, 그리고 거주된 타입으로 가는 함수들의 타입도 거주된 타입임을 보여 보시기를 권합니다.
7.3. 귀납적으로 정의된 명제
귀납적으로 정의된 타입은 가장 아래에 있는 유니버스인 Prop을 포함하여 어떤 타입 유니버스에도 속할 수 있습니다. 사실 논리 연결사는 바로 이러한 방식으로 정의됩니다.
namespace Hidden
inductive False : Prop
inductive True : Prop where
| intro : True
inductive And (a b : Prop) : Prop where
| intro : a → b → And a b
inductive Or (a b : Prop) : Prop where
| inl : a → Or a b
| inr : b → Or a b
end Hidden
이것들이 어떻게 여러분이 이미 본 도입 규칙과 제거 규칙을 만들어 내는지 생각해 보십시오. 귀납적 타입의 제거자가 무엇으로 제거할 수 있는지, 즉 어떤 종류의 타입이 재귀자의 대상이 될 수 있는지를 규정하는 규칙들이 있습니다. 대략적으로 말하면, Prop에 속한 귀납적 타입의 특징은 Prop에 속한 다른 타입으로만 소거할 수 있다는 점입니다. 이는 p : Prop이면 원소 hp : p는 아무런 데이터도 담지 않는다는 이해와 일치합니다. 그러나 이 규칙에는 작은 예외가 하나 있으며, 이는 아래 귀납적 족에서 논의하겠습니다.
존재 한정자조차도 귀납적으로 정의됩니다:
namespace Hidden
inductive Exists {α : Sort u} (p : α → Prop) : Prop where
| intro (w : α) (h : p w) : Exists p
end Hidden
∃ x : α, p 표기법은 Exists (fun x : α => p)의 문법적 설탕(syntactic sugar)이라는 점을 기억하십시오.
False, True, And, Or의 정의는 Empty, Unit, Prod, Sum의 정의와 완전히 대응합니다. 차이점은 앞의 것들은 Prop의 원소를 만들어 내고, 뒤의 것들은 어떤 u에 대해 Type u의 원소를 만들어 낸다는 것입니다. 마찬가지로 ∃ x : α, p는 Σ x : α, β를 Prop 값으로 바꾼 변형입니다.
여기서 {x : α // p}로 표기하는 또 다른 귀납적 타입을 소개하면 좋겠습니다. 이 타입은 ∃ x : α, p와 Σ x : α, β를 섞은 것이라고 할 수 있습니다.
namespace Hidden
inductive Subtype {α : Type u} (p : α → Prop) where
| mk : (x : α) → p x → Subtype p
end Hidden
실제로 Lean에서 Subtype은 structure 명령을 사용하여 정의됩니다:
namespace Hidden
structure Subtype {α : Sort u} (p : α → Prop) where
val : α
property : p val
end Hidden
{x : α // p x} 표기법은 Subtype (fun x : α => p x)의 문법적 설탕(syntactic sugar)입니다. 이것은 집합 이론의 부분집합 표기법을 본뜬 것입니다. {x : α // p x}가 α의 원소 중에서 성질 p를 만족하는 것들의 모임을 나타낸다는 생각입니다.
7.4. 자연수 정의하기
지금까지 살펴본 귀납적으로 정의된 타입들은 “평평”합니다. 생성자는 데이터를 감싸서 타입 안에 넣고, 이에 대응하는 재귀자는 그 데이터를 풀어서 처리합니다. 생성자가 지금 정의되고 있는 바로 그 타입의 원소에 작용할 때 상황은 훨씬 더 흥미로워집니다. 대표적인 예는 자연수 타입 Nat입니다:
생성자는 두 개입니다. 먼저 zero : Nat에서 시작합니다. 이 생성자는 인자를 받지 않으므로 처음부터 주어져 있습니다. 반면 생성자 succ은 이전에 생성된 Nat에만 적용할 수 있습니다. 이를 zero에 적용하면 succ zero : Nat을 얻습니다. 한 번 더 적용하면 succ (succ zero) : Nat을 얻으며, 이런 식으로 계속됩니다. 직관적으로 Nat은 이러한 생성자들을 갖는 “가장 작은” 타입입니다. 즉, zero에서 시작하여 succ을 반복해서 적용함으로써 빠짐없이 (그리고 자유롭게) 생성된다는 뜻입니다.
앞에서와 마찬가지로, Nat의 재귀자는 Nat에서 임의의 정의역으로 가는 의존 함수 f를 정의하도록 설계되어 있습니다. 즉, 어떤 motive : Nat → Sort u에 대해 (n : Nat) → motive n의 원소인 f를 정의합니다. 재귀자는 두 가지 경우를 처리해야 합니다. 하나는 입력이 zero인 경우이고, 다른 하나는 입력이 어떤 n : Nat에 대해 succ n 형태인 경우입니다. 첫 번째 경우에는 앞에서와 마찬가지로 알맞은 타입을 가진 목표 값을 지정하기만 하면 됩니다. 그러나 두 번째 경우에는 재귀자가 n에서의 f 값이 이미 계산되었다고 가정할 수 있습니다. 그 결과, 재귀자의 다음 인자는 f (succ n)의 값을 n과 f n의 항으로 지정합니다. 재귀자의 타입을 확인해 보면 다음과 같습니다.
Nat.rec.{u} :
{motive : Nat → Sort u} →
(zero : motive Nat.zero) →
(succ : (n : Nat) → motive n → motive (Nat.succ n)) →
(t : Nat) → motive t
암시적 인자 motive는 정의되는 함수의 공역입니다. 타입 이론에서는 motive를 제거/재귀의 동기(motive)라고 부르는 것이 일반적입니다. 이는 우리가 구성하고자 하는 대상의 종류를 기술하기 때문입니다. 다음 두 인수는 앞서 설명한 대로 0인 경우와 후속자인 경우를 계산하는 방법을 지정합니다. 이들은 소전제(minor premises)라고도 합니다. 마지막으로, t : Nat은 함수의 입력입니다. 이것은 대전제(major premise)라고도 합니다.
Nat.recOn은 Nat.rec과 비슷하지만, 주 전제가 부 전제들보다 앞에 옵니다.
Nat.recOn.{u} :
{motive : Nat → Sort u} →
(t : Nat) →
(zero : motive Nat.zero) →
(succ : ((n : Nat) → motive n → motive (Nat.succ n))) →
motive t
예를 들어, 자연수에 대한 덧셈 함수 add m n을 생각해 봅시다. m을 고정하면 n에 대한 재귀로 덧셈을 정의할 수 있습니다. 기저 사례에서는 add m zero를 m으로 정합니다. 후속자 단계에서는 add m n의 값이 이미 결정되어 있다고 가정하고, add m (succ n)을 succ (add m n)으로 정의합니다.
namespace Hidden
inductive Nat where
| zero : Nat
| succ : Nat → Nat
deriving Repr
def add (m n : Nat) : Nat :=
match n with
| Nat.zero => m
| Nat.succ n => Nat.succ (add m n)
open Nat
#eval add (succ (succ zero)) (succ zero)end Hidden
이러한 정의들은 Nat이라는 네임스페이스에 넣어 두는 것이 유용합니다. 그런 다음 그 네임스페이스 안에서 익숙한 표기법을 정의할 수 있습니다. 이제 덧셈에 대한 두 정의 방정식은 정의적으로 성립합니다:
namespace Nat
def add (m n : Nat) : Nat :=
match n with
| Nat.zero => m
| Nat.succ n => Nat.succ (add m n)
instance : Add Nat where
add := add
theorem add_zero (m : Nat) : m + zero = m := rfl
theorem add_succ (m n : Nat) : m + succ n = succ (m + n) := rfl
end Nat
end Hidden
instance 명령이 어떻게 동작하는지는 타입 클래스 장에서 설명하겠습니다. 아래 예제에서는 Lean에서 제공하는 자연수를 사용하겠습니다.
그러나 0 + n = n과 같은 사실을 증명하려면 귀납법에 의한 증명이 필요합니다. 앞서 살펴본 바와 같이, 공역 motive n이 Prop의 원소인 경우 귀납법 원리는 재귀 원리의 특수한 경우일 뿐입니다. 이는 우리에게 익숙한 귀납적 증명의 패턴을 나타냅니다. ∀ n, motive n을 증명하려면 먼저 motive 0을 증명하고, 그다음 임의의 n에 대해 ih : motive n을 가정하고 motive (n + 1)을 증명합니다.
namespace Hidden
open Nat
theorem zero_add (n : Nat) : 0 + n = n :=
Nat.recOn (motive := fun x => 0 + x = x)
n
(show 0 + 0 = 0 from rfl)
(fun (n : Nat) (ih : 0 + n = n) =>
show 0 + (n + 1) = n + 1 from
calc 0 + (n + 1)
_ = (0 + n) + 1 := rfl
_ = n + 1 := n✝:Natn:Natih:0 + n = n⊢ 0 + n + 1 = n + 1 All goals completed! 🐙)
end Hidden
다시 한번 주목하십시오. 증명의 맥락에서 Nat.recOn을 사용하면, 이는 사실상 모습을 바꾼 귀납법 원리입니다. 이와 같은 증명에서는 rw와 simp 택틱이 매우 효과적인 경우가 많습니다. 이 경우에는 어느 쪽을 사용하든 증명을 다음과 같이 줄일 수 있습니다:
namespace Hidden
open Nat
theorem zero_add (n : Nat) : 0 + n = n :=
Nat.recOn (motive := fun x => 0 + x = x) n
rfl
(fun n ih => n✝:Natn:Natih:0 + n = n⊢ 0 + n.succ = n.succ All goals completed! 🐙)
end Hidden
또 다른 예로, 덧셈의 결합법칙 ∀ m n k, m + n + k = m + (n + k)를 증명해 봅시다. (우리가 정의한 + 표기법은 왼쪽으로 결합하므로, m + n + k는 실제로는 (m + n) + k입니다.) 가장 어려운 부분은 어떤 변수에 대해 귀납법을 적용할지 알아내는 것입니다. 덧셈은 두 번째 인자에 대한 재귀로 정의되어 있으므로 k를 고르는 것이 좋은 선택이며, 일단 그렇게 선택하고 나면 증명은 거의 저절로 써집니다:
namespace Hidden
open Nat
theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) :=
Nat.recOn (motive := fun k => m + n + k = m + (n + k)) k
(show m + n + 0 = m + (n + 0) from rfl)
(fun k (ih : m + n + k = m + (n + k)) =>
show m + n + (k + 1) = m + (n + (k + 1)) from
calc m + n + (k + 1)
_ = (m + n + k) + 1 := rfl
_ = (m + (n + k)) + 1 := m:Natn:Natk✝:Natk:Natih:m + n + k = m + (n + k)⊢ m + n + k + 1 = m + (n + k) + 1 All goals completed! 🐙
_ = m + ((n + k) + 1) := rfl
_ = m + (n + (k + 1)) := rfl)
end Hidden
이번에도 증명을 다음과 같이 줄일 수 있습니다:
open Nat
theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) :=
Nat.recOn (motive := fun k => m + n + k = m + (n + k)) k
rfl
(fun k ih => m:Natn:Natk✝:Natk:Natih:m + n + k = m + (n + k)⊢ m + n + k.succ = m + (n + k.succ) m:Natn:Natk✝:Natk:Natih:m + n + k = m + (n + k)⊢ m + (n + k) + 1 = m + (n + (k + 1)); All goals completed! 🐙)
덧셈의 교환법칙을 증명하려 한다고 가정해 봅시다. 두 번째 인자에 대한 귀납법을 선택하면 다음과 같이 시작할 수 있습니다.
open Nat
theorem add_comm (m n : Nat) : m + n = n + m :=
Nat.recOn (motive := fun x => m + x = x + m) n
(show m + 0 = 0 + m All goals completed! 🐙 All goals completed! 🐙)
(fun (n : Nat) (ih : m + n = n + m) =>
show m + succ n = succ n + m from
calc m + succ n
_ = succ (m + n) := rfl
_ = succ (n + m) := m:Natn✝:Natn:Natih:m + n = n + m⊢ (m + n).succ = (n + m).succ All goals completed! 🐙
_ = succ n + m := sorry)
이 시점에서 또 다른 보조 사실, 즉 succ (n + m) = succ n + m이 필요하다는 것을 알 수 있습니다. 이는 m에 대한 귀납법으로 증명할 수 있습니다:
open Nat
theorem succ_add (n m : Nat) : succ n + m = succ (n + m) :=
Nat.recOn (motive := fun x => succ n + x = succ (n + x)) m
(show succ n + 0 = succ (n + 0) from rfl)
(fun (m : Nat) (ih : succ n + m = succ (n + m)) =>
show succ n + succ m = succ (n + succ m) from
calc succ n + succ m
_ = succ (succ n + m) := rfl
_ = succ (succ (n + m)) := n:Natm✝:Natm:Natih:n.succ + m = (n + m).succ⊢ (n.succ + m).succ = (n + m).succ.succ All goals completed! 🐙
_ = succ (n + succ m) := rfl)
그런 다음 이전 증명의 sorry를 succ_add로 바꿀 수 있습니다. 이번에도 증명을 압축할 수 있습니다:
namespace Hidden
inductive Nat where
| zero : Nat
| succ : Nat → Nat
deriving Repr
def add (m n : Nat) : Nat :=
match n with
| Nat.zero => m
| Nat.succ n => Nat.succ (add m n)
instance : Add Nat where
add := add
namespace Nat
theorem add_zero (m : Nat) : m + zero = m := rfl
theorem add_succ (m n : Nat) : m + succ n = succ (m + n) := rfl
theorem zero_add (n : Nat) : zero + n = n :=
Nat.recOn (motive := fun x => zero + x = x) n
rfl
(fun n ih => n✝:Natn:Natih:zero + n = n⊢ zero + n.succ = n.succ All goals completed! 🐙)
end Nat
open Nat
theorem succ_add (n m : Nat) : succ n + m = succ (n + m) :=
Nat.recOn (motive := fun x => succ n + x = succ (n + x)) m
rfl
(fun m ih => n:Natm✝:Natm:Natih:n.succ + m = (n + m).succ⊢ n.succ + m.succ = (n + m.succ).succ All goals completed! 🐙)
theorem add_comm (m n : Nat) : m + n = n + m :=
Nat.recOn (motive := fun x => m + x = x + m) n
(m:Natn:Nat⊢ m + zero = zero + m All goals completed! 🐙)
(fun m ih => m✝:Natn:Natm:Natih:m✝ + m = m + m✝⊢ m✝ + m.succ = m.succ + m✝ All goals completed! 🐙)
end Hidden
7.5. 그 밖의 재귀적 데이터 타입
귀납적으로 정의된 타입의 예를 몇 가지 더 살펴봅시다. 임의의 타입 α에 대해, α의 원소들로 이루어진 리스트의 타입 List α가 라이브러리에 정의되어 있습니다.
namespace Hidden
inductive List (α : Type u) where
| nil : List α
| cons (h : α) (t : List α) : List α
namespace List
def append (as bs : List α) : List α :=
match as with
| nil => bs
| cons a as => cons a (append as bs)
theorem nil_append (as : List α) : append nil as = as :=
rfl
theorem cons_append (a : α) (as bs : List α) :
append (cons a as) bs = cons a (append as bs) :=
rfl
end List
end Hidden
α 타입 원소들의 리스트는 빈 리스트 nil이거나, 원소 h : α 뒤에 리스트 t : List α가 이어지는 것입니다. 첫 번째 원소인 h는 흔히 리스트의 “머리(head)”라고 불리며, 나머지인 t는 “꼬리(tail)”라고 불립니다.
연습 문제로 다음을 증명해 보십시오:
namespace Hidden
inductive List (α : Type u) where
| nil : List α
| cons : α → List α → List α
namespace List
def append (as bs : List α) : List α :=
match as with
| nil => bs
| cons a as => cons a (append as bs)
theorem nil_append (as : List α) : append nil as = as :=
rfl
theorem cons_append (a : α) (as bs : List α)
: append (cons a as) bs = cons a (append as bs) :=
rfl
theorem append_nil (as : List α) :
append as nil = as :=
sorry
theorem append_assoc (as bs cs : List α) :
append (append as bs) cs = append as (append bs cs) :=
sorry
end List
end Hidden
리스트의 길이를 반환하는 함수 length : {α : Type u} → List α → Nat도 정의해 보고, 이 함수가 예상대로 동작함을 증명해 보십시오(예를 들어, length (append as bs) = length as + length bs).
또 다른 예로, 이진 트리 타입을 다음과 같이 정의할 수 있습니다:
inductive BinaryTree where
| leaf : BinaryTree
| node : BinaryTree → BinaryTree → BinaryTree
사실, 가산 개의 가지를 갖는 트리의 타입까지도 정의할 수 있습니다:
7.6. 귀납적 타입을 위한 택틱
Lean에서 귀납적 타입이 지니는 근본적인 중요성을 고려하면, 귀납적 타입을 효과적으로 다루도록 설계된 택틱이 여럿 있다는 것은 그리 놀라운 일이 아닙니다. 여기서는 그중 몇 가지를 설명합니다.
cases 택틱은 귀납적으로 정의된 타입의 원소에 작용하며, 이름 그대로의 일을 합니다. 즉, 가능한 각 생성자에 따라 해당 원소를 분해합니다. 가장 기본적인 형태에서 이 택틱은 로컬 컨텍스트에 있는 원소 x에 적용됩니다. 그러면 목표를 x가 각 생성자로 만든 형태로 대체된 경우들로 환원합니다.
example (p : Nat → Prop)
(hz : p 0) (hs : ∀ n, p (Nat.succ n)) :
∀ n, p n := p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succ⊢ ∀ (n : Nat), p n
p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succn:Nat⊢ p n
p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succ⊢ p 0p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succn✝:Nat⊢ p (n✝ + 1)
p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succ⊢ p 0 All goals completed! 🐙
p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succn✝:Nat⊢ p (n✝ + 1) All goals completed! 🐙
첫 번째 분기에서 증명 상태는 다음과 같습니다.
두 번째 분기에서는 다음과 같습니다:
이 밖에도 부가 기능이 더 있습니다. 우선, cases에서는 with 절을 사용하여 각 경우의 이름을 직접 정할 수 있습니다. 예를 들어 다음 예제에서는 succ의 인자 이름을 m으로 정하여 두 번째 경우가 succ m을 가리키도록 합니다. 더 중요한 점은, cases 택틱이 로컬 컨텍스트에서 대상 변수에 의존하는 모든 항목을 감지한다는 것입니다. 이 택틱은 해당 항목들을 되돌리고, 경우를 나눈 다음, 다시 도입합니다. 아래 예제에서 가설 h : n ≠ 0이 첫 번째 분기에서는 h : 0 ≠ 0이 되고, 두 번째 분기에서는 h : m + 1 ≠ 0이 된다는 점에 주목하십시오.
open Nat
example (n : Nat) (h : n ≠ 0) : succ (pred n) = n := n:Nath:n ≠ 0⊢ n.pred.succ = n
cases n with
h:0 ≠ 0⊢ (pred 0).succ = 0
All goals completed! 🐙
m:Nath:m + 1 ≠ 0⊢ (m + 1).pred.succ = m + 1
All goals completed! 🐙
cases는 명제를 증명할 때뿐만 아니라 데이터를 만들어 낼 때에도 사용할 수 있다는 점에 주목하십시오.
def f (n : Nat) : Nat := n:Nat⊢ Nat
⊢ Natn✝:Nat⊢ Nat; n✝:Nat⊢ Nat; All goals completed! 🐙
example : f 0 = 3 := rfl
example : f 5 = 7 := rfl
이번에도 cases는 컨텍스트의 의존성을 되돌리고(revert), 분할한 다음, 다시 도입합니다.
def Tuple (α : Type) (n : Nat) :=
{ as : List α // as.length = n }
def f {n : Nat} (t : Tuple α n) : Nat := α:Typen:Natt:Tuple α n⊢ Nat
α:Typet:Tuple α 0⊢ Natα:Typen✝:Natt:Tuple α (n✝ + 1)⊢ Nat; α:Typen✝:Natt:Tuple α (n✝ + 1)⊢ Nat; All goals completed! 🐙
def myTuple : Tuple Nat 3 :=
⟨[0, 1, 2], rfl⟩
example : f myTuple = 7 :=
rfl
다음은 인자를 갖는 생성자가 여러 개 있는 예입니다.
inductive Foo where
| bar1 : Nat → Nat → Foo
| bar2 : Nat → Nat → Nat → Foo
def silly (x : Foo) : Nat := x:Foo⊢ Nat
cases x with
a:Natb:Nat⊢ Nat All goals completed! 🐙
c:Natd:Nate:Nat⊢ Nat All goals completed! 🐙
각 생성자에 대한 대안은 생성자가 선언된 순서대로 해결하지 않아도 됩니다.
def silly (x : Foo) : Nat := x:Foo⊢ Nat
cases x with
c:Natd:Nate:Nat⊢ Nat All goals completed! 🐙
a:Natb:Nat⊢ Nat All goals completed! 🐙
with의 구문은 구조화된 증명을 작성하는 데 편리합니다. Lean은 이를 보완하는 case 택틱도 제공하며, 이 택틱을 사용하면 목표에 집중하고 변수 이름을 지정할 수 있습니다.
def silly (x : Foo) : Nat := x:Foo⊢ Nat
a✝¹:Nata✝:Nat⊢ Nata✝²:Nata✝¹:Nata✝:Nat⊢ Nat
case bar1 a b a:Natb:Nat⊢ Nat All goals completed! 🐙
case bar2 c d e c:Natd:Nate:Nat⊢ Nat All goals completed! 🐙
case 택틱은 생성자를 알맞은 목표에 대응시켜 준다는 점에서 영리합니다. 예를 들어, 위의 목표들을 반대 순서로 채울 수도 있습니다.
def silly (x : Foo) : Nat := x:Foo⊢ Nat
a✝¹:Nata✝:Nat⊢ Nata✝²:Nata✝¹:Nata✝:Nat⊢ Nat
case bar2 c d e c:Natd:Nate:Nat⊢ Nat All goals completed! 🐙
case bar1 a b a:Natb:Nat⊢ Nat All goals completed! 🐙
임의의 표현식에 cases를 사용할 수도 있습니다. 그 표현식이 목표에 나타난다면, cases 택틱은 그 표현식을 일반화하고, 그 결과로 생기는 전칭 양화된 변수를 도입한 다음, 그 변수에 대해 경우를 나눕니다.
open Nat
example (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (succ n)) (m k : Nat)
: p (m + 3 * k) := p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succm:Natk:Nat⊢ p (m + 3 * k)
p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succm:Natk:Nat⊢ p 0p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succm:Natk:Natn✝:Nat⊢ p (n✝ + 1)
p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succm:Natk:Natn✝:Nat⊢ p (n✝ + 1) -- goal is p 0
All goals completed! 🐙 -- goal is a : Nat ⊢ p (succ a)
이를 “m + 3 * k가 0인지 아니면 어떤 수의 후속자인지에 따라 경우를 나누라”는 말로 생각하십시오. 그 결과는 기능적으로 다음과 동등합니다:
open Nat
example (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (succ n)) (m k : Nat)
: p (m + 3 * k) := p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succm:Natk:Nat⊢ p (m + 3 * k)
p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succm:Natk:Natn:Nat⊢ p n
p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succm:Natk:Nat⊢ p 0p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succm:Natk:Natn✝:Nat⊢ p (n✝ + 1)
p:Nat → Prophz:p 0hs:∀ (n : Nat), p n.succm:Natk:Natn✝:Nat⊢ p (n✝ + 1)
All goals completed! 🐙
generalize에 의해 표현식 m + 3 * k가 지워진다는 점에 주목하십시오. 중요한 것은 그것이 0 꼴인지 n✝ + 1 꼴인지뿐입니다. 이 형태의 cases는 등식 안의 표현식(이 경우에는 m + 3 * k)을 함께 언급하는 가설을 되돌리지 않습니다. 그러한 항이 가설에 나타나고 그것에 대해서도 일반화하고 싶다면, 그 가설을 명시적으로 revert해야 합니다.
케이스 분석 대상인 표현식이 목표에 나타나지 않으면 cases 택틱은 have를 사용하여 그 표현식의 타입을 컨텍스트에 넣습니다. 다음은 예시입니다.
example (p : Prop) (m n : Nat)
(h₁ : m < n → p) (h₂ : m ≥ n → p) : p := p:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → p⊢ p
p:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → ph✝:m < n⊢ pp:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → ph✝:m ≥ n⊢ p
case inl hlt p:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → phlt:m < n⊢ p All goals completed! 🐙
case inr hge p:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → phge:m ≥ n⊢ p All goals completed! 🐙
정리 Nat.lt_or_ge m n은 m < n ∨ m ≥ n이라는 내용이며, 위 증명은 이 두 경우로 나누어 진행한다고 생각하는 것이 자연스럽습니다. 첫 번째 분기에서는 가설 hlt : m < n이 있고, 두 번째 분기에서는 가설 hge : m ≥ n이 있습니다. 위 증명은 기능적으로 다음과 동등합니다.
example (p : Prop) (m n : Nat)
(h₁ : m < n → p) (h₂ : m ≥ n → p) : p := p:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → p⊢ p
p:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → ph:m < n ∨ m ≥ n⊢ p
p:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → ph✝:m < n⊢ pp:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → ph✝:m ≥ n⊢ p
case inl hlt p:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → phlt:m < n⊢ p All goals completed! 🐙
case inr hge p:Propm:Natn:Nath₁:m < n → ph₂:m ≥ n → phge:m ≥ n⊢ p All goals completed! 🐙
처음 두 줄 다음에는 h : m < n ∨ m ≥ n이 가설로 주어지며, 이에 대해 경우 분석을 하기만 하면 됩니다.
다음은 또 다른 예제입니다. 여기서는 자연수 상등의 결정 가능성을 이용하여 m = n인 경우와 m ≠ n인 경우로 나눕니다.
#check Nat.sub_self
example (m n : Nat) : m - n = 0 ∨ m ≠ n := m:Natn:Nat⊢ m - n = 0 ∨ m ≠ n
cases Decidable.em (m = n) with
m:Natn:Natheq:m = n⊢ m - n = 0 ∨ m ≠ n m:Natn:Natheq:m = n⊢ n - n = 0 ∨ n ≠ n; m:Natn:Natheq:m = n⊢ n - n = 0; All goals completed! 🐙
m:Natn:Nathne:¬m = n⊢ m - n = 0 ∨ m ≠ n m:Natn:Nathne:¬m = n⊢ m ≠ n; All goals completed! 🐙
open Classical을 하면 어떤 명제에 대해서든 배중률을 사용할 수 있다는 점을 기억하십시오. 그러나 타입 클래스 추론(타입 클래스 참조)을 사용하면 Lean이 실제로 관련 결정 절차를 찾아낼 수 있으며, 이는 계산 가능한 함수 안에서도 이 경우 분할을 사용할 수 있다는 뜻입니다.
cases 택틱을 사용하여 경우에 따른 증명을 수행할 수 있는 것처럼, induction 택틱을 사용하여 귀납법에 의한 증명을 수행할 수 있습니다. 구문은 cases의 구문과 비슷하지만, 인자는 로컬 컨텍스트에 있는 항만 될 수 있다는 점이 다릅니다. 다음은 예시입니다:
namespace Hidden
theorem zero_add (n : Nat) : 0 + n = n := n:Nat⊢ 0 + n = n
induction n with
⊢ 0 + 0 = 0 All goals completed! 🐙
n:Natih:0 + n = n⊢ 0 + (n + 1) = n + 1 All goals completed! 🐙
end Hidden
cases와 마찬가지로, with 대신 case 택틱을 사용할 수 있습니다.
namespace Hidden
theorem zero_add (n : Nat) : 0 + n = n := n:Nat⊢ 0 + n = n
⊢ 0 + 0 = 0n✝:Nata✝:0 + n✝ = n✝⊢ 0 + (n✝ + 1) = n✝ + 1
case zero ⊢ 0 + 0 = 0 All goals completed! 🐙
case succ n ih n:Natih:0 + n✝ = n✝⊢ 0 + (n✝ + 1) = n✝ + 1 All goals completed! 🐙
end Hidden
다음은 몇 가지 추가 예제입니다.
namespace Hidden
inductive Nat where
| zero
| succ : Nat → Nat
def Nat.toNat : Nat → _root_.Nat
| .zero => .zero
| .succ n => .succ n.toNat
def Nat.ofNat : _root_.Nat → Nat
| .zero => .zero
| .succ n => .succ (.ofNat n)
def add (m n : Nat) : Nat :=
match n with
| Nat.zero => m
| Nat.succ n => Nat.succ (add m n)
instance : Add Nat where
add := add
instance : OfNat Nat n where
ofNat := .ofNat n
@[simp]
theorem zero_zero : (.zero : Nat) = 0 := rfl
theorem add_zero (n : Nat) : n + 0 = n := rfl
theorem add_succ (n k : Nat) : n + k.succ = (n + k).succ := rfl
open Nat
theorem zero_add (n : Nat) : 0 + n = n := n:Nat⊢ 0 + n = n
⊢ 0 + zero = zeroa✝:Nata_ih✝:0 + a✝ = a✝⊢ 0 + a✝.succ = a✝.succ ⊢ 0 + zero = zeroa✝:Nata_ih✝:0 + a✝ = a✝⊢ 0 + a✝.succ = a✝.succ All goals completed! 🐙
theorem succ_add (m n : Nat) : succ m + n = succ (m + n) := m:Natn:Nat⊢ m.succ + n = (m + n).succ
m:Nat⊢ m.succ + zero = (m + zero).succm:Nata✝:Nata_ih✝:m.succ + a✝ = (m + a✝).succ⊢ m.succ + a✝.succ = (m + a✝.succ).succ m:Nat⊢ m.succ + zero = (m + zero).succm:Nata✝:Nata_ih✝:m.succ + a✝ = (m + a✝).succ⊢ m.succ + a✝.succ = (m + a✝.succ).succ All goals completed! 🐙
theorem add_comm (m n : Nat) : m + n = n + m := m:Natn:Nat⊢ m + n = n + m
m:Nat⊢ m + zero = zero + mm:Nata✝:Nata_ih✝:m + a✝ = a✝ + m⊢ m + a✝.succ = a✝.succ + m m:Nat⊢ m + zero = zero + mm:Nata✝:Nata_ih✝:m + a✝ = a✝ + m⊢ m + a✝.succ = a✝.succ + m All goals completed! 🐙
theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) := m:Natn:Natk:Nat⊢ m + n + k = m + (n + k)
m:Natn:Nat⊢ m + n + zero = m + (n + zero)m:Natn:Nata✝:Nata_ih✝:m + n + a✝ = m + (n + a✝)⊢ m + n + a✝.succ = m + (n + a✝.succ) m:Natn:Nat⊢ m + n + zero = m + (n + zero)m:Natn:Nata✝:Nata_ih✝:m + n + a✝ = m + (n + a✝)⊢ m + n + a✝.succ = m + (n + a✝.succ) All goals completed! 🐙
end Hidden
induction 택틱은 여러 개의 대상(대전제라고도 합니다)을 갖는 사용자 정의 귀납법 원리도 지원합니다. 이 예제에서는 Nat.mod.inductionOn을 사용하며, 그 시그니처는 다음과 같습니다:
Nat.mod.inductionOn
{motive : Nat → Nat → Sort u}
(x y : Nat)
(ind : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y)
(base : ∀ x y, ¬(0 < y ∧ y ≤ x) → motive x y) :
motive x y
example (x : Nat) {y : Nat} (h : y > 0) : x % y < y := x:Naty:Nath:y > 0⊢ x % y < y
induction x, y using Nat.mod.inductionOn with
x:Naty:Nath₁:0 < y ∧ y ≤ xih:y > 0 → (x - y) % y < yh:y > 0⊢ x % y < y
x:Naty:Nath₁:0 < y ∧ y ≤ xih:y > 0 → (x - y) % y < yh:y > 0⊢ (x - y) % y < y
All goals completed! 🐙
x:Naty:Nath₁:¬(0 < y ∧ y ≤ x)h:y > 0⊢ x % y < y
x:Naty:Nath₁:¬(0 < y ∧ y ≤ x)h:y > 0this:¬0 < y ∨ ¬y ≤ x⊢ x % y < y
match this with
x:Naty:Nath₁✝:¬(0 < y ∧ y ≤ x)h:y > 0this:¬0 < y ∨ ¬y ≤ xh₁:¬0 < y⊢ x % y < y All goals completed! 🐙
x:Naty:Nath₁✝:¬(0 < y ∧ y ≤ x)h:y > 0this:¬0 < y ∨ ¬y ≤ xh₁:¬y ≤ x⊢ x % y < y
x:Naty:Nath₁✝:¬(0 < y ∧ y ≤ x)h:y > 0this:¬0 < y ∨ ¬y ≤ xh₁:¬y ≤ xhgt:y > x⊢ x % y < y
x:Naty:Nath₁✝:¬(0 < y ∧ y ≤ x)h:y > 0this:¬0 < y ∨ ¬y ≤ xh₁:¬y ≤ xhgt:y > x % y⊢ x % y < y
All goals completed! 🐙
택틱에서도 match 표기법을 사용할 수 있습니다:
example : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p
p:Propq:Proph:p ∨ q⊢ q ∨ p
match h with
p:Propq:Proph:p ∨ qh✝:p⊢ q ∨ p p:Propq:Proph:p ∨ qh✝:p⊢ p; All goals completed! 🐙
p:Propq:Proph:p ∨ qh2:q⊢ q ∨ p p:Propq:Proph:p ∨ qh2:q⊢ q; All goals completed! 🐙
편의를 위해 패턴 매칭은 intro, funext와 같은 택틱에도 통합되어 있습니다.
example : s ∧ q ∧ r → p ∧ r → q ∧ p := s:Propq:Propr:Propp:Prop⊢ s ∧ q ∧ r → p ∧ r → q ∧ p
s:Propq:Propr:Propp:Propleft✝:shq:qright✝¹:rhp:pright✝:r⊢ q ∧ p
All goals completed! 🐙
example :
(fun (x : Nat × Nat) (y : Nat × Nat) => x.1 + y.2)
=
(fun (x : Nat × Nat) (z : Nat × Nat) => z.2 + x.1) := ⊢ (fun x y => x.fst + y.snd) = fun x z => z.snd + x.fst
a:Natb:Natc:Natd:Nat⊢ (a, b).fst + (c, d).snd = (c, d).snd + (a, b).fst
a:Natb:Natc:Natd:Nat⊢ a + d = d + a
All goals completed! 🐙
귀납적 타입을 쉽게 다룰 수 있도록 설계된 마지막 택틱인 injection 택틱을 소개하며 이 절을 마무리합니다. 귀납적 타입의 원소는 설계상 자유롭게 생성됩니다. 다시 말해, 생성자는 단사이며 치역이 서로소입니다. injection 택틱은 이 사실을 활용하도록 설계되었습니다:
open Nat
example (m n k : Nat) (h : succ (succ m) = succ (succ n))
: n + k = m + k := m:Natn:Natk:Nath:m.succ.succ = n.succ.succ⊢ n + k = m + k
m:Natn:Natk:Nath':m + 1 = n + 1⊢ n + k = m + k
m:Natn:Natk:Nath'':m = n⊢ n + k = m + k
All goals completed! 🐙
이 택틱은 처음 적용될 때 문맥에 h' : m + 1 = n + 1을 추가하고, 두 번째로 적용될 때 h'' : m = n을 추가합니다.
injection 택틱은 서로 다른 생성자를 같다고 놓았을 때 생기는 모순도 감지하며, 이를 이용해 목표를 닫습니다.
open Nat
example (m n : Nat) (h : succ m = 0) : n = n + 7 := m:Natn:Nath:m.succ = 0⊢ n = n + 7
All goals completed! 🐙
example (m n : Nat) (h : succ m = 0) : n = n + 7 := m:Natn:Nath:m.succ = 0⊢ n = n + 7
All goals completed! 🐙
example (h : 7 = 4) : False := h:7 = 4⊢ False
All goals completed! 🐙
두 번째 예제에서 볼 수 있듯이, contradiction 택틱도 이러한 형태의 모순을 감지합니다.
7.7. 귀납적 족
이제 Lean이 허용하는 귀납적 정의의 전체 범위에 대한 설명이 거의 끝나 갑니다. 지금까지 Lean에서는 재귀 생성자를 몇 개든 가진 귀납적 타입을 도입할 수 있음을 살펴보았습니다. 사실 하나의 귀납적 정의로 인덱스가 붙은 귀납적 타입의 족(family)을 도입할 수도 있으며, 그 방법을 지금부터 설명하겠습니다.
귀납적 족(inductive family)은 다음과 같은 형태의 동시 귀납법으로 정의되는, 인덱스가 붙은 타입들의 족입니다.
inductive foo : ... → Sort u where | constructor₁ : ... → foo ... | constructor₂ : ... → foo ... ... | constructorₙ : ... → foo ...
일반적인 귀납적 정의는 어떤 Sort u의 원소를 구성하지만, 이보다 더 일반적인 형태는 함수 ... → Sort u를 구성합니다. 여기서 “...”는 인자 타입들의 나열을 나타내며, 이를 인덱스라고도 부릅니다. 이때 각 생성자는 이 족(family)에 속한 어떤 구성원의 원소를 구성합니다. 한 예로 Vect α n의 정의가 있습니다. 이는 α의 원소들로 이루어진 길이 n의 벡터 타입입니다:
inductive Vect (α : Type u) : Nat → Type u where
| nil : Vect α 0
| cons : α → {n : Nat} → Vect α n → Vect α (n + 1)
cons 생성자는 Vect α n의 원소를 받아 Vect α (n + 1)의 원소를 반환한다는 점에 주목하십시오. 즉, 이 생성자는 타입 족의 한 구성원에 속하는 원소를 사용하여 다른 구성원의 원소를 만듭니다.
더 특이한 예로 Lean의 상등 타입 정의를 들 수 있습니다.
고정된 각 α : Sort u와 a : α에 대해, 이 정의는 x : α로 인덱싱되는 타입족 Eq a x를 구성합니다. 그러나 주목할 점은 생성자가 refl 하나뿐이며, 이것이 Eq a a의 원소라는 것입니다. 직관적으로, Eq a x의 증명을 구성하는 유일한 방법은 x가 a인 경우에 반사성을 사용하는 것입니다. Eq a a는 타입족 Eq a x에서 원소를 가지는 유일한 타입이라는 점에 유의하십시오. Lean이 생성하는 제거 원리는 다음과 같습니다.
set_option pp.proofs true
universe u v
#check (@Eq.rec : {α : Sort u} → {a : α} →
{motive : (x : α) → a = x → Sort v} →
motive a rfl →
{b : α} → (h : a = b) → motive b h)
상등에 관한 기본 공리가 모두 생성자 refl과 제거자 Eq.rec로부터 도출된다는 것은 주목할 만한 사실입니다. 그러나 상등의 정의는 일반적이지 않습니다. 공리적 세부 사항의 논의를 참고하십시오.
재귀자 Eq.rec는 치환을 정의하는 데에도 사용됩니다:
namespace Hidden
theorem subst {α : Type u} {a b : α} {p : α → Prop}
(h₁ : Eq a b) (h₂ : p a) : p b :=
Eq.rec (motive := fun x _ => p x) h₂ h₁
end Hidden
match를 사용하여 subst를 정의할 수도 있습니다.
namespace Hidden
theorem subst {α : Type u} {a b : α} {p : α → Prop}
(h₁ : Eq a b) (h₂ : p a) : p b :=
match h₁ with
| rfl => h₂
end Hidden
사실 Lean은 match 표현식을 Eq.casesOn이나 Eq.ndrec 같이 자동 생성된 보조 정의에 기반한 정의로 컴파일하며, 이 보조 정의들 자체도 Eq.rec을 사용하여 정의되어 있습니다.
theorem subst {α : Type u} {a b : α} {p : α → Prop}
(h₁ : a = b) (h₂ : p a) : p b :=
match h₁ with
| rfl => h₂
set_option pp.all true
#print subst
#print subst.match_1_1
#print Eq.casesOn
#print Eq.ndrec
재귀자나 match를 h₁ : a = b와 함께 사용하면 a와 b가 같다고 가정할 수 있으며, 이 경우 p b와 p a는 같습니다.
Eq가 대칭적이고 추이적이라는 것은 어렵지 않게 증명할 수 있습니다. 다음 예제에서는 symm을 증명하고, trans와 congr(합동) 정리는 연습 문제로 남겨 둡니다.
namespace Hidden
variable {α β : Type u} {a b c : α}
theorem symm (h : Eq a b) : Eq b a :=
match h with
| rfl => rfl
theorem trans (h₁ : Eq a b) (h₂ : Eq b c) : Eq a c :=
sorry
theorem congr (f : α → β) (h : Eq a b) : Eq (f a) (f b) :=
sorry
end Hidden
타입 이론 문헌에는 귀납적 정의를 더 일반화한 원리들이 있습니다. 예를 들어 귀납-재귀(induction-recursion) 원리와 귀납-귀납(induction-induction) 원리가 있습니다. Lean은 이러한 원리를 지원하지 않습니다.
7.8. 공리적 세부 사항
지금까지 예제를 통해 귀납적 타입과 그 구문을 설명했습니다. 이 절에서는 공리적 기초에 관심이 있는 독자를 위해 추가 정보를 제공합니다.
귀납적 타입의 생성자는 매개변수—직관적으로는 귀납적 구성 전체에 걸쳐 고정된 채로 유지되는 인자—와 인덱스, 즉 동시에 구성되고 있는 타입 족을 매개화하는 인자를 받는다는 것을 살펴보았습니다. 각 생성자는 타입을 가져야 하며, 이때 인자 타입은 이전에 정의된 타입, 매개변수 타입과 인덱스 타입, 그리고 현재 정의 중인 귀납적 족으로부터 구성됩니다. 요구 사항은 후자가 조금이라도 나타난다면 오직 엄격하게 양성적으로만 나타나야 한다는 것입니다. 이는 단순히 해당 귀납적 족이 나타나는 생성자의 모든 인자가 의존 화살표 타입이어야 하며, 그 타입에서 정의 중인 귀납적 타입은 결과 타입으로만 나타나고, 인덱스는 상수와 이전 인자들로 이루어진 항으로 주어져야 한다는 뜻입니다.
귀납적 타입은 어떤 u에 대해 Sort u에 속하므로, u가 어떤 유니버스 레벨로 인스턴스화될 수 있는지 묻는 것은 합당합니다. 귀납적 타입 족 C의 정의에 있는 각 생성자 c는 다음과 같은 형태입니다.
c : (a : α) → (b : β[a]) → C a p[a,b]
여기서 a는 데이터 타입 매개변수의 나열이고, b는 생성자에 대한 인수의 나열이며, p[a, b]는 인덱스로, 해당 구성이 귀납적 족의 어느 원소에 속하는지를 결정합니다. (이 설명은 다소 오해의 소지가 있다는 점에 유의하십시오. 의존 관계가 성립하기만 한다면 생성자의 인수는 어떤 순서로든 나타날 수 있기 때문입니다.) C의 유니버스 레벨에 대한 제약은 귀납적 타입이 Prop(즉, Sort 0)에 속하도록 지정되었는지 여부에 따라 두 가지 경우로 나뉩니다.
먼저 귀납적 타입이 Prop에 속하도록 지정되지 않은 경우를 살펴봅시다. 이 경우 유니버스 레벨 u는 다음 조건을 만족하도록 제약됩니다:
위와 같은 각 생성자
c와 시퀀스β[a]에 속한 각βk[a]에 대해,βk[a] : Sort v이면u≥v가 성립합니다.
다시 말해, 유니버스 레벨 u는 생성자의 인자를 나타내는 각 타입의 유니버스 레벨보다 크거나 같아야 합니다.
귀납적 타입이 Prop에 속하도록 지정된 경우, 생성자 인자의 유니버스 레벨에는 아무런 제약이 없습니다. 하지만 이러한 유니버스 레벨은 제거 규칙에 영향을 미칩니다. 일반적으로 Prop에 속하는 귀납적 타입의 경우, 제거 규칙의 모티브는 Prop에 속해야 합니다.
이 마지막 규칙에는 예외가 있습니다. 생성자가 하나뿐이고 각 생성자 인자가 Prop에 속하거나 인덱스인 경우에는, 귀납적으로 정의된 Prop에서 임의의 Sort로 소거하는 것이 허용됩니다. 이 경우의 직관은, 제거가 인자의 타입에 원소가 존재한다는 사실 자체로 이미 주어진 정보 외에는 어떤 정보도 사용하지 않는다는 것입니다. 이 특수한 경우를 싱글톤 소거(singleton elimination)라고 합니다.
귀납적으로 정의된 상등 타입의 제거자인 Eq.rec를 적용할 때 싱글턴 제거가 작동하는 것을 이미 보았습니다. p a와 p b가 임의의 타입이더라도 원소 h : Eq a b를 사용하여 원소 h₂ : p a를 p b로 캐스트할 수 있습니다. 캐스트는 새로운 데이터를 만들어 내지 않고 이미 가진 데이터를 다시 해석할 뿐이기 때문입니다. 싱글턴 제거는 이종 상등과 정초 재귀에도 사용되며, 이에 대해서는 귀납법과 재귀에 관한 장에서 다룰 것입니다.
7.9. 상호 귀납적 타입과 중첩 귀납적 타입
이제 자주 유용하게 쓰이는 귀납적 타입의 두 가지 일반화를 살펴보겠습니다. Lean은 이들을 앞에서 설명한 더 기본적인 종류의 귀납적 타입으로 “컴파일”하여 지원합니다. 다시 말해, Lean은 더 일반적인 정의를 파싱하고, 이를 바탕으로 보조 귀납적 타입을 정의한 다음, 그 보조 타입을 사용하여 우리가 실제로 원하는 타입을 정의합니다. 다음 장에서 설명할 Lean의 등식 컴파일러가 있어야 이 타입들을 효과적으로 활용할 수 있습니다. 그럼에도 이러한 선언은 일반적인 귀납적 정의를 간단히 변형한 것이므로 여기서 설명하는 것이 타당합니다.
먼저, Lean은 상호 정의된 귀납적 타입을 지원합니다. 두 개(또는 그 이상)의 귀납적 타입을 동시에 정의하면서 각 타입이 다른 타입을 참조하도록 할 수 있다는 것이 그 핵심입니다.
mutual
inductive Even : Nat → Prop where
| even_zero : Even 0
| even_succ : (n : Nat) → Odd n → Even (n + 1)
inductive Odd : Nat → Prop where
| odd_succ : (n : Nat) → Even n → Odd (n + 1)
end
이 예제에서는 두 타입이 동시에 정의됩니다. 자연수 n은 0이거나 Odd인 수보다 1 크면 Even이고, Even인 수보다 1 크면 Odd입니다. 아래 연습 문제에서는 세부 사항을 자세히 풀어 써 보게 됩니다.
상호 귀납적 정의는 노드가 α의 원소로 레이블된 유한 트리의 표기법을 정의하는 데에도 사용할 수 있습니다:
mutual
inductive Tree (α : Type u) where
| node : α → TreeList α → Tree α
inductive TreeList (α : Type u) where
| nil : TreeList α
| cons : Tree α → TreeList α → TreeList α
end
이 정의에 따르면, α의 원소 하나와 (비어 있을 수도 있는) 부분 트리의 리스트를 함께 제공하여 Tree α의 원소를 구성할 수 있습니다. 부분 트리의 리스트는 TreeList α 타입으로 표현되며, 이 타입은 빈 리스트인 nil이거나, 트리 하나와 TreeList α의 원소 하나에 cons를 적용한 것으로 정의됩니다.
하지만 이 정의는 다루기가 불편합니다. 하위 트리의 리스트가 List (Tree α) 타입으로 주어진다면 훨씬 좋을 것입니다. 특히 Lean의 라이브러리에는 리스트를 다루는 함수와 정리가 많이 들어 있기 때문입니다. TreeList α 타입이 List (Tree α)와 동형이라는 것을 보일 수는 있지만, 이 동형 사상을 따라 결과를 앞뒤로 옮기는 일은 번거롭습니다.
사실 Lean에서는 우리가 정말로 원하는 귀납적 타입을 정의할 수 있습니다:
inductive Tree (α : Type u) where
| mk : α → List (Tree α) → Tree α
이를 중첩 귀납적 타입이라고 합니다. Tree가 mk의 인자들 사이에 엄격하게 양성적으로 나타나지 않고 오히려 List 타입 생성자 안에 중첩되어 있으므로, 이는 앞 절에서 제시한 귀납적 타입의 엄격한 명세를 벗어납니다. 그런 다음 Lean은 커널에서 TreeList α와 List (Tree α) 사이의 동형을 자동으로 구성하고, 이 동형을 사용한 항으로 Tree의 생성자들을 정의합니다.
7.10. 연습 문제
-
곱셈, 선행자 함수(
pred 0 = 0), 절삭 뺄셈(m이n보다 크거나 같을 때n - m = 0), 거듭제곱 등 자연수에 대한 다른 연산을 정의해 보십시오. 그런 다음 이미 증명한 정리들을 바탕으로 이 연산들의 기본 성질 몇 가지를 증명해 보십시오.이 중 상당수는 이미 Lean의 코어 라이브러리에 정의되어 있으므로, 이름 충돌을 피하려면
Hidden이나 그와 비슷한 이름의 네임스페이스 안에서 작업해야 합니다. -
length함수나reverse함수와 같이 리스트에 대한 몇 가지 연산을 정의하십시오. 다음과 같은 몇 가지 성질을 증명하십시오.a.
length (xs ++ ys) = length xs + length ysb.
length (reverse xs) = length xsc.
reverse (reverse xs) = xs -
다음 생성자들로 만들어지는 항으로 구성된 귀납적 데이터 타입을 정의하십시오:
변수에 대한 값 할당이 주어졌을 때 그러한 항을 평가하는 함수를 재귀적으로 정의하십시오.
-
마찬가지로, 명제 논리식의 타입과 함께 그러한 논리식 타입에 대한 함수들, 즉 평가 함수, 논리식의 복잡도를 측정하는 함수들, 그리고 주어진 변수를 다른 논리식으로 치환하는 함수를 정의하십시오.