정리 증명

정리 증명 (Theorem Proving)

동등성 (Equality)

Idris는 명제 동등성(propositional equalities)의 선언을 허용해, 프로그램에 대한 정리를 진술하고 증명할 수 있게 해줘요. 동등성은 내장되어 있지만, 개념적으로 다음 정의를 가져요:

data (=) : a -> b -> Type where
   Refl : x = x

동등성은 어떤 타입의 어떤 값들 사이에서도 제안될 수 있지만, 동등성 증명을 구성하는 유일한 방법은 값들이 실제로 같을 때뿐이에요. 예를 들어:

fiveIsFive : 5 = 5
fiveIsFive = Refl

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl

빈 타입 (The Empty Type)

생성자가 없는 빈 타입 \(\bot\)이 있어요. 따라서 빈 타입의 원소를 구성하는 것은 불가능해요 — 적어도 부분 정의되거나 일반 재귀적인 함수를 사용하지 않고서는요 (자세한 내용은 Totality Checking 절 참조). 따라서 빈 타입을 사용해 어떤 것이 불가능함을 증명할 수 있어요. 예를 들어 0은 결코 후임자(successor)와 같지 않다는 것을요:

disjoint : (n : Nat) -> Z = S n -> Void
disjoint n p = replace {P = disjointTy} p ()
  where
    disjointTy : Nat -> Type
    disjointTy Z = ()
    disjointTy (S k) = Void

이 함수가 어떻게 작동하는지 지나치게 걱정할 필요는 없어요 — 본질적으로, 라이브러리 함수 replace를 적용하는데, 이는 동등성 증명을 사용해 술어(predicate)를 변환해요. 여기서는 존재할 수 없는 것에 대한 증명을 사용해, 존재할 수 있는 타입(빈 튜플)의 값을 존재할 수 없는 타입의 값으로 변환해요.

빈 타입의 원소를 갖게 되면 무엇이든 증명할 수 있어요. void는 모순에 의한 증명(proofs by contradiction)을 돕기 위해 라이브러리에 정의돼 있어요.

void : Void -> a

간단한 정리 (Simple Theorems)

의존 타입을 타입 검사할 때 타입 자체가 정규화돼요. 그래서 plus의 축소(reduction) 동작에 대한 다음 정리를 증명하고 싶다고 상상해보세요:

plusReduces : (n:Nat) -> plus Z n = n

우리는 프로그램의 타입을 쓰는 것과 똑같은 방식으로 정리의 진술을 타입으로 적어 내려놨어요. 사실 증명과 프로그램 사이에 진짜 구분은 없어요. 여기서 우리가 보는 한 증명은 단지 관심 있는 특정 속성을 보장할 만큼 충분히 정밀한 타입을 가진 프로그램에 불과해요.

여기서 세부 사항은 다루지 않겠지만, Curry-Howard 대응(Curry-Howard correspondence) [1]이 이 관계를 설명해요. plus Z n이 plus의 정의에 의해 n으로 정규화되므로 증명 자체는 사소해요:

plusReduces n = Refl

인자를 반대 방향으로 시도하면 조금 더 어려워요. plus가 첫 번째 인자에 대해 재귀적으로 정의되기 때문이에요. 증명도 plus의 첫 번째 인자인 n에 대해 재귀적으로 작동해요.

plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = Refl
plusReducesZ (S k) = cong (plusReducesZ k)

cong는 동등성이 함수 적용을 존중함을 진술하는 라이브러리에 정의된 함수예요:

cong : {f : t -> u} -> a = b -> f a = f b

후임자에 대한 plus의 축소 동작에 대해서도 같은 것을 할 수 있어요:

plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS Z m = Refl
plusReducesS (S k) m = cong (plusReducesS k m)

이런 사소한 정리조차도, 증명을 한 번에 구성하는 것은 약간 까다로워요. 상황이 조금만 더 복잡해져도 "배치 모드(batch mode)"로 증명을 구성하는 것은 생각할 것이 너무 많아져요.

Idris는 증명 구축을 도울 수 있는 대화형 편집 기능을 제공해요. 에디터에서 대화형으로 증명을 구축하는 자세한 내용은 Theorem Proving을 참조하세요.

실전의 정리 (Theorems in Practice)

정리를 증명해야 할 필요는 실제로 자연스럽게 발생할 수 있어요. 예를 들어 앞서 (Views and the "with" rule) parity 함수를 사용해 natToBin을 구현했어요:

parity : (n:Nat) -> Parity n

하지만 parity에 대한 정의는 제공하지 않았어요. 대략 다음과 같을 것이라고 기대할 수 있어요:

parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = Even {n=S j}
  parity (S (S (S (j + j)))) | Odd  = Odd {n=S j}

안타깝게도 이는 타입 오류로 실패해요:

When checking right hand side of with block in views.parity with expected type
        Parity (S (S (j + j)))

Type mismatch between
        Parity (S j + S j) (Type of Even)
and
        Parity (S (S (plus j j))) (Expected type)

문제는 Even의 타입에서 S j + S j를 정규화해도 Parity의 오른쪽 타입에 필요한 것이 나오지 않는다는 것이에요. 우리는 S (S (plus j j))가 S j + S j와 같을 것임을 알지만, 그것을 증명으로 Idris에 설명해야 해요. 정의에 홀(holes, Holes 참조)을 추가하는 것부터 시작할 수 있어요:

parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = let result = Even {n=S j} in
                                          ?helpEven
  parity (S (S (S (j + j)))) | Odd  = let result = Odd {n=S j} in
                                          ?helpOdd

helpEven의 타입을 검사하면 Even 경우에 무엇을 증명해야 하는지 보여줘요:

  j : Nat
  result : Parity (S (plus j (S j)))
--------------------------------------
helpEven : Parity (S (S (plus j j)))

따라서 타입을 필요한 형태로 다시 쓰는 헬퍼 함수를 작성할 수 있어요:

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p

rewrite ... in 문법은 동등성 증명에 따라 식을 다시 써서 식의 요구 타입을 바꾸는 것을 허용해요. 여기서는 다음 타입을 가진 plusSuccRightSucc를 사용했어요:

plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right

helpEven의 오른쪽을 홀로 바꾸고 단계별로 작업함으로써 rewrite의 효과를 볼 수 있어요. 다음에서 시작해요:

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = ?helpEven_rhs

helpEven_rhs의 타입을 볼 수 있어요:

  j : Nat
  p : Parity (S (plus j (S j)))
--------------------------------------
helpEven_rhs : Parity (S (S (plus j j)))

그 다음 plusSuccRightSucc j j를 적용해 다시 쓰면, 방정식 S (j + j) = j + S j를 주고, 따라서 타입의 S (j + j) (이 경우에는 S (plus j j) — S (j + j)가 그렇게 축소되므로)를 j + S j로 바꿔요:

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs

이제 helpEven_rhs의 타입을 검사하면 무슨 일이 일어났는지 보여줘요. 방금 사용한 방정식의 타입(_rewrite_rule의 타입으로서)을 포함해요:

  j : Nat
  p : Parity (S (plus j (S j)))
  _rewrite_rule : S (plus j j) = plus j (S j)
--------------------------------------
helpEven_rhs : Parity (S (plus j (S j)))

rewrite와 Odd 경우에 대한 또 다른 헬퍼를 사용해, parity를 다음과 같이 완성할 수 있어요:

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p

helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p

parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})
  parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})

rewrite에 대한 완전한 세부 사항은 이 입문 튜토리얼의 범위를 넘지만, 정리 증명 튜토리얼(Theorem Proving 참조)에서 다루어져 있어요.

전체성 검사 (Totality Checking)

증명을 정말로 신뢰하고 싶다면, 그것들이 전체 함수(total functions) — 즉 모든 가능한 입력에 대해 정의되고 종료가 보장되는 함수 — 로 정의되는 것이 중요해요. 그렇지 않으면 빈 타입의 원소를 구성할 수 있고, 그로부터 무엇이든 증명할 수 있게 돼요:

-- making use of 'hd' being partially defined
empty1 : Void
empty1 = hd [] where
    hd : List a -> a
    hd (x :: xs) = x

-- not terminating
empty2 : Void
empty2 = empty2

내부적으로 Idris는 모든 정의에 대해 전체성을 검사하며, 프롬프트에서 :total 명령으로 확인할 수 있어요. 위의 두 정의 모두 전체적이지 않다는 것을 볼 수 있어요:

*Theorems> :total empty1
possibly not total due to: empty1#hd
    not total as there are missing cases
*Theorems> :total empty2
possibly not total due to recursive path empty2

"possibly(아마도)"라는 단어의 사용을 유의하세요 — 물론 정지 문제(halting problem)의 결정 불가능성 때문에 전체성 검사는 확실할 수 없어요. 따라서 검사는 보수적이에요. 또한 함수를 전체로 표시해 전체성 검사 실패가 컴파일 타임 오류가 되게 하는 것도 (증명의 경우 바람직하고 실제로 권장되는) 가능해요:

total empty2 : Void
empty2 = empty2

Type checking ./theorems.idr
theorems.idr:25:empty2 is possibly not total due to recursive path empty2

안심스럽게도, The Empty Type 절에서 0과 후임자 생성자가 분리되었음을 증명한 우리의 증명은 전체적이에요:

*theorems> :total disjoint
Total

전체성 검사는 필연적으로 보수적이에요. 전체로 기록되려면 함수 f는 다음을 해야 해요:

  • 모든 가능한 입력을 덮음

  • 잘-기반(well-founded)이어야 함 — 즉 (어쩌면 상호) 재귀 호출들의 수열이 다시 f에 도달할 때쯤엔, 인자 중 하나가 감소했음을 보일 수 있어야 함.

  • 엄격히 양수(strictly positive)가 아닌 데이터 타입을 사용하지 않아야 함

  • 비전체 함수를 호출하지 않아야 함

전체성 지시어와 컴파일러 플래그 (Directives and Compiler Flags for Totality)

기본적으로 Idris는 전체적이든 아니든 모든 잘 타입된 정의를 허용해요. 하지만 가능한 한 함수가 전체적인 것이 바람직해요. 이는 모든 가능한 입력에 대해 유한한 시간 안에 결과를 제공한다는 보장을 주기 때문이에요. 전체 함수를 요구 사항으로 만들 수 있어요:

  • --total 컴파일러 플래그를 사용하거나.

  • 소스 파일에 %default total 지시어를 추가함. 이후의 모든 정의는 명시적으로 partial로 표시되지 않는 한 전체적이어야 함.

%default total 선언 이후의 모든 함수는 전체적이어야 해요. 그에 따라 %default partial 선언 이후에는 요구 사항이 완화돼요.

마지막으로, 컴파일러 플래그 --warnpartial는 선언되지 않은 부분 함수에 대해 경고를 출력하게 해요.

전체성 검사 문제 (Totality checking issues)

전체성 검사기는 완벽하지 않다는 점을 유의하세요! 첫째, 정지 문제의 결정 불가능성 때문에 필연적으로 보수적이어서, 전체적인 많은 프로그램이 그렇게 감지되지 않을 거예요. 둘째, 현재 구현에는 지금까지 투입된 노력이 제한적이어서, 전체적이지 않은 함수를 전체적이라고 믿는 경우가 여전히 있을 수 있어요. 아직 증명에 의존하지 마세요!

전체성을 위한 힌트 (Hints for totality)

프로그램이 전체적이라고 믿지만 Idris가 동의하지 않는 경우, 종료 인자에 대해 더 많은 세부 사항을 주도록 검사기에 힌트를 주는 것이 가능해요. 검사기는 모든 재귀 호출 체인이 결국 기본 경우를 향해 감소하는 인자 중 하나로 이어지도록 보장함으로써 작동하지만, 때로는 이것을 발견하기 어려워요. 예를 들어 다음 정의는 검사기가 filter (< x) xs가 항상 (x :: xs)보다 작을 것이라고 결정할 수 없기 때문에 전체로 검사될 수 없어요:

qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
   = qsort (filter (< x) xs) ++
      (x :: qsort (filter (>= x) xs))

프렐류드에 정의된 함수 assert_smaller는 이 문제를 다루기 위한 것이에요:

assert_smaller : a -> a -> a
assert_smaller x y = y

이것은 단순히 두 번째 인자로 평가되지만, 전체성 검사기에게 y가 x보다 구조적으로 더 작다고 단언(assert)해요. 검사기가 스스로 알아낼 수 없을 때 전체성의 추론을 설명하는 데 사용될 수 있어요. 위의 예는 이제 다음과 같이 작성될 수 있어요:

total
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
   = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
      (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))

식 assert_smaller (x :: xs) (filter (<= x) xs)는 filter의 결과가 항상 패턴 (x :: xs)보다 작을 것임을 단언해요.

더 극단적인 경우, assert_total 함수는 부분식을 항상 전체적이라고 표시해요:

assert_total : a -> a
assert_total x = x

일반적으로 이 함수는 피해야 하지만, 전체성이 외부 인자로 보일 수 있는 프리미티브나 외부 정의 함수(예: C 라이브러리)에 대해 추론할 때 매우 유용할 수 있어요.

[1]

Timothy G. Griffin. 1989. A formulae-as-type notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714 http://doi.acm.org/10.1145/96709.96714

출처: 문서