<Interactive Theorem Proving and Program Development>라는 책을 추천받아 조금씩 읽어보기로 했다. 첫 장에서는 Coq에 대한 간단한 안내를 진행한다. 책의 순서를 따라가면서 하나씩 알아보자

타입

먼저 Coq에서는 Gallina라는 언어를 사용해 요구사항(Specification)을 서술한다. 대부분의 다른 프로그래밍 언어들과 마찬가지로 타입은 declaration과 typing rule에 의해 정해진다.

  • declaration : type Z 에 대해 이 타입의 변수 z를 선언
  • typing rule : type Z에 속하는 변수 z와 -6이 있으면 -6z는 type Z

또한 기본 타입(primitive type) A, B로부터 새로운 타입을 만들어내는 것 또한 가능하다

  • type A x B : a가 type A, b가 type B일 때 (a, b)의 타입
  • type A🡒B : type A에 속하는 a를 받아 type B에 속하는 b를 내놓는 함수의 타입

하스켈의 Currying에 익숙하다면 다음과 같이 좀더 복잡한 타입을 정의할 수도 있다.

Q. \(f:\mathrm{N}\rightarrow \mathrm{Z}, n \in \mathrm{N}\)을 받아 \( \sum_{i=0}^{i=n} f(i) \)를 반환하는 함수의 타입은?

A. (nat🡒Z)🡒nat🡒Z

Proposition과 Proof

Proposition

Coq가 다른 프로그래밍 언어들과 다른 점은 다루고자 하는 대상에 대한 표명(assertion)을 표현할 수 있다는 점이다. 단순한 수학적 object에서부터 프로그램 자체에 이르기까지 다양한 대상에 대한 표현이 가능하다는 점에 유의하자. 이런 assertion(혹은 proposition)의 예로는 다음을 들 수 있다.

  • 3 ≤ 8

  • 8 ≤ 3

  • “for all n>1, the sequence of integers defined by

    \[{\begin{matrix} u_0 = n \\ u_{i+1}={\begin{Bmatrix}{u_i \over 2},&{\mbox{if }}u_i{\mbox{ is even}}\\3u_i+1,&{\mbox{if }}u_i{\mbox{ is odd}}\end{Bmatrix}} \end{matrix}}\]

    ultimately reaches the value 1”

  • “list concatenation is associative”

  • “the algorithm insertion_sort is a correct sorting method”

이들 중 일부는 참, 거짓 여부를 쉽게 알 수 있고 일부는 아직 참 여부가 밝혀지지 않았지만 모두 명확한 명제(well-formed proposition)이다. 그렇다면 이런 명제들이 참임은 어떻게 알 수 있을까?

Proof

어떤 명제가 참임을 보이는 가장 좋은 방법은 그 명제에 대한 증명을 보여주는 것이다. 사실 Sound한 체계에서만 그렇다. 문제는, 제시된 증명이 올바른지 판단하려면 해당 증명은 complete하고 readable해야 한다는 점이다. 그리고 대부분의 경우 자연어로 된 수많은 증명은 이를 만족하지 않는다. 이런 문제를 해결하기 위해 다음과 같은 해결책이 제시되었다.

  • 자연어는 모호하다

    🡒 증명을 위한 formal language를 설계하고, proof theory의 rule들을 이용해 증명을 서술한다

  • 그렇게 formal language로 서술된 증명은 (너무 길어서) 검증이 수고스럽다

    🡒 formal rule이 제대로 사용되었는지 검증하는 verification 과정을 자동화한다

  • formal language로 서술된 증명은 (너무 길어서) 처음 증명을 작성하기도 힘들다

    🡒 formal proof를 작성하는 단계에서부터 자동화 도구(proof assistant)의 도움을 받는다

자동화 도구에서 proof generator가 아니라 proof assistant 라는 표현에 유의하자. 안타깝게도 증명의 모든 과정을 자동화할 수 있는 방법은 존재하지 않는다. 따라서 Coq는 사용자가 전제 증명을 작은 lemma들로 쪼개고 각각에 대해 적절한 증명전략(tactic)을 선택하는 interactive한 방식으로 동작하게 된다.

Proposition과 Type

증명을 작성할 때는 어떤 언어를 사용하는 것이 좋을까. 증명(proof)과 프로그램(program)은 같은 formal한 방법으로 서술될 수 있다. 양쪽 모두 Church가 고안해낸 typed λ-calculus를 통해 서술될 수 있으며, Coq는 이 typed λ-calculus에서 좀더 다양한 서술을 가능하게 만든 Calculus of Inductive Constructions라는 체계를 사용한다.

책의 3장에서 Curry-Howard isomorphism을 통해 proof와 program의 관계를 설명하지만 그건 일단 나중으로 미루고, program과 (그 program의) type 사이의 관계는 proof와 (그 proof가 증명하는) statement의 관계와 같다는 점에 유의하자. 이를 이용하면 proof를 검증하는 과정은 type verification algorithm과 크게 다를 바가 없음을 이해할 수 있다.

모든 type은 해당 타입의 term(객체)을 가진다. Calculus of Inductive Costruction의 핵심은 “type은 type이면서 그 자체로 어떤 type을 가지는 term이다”라는 말을 이해하는 것이다. proposition의 타입을 Prop이라고 하고 예시를 통해 이 말의 의미를 살펴보자

  • Proposition “3 ≤ 7”은
    • type Prop을 가지는 term 이면서
    • (3≤7임을 보이는 증명)의 type 이 된다.
      • 이때 (3≤7임을 보이는 어떤 증명 A)는 type 3≤7의 term 이 된다

또한 술어논리의 술어(predicate)에도 적절한 타입을 부여할 수 있다.

  • “to be a prime number”의 타입 : nat🡒Prop
  • “to be a sorted list”의 타입 : (list Z)🡒Prop
  • binary relation ≤ 의 타입 : Z🡒Z🡒Prop
  • “to be a transitive relation”의 타입 : (Z🡒Z🡒Prop)🡒Prop

여기서는 type Z를 예시로 사용했지만, 임의의 타입을 변수 A로 나타내 polymorphic type을 표현하는 것 또한 가능함을 알아두자.

Specification과 Certified Programs

Coq에서 프로그램의 타입은 데이터가 지켜야 할 제약조건들을 propositions으로 나타내 포함할 수 있다. 예로 “a prime number tha divides n(of type nat)”이라는 type을 보자. 이는 다음과 같이 두 부분으로 나눌 수 있다.

  • computation-related part : “a value of type nat”
  • logical part : “this value is prime and divides n”

이는 결국 n에 의존하게 되며, 이런 종류의 타입을 dependent type이라고 한다. Coq의 표현력에는 이런 dependent type의 존재가 큰 몫을 차지한다고 한다. 책을 좀더 읽어봐야 이해할 수 있을듯.

같은 맥락에서 “n>1을 받아 n의 소인수를 반환하는 함수”의 타입을 Coq 안에서 표현할 수 있다. 이 타입에 해당하는 함수는 입력 n이 조건(nat 타입이고 n>1)을 만족하면 언제나 n의 소인수를 반환한다. Coq의 interactive help를 이용해 이런 함수를 실제로 만들어낼 수 있으며, 이렇게 만들어진 결과물을 certified program이라고 한다. certified program은 크게 두 부분으로 이루어져 있다.

  • computing information : 어떻게 n의 소인수를 계산해낼 것인가
  • proof : 그렇게 계산하면 왜 n의 소인수가 나오는가

일단 certified program을 만들고 나면 extraction algorithm을 통해 이를 실제 돌아가는 프로그램의 코드(주로 OCAML 등을 이용한다)로 변환해낼 수 있다. 이렇게 변환된 프로그램은 (증명을 했으므로) 안전함을 보장받을 수 있으며, 최종 결과물에는 proof에 대한 논리전개는 모두 제거되고 실제 동작에 필요한 ‘계산을 어떻게 수행하는가’에 대한 정보만 남게 된다.