1. 서 론

*본 연구는 한국과학재단 핵심전문연구 (과제번호: 971-0903-024-2)의 지원에 의한 것임.

논리 프로그래밍 언어와 같이 순수 논리만 이용한 정리 증명기에서 원자 식까지는 삭제 규칙(Elimination Rule)에 의해 분해하여 추론할 수 있지만  원자 식을 분해하여 추론하는 것이 불가능하다. 즉 원자 식의 진리를 판단하기 위해서는 이 원자 식이 주어진 도메인 상에서 참인지 거짓인지를 계산을 하여야 한다. 예를 들면, 자연수가 도메인인 논리에서 □2+3=5□은 논리연산자가 없으므로 원자 식이다. 이 시스템에서 추론을 계속하기 위해서는 이 원자 식이 참인지 거짓인지를 판단해야 하지만 순수 논리 시스템이라면 판단할 근거가 없다. 이런 추론을 인간이 한다면 2+3을 계산을 하여 이것이 5라는 것을 판단할 수 있을 것이다.

본 연구에서는 위와 같은 순수 논리 시스템을 보완하기 위해 Luo의 CC[2]에 있는 수축 이론적 의미론(Reductional Semantics)[4]을 이용하여 정리증명을 하고, 또 정리 증명과 (순환적) 계산이 자연스럽게 융화될 수 있다는 것을 보였다.

2. 의존적 타입공간(Dependent Type Space)과 타입

본 논문에서는 수학적인 증명을 검사하는 기계에 대해서 논한다.

2.1 곱(Products)

2.1.1 카티션곱(Catesian Product)

[eqn: B_1, cdots, B_n]이 집합이라면, 카티션곱은

[eqn: B_1 TIMES □ TIMES B_n =PI _{i=1 } ^n B_i ="{"(b_1 ,□,b_n ) | b_i in B_i , 1 <= i <= n "}"].

2.1.2 집합 [eqn: B_a]들의 [eqn: a in A]에 의해 색인된 일반곱

[eqn: PI_{a in A} B_a ="{" (b_a )_{a in A} | b_a in B_a "}"]

이것은 무한 튜플이고, 다음과 같이 함수로 표현할 수 있다.

[eqn: PI_{a in A} B_a ="{" f:A -> CUP _{ a in A} B_a | f(a) in B_a "}"]

곱의 삭제규칙은 투사(projection)이므로 응용으로 표현할 수 있다. 즉, [eqn: p in PI_{a in A} B_a] 일 때 [eqn: p_a =pa in B_a]를 p 의 a 번째 요소로 생각할 수 있다.

2.2 곱과 타입

합접(conjunction)은 곱 타입으로 볼 수 있다. 즉

[eqn: A wedge B =A TIMES B]

따라서 삭제는 투사에 의한다. lft() 와 rht()이다.

단순 함수 타입(□)은 모든 집합 Ba 가 동일한 일반곱으로 볼 수 있다.

[eqn: A-> B=PI_{a in A} B]

따라서 삭제는 응용이다. 의존적 함수 타입(dependent function type)은 완전히 일반적 곱이다.

[eqn: FORALL x^□ CDOT B=PI_{i in □}B(x)]

따라서 삭제는 응용이다. 일차논리에서는 다음의 두 가지를 구분하여 생각한다. 증명들의 타입인 명제(예: A)와 수학적 개인들의 타입인 □ (또는 종류 논리에서 종류). 그러나, 타입 이론에서는 위와 같은 구분을 없앤다. LEGO에서는, A와 B가 명제이거나 개인의 타입일 때, {x:A}B와 같이 표기한다면 이것은 함수 타입이기도 하면서 전칭 정량자(universal quantifier)이기도 하다. 또, B 가 x에 의존하지 않은 특별한 경우 우리는 {x:A}B를 특별히 A->B로 표현하기도 한다.

2.3 합(sums)

B1 과 B2가 집합일 때, 다음과 같이 디스조인트 유니온을 정의할 수 있다.

[eqn: B_1 + B_2 = SUM from { { i}=1} to 2 B_i = "{"(1, b_1 )|b_1 in B_1 "}" cup "{"(2, b_2 )|b_2 in B_2 "}"]

또, Ba를  [eqn: a in A]에 의해 색인된 집합들의 패밀리라면, 다음처럼 색인된 일반 합을 정의할 수 있다.

[eqn: sum from { a in A} B_a = "{"(a, b_a )|a in A, b_a in B_a "}"]

따라서 합은 (투사가 아니고) 케이스 분석에 의해서 삭제될 수 있다.

2.4 합과 타입

이접은 디스조인트 합으로 볼 수 있다.

[eqn: A VEE B = A+B]

존재 정량자는 일반 합으로 볼 수 있다.

[eqn: EXIST x^□ cdot B= sum from {x in □} B(x)]

위에서 이접과 존재 한정사의 삭제가 투사가 아닌 케이스 분석이라는 점에 유의해야 한다. 따라서, [eqn: A vee B] 의 증명 (즉 (inl, a)또는 (inr, b))으로 부터 첫 번째 요소(inl 또는 inr)을 알 수는 있으나, B 또는 A의 증명은 복구할 수는 없다. 또한 [eqn: EXIST x cdot B]의 증명(쌍 (t, a))으로부터 증거 t는 결정할 수는 있으나 B(t')의 증명 a는 구할 수는 없다.

타입이론에서는 좀더 강력한 삭제 규칙을 가지고 있는 합을 정의할 수 있다.

3. 식의 원자적 구성 블락

논리 연산자는 이미 있는 논리식으로 부터 논리식을 구축한다. 커리-하워드 아이소모피즘에 의해 논리 연산자가 이미 존재하는 타입으로부터 새로운 타입을 구축하는 구축자(constructor)로 생각할 수도 있다. 모든 구축자는 어떠한 기초적 케이스가 필요하다. 즉 □원자 식과 원자 타입은 무엇인가?□하는 질문이다. 원자식 은 R 이 n-ary 관계기호이고, [eqn: t_1 ,□, t_n]이 항일 때, [eqn: R(t_1 ,□, t_n )]의 형태를 갖는다. 여기서 n은 0일수도 있다.

또, 한편 논리 연산자를 소개규칙과 삭제규칙에 의해 특징을 설명하였으며, 수축에 의해 inversion 원칙을 표현하였다. 여기서도 원자 식과 타입에 대해서도 위와 같이 할 수 있을까?

예 3.1 □은 원자 식이다. 따라서 □의 소개규칙은 있을 수가 없다. 사실은 이것에 의해 □의 의미가 정해진다. 그렇다면 삭제 규칙은 무엇이 되어야 할까? 여기서는 다음과 같이 기계적으로 만들 수 있다. 주전제(major premise)는 삭제하려고 하는 기호를 포함하는 것이어야 한다. 또 결론은 임의의 식 C 이다.

[eqn: { □ ~~~□} over { C} (□-elim)]

각 소개규칙에 대해서 한 개의 보조 전제를 만들면 되는데, 여기서는 소개 규칙이 하나도 없으므로 다음과 같다.

[eqn: { □ } over { C} (□-elim)]

이렇게 하여 우리가 전에 보였던 □-elim 규칙의 건설적인 의미가 설명된다. 한편 소개규칙이 없다는 것은 수축이 없다는 것을 의미한다.

예 3.2 데이터타입

타입 이론에서 원자적인 것은 데이터타입이다. 즉 귀납적으로 정의된 집합이라고 할 수 있다.

datatype bool = true:bool | false:bool

datatype nat = zero:nat | suc:nat->nat

따라서 데이터타입의 논리적 의미는 구축자들을 다음과 같이 소개규칙을 통해서 보면 알 수 있게된다.

[eqn: {} over { □true:bool } bool-intro-true]	[eqn: {} over { □false:bool } bool-intro-false]

[eqn: { } over {□0:nat } nat-intro-zero]	[eqn: { GAMMA □n:nat} over { GAMMA □suc(n):nat } nat-intro-suc]

4. 원자 타입의 삭제규칙

원자 타입은 소개 규칙에 의해 특징지워진다. 과연 모든 소개규칙들의 모임이 의미가 있거나 일관되다고 말할 수 있을까? 여기서의 목적은 다음과 같은 규칙들을 기계적으로 생성하거나 컴파일 하는 것이다.

소개규칙들의 집합이 있는 경우 삭제규칙을 이들로부터 생성한다. 소개규칙의 결론이 삭제규칙의 주전제일 때, 모든 우회계산을 없앨 수 있는 것이 수축들의 집합이다.

위의 과정이 올바르다는 것의 잣대는 수축들이 표준화한다(normalize)는 것이 된다. 이렇게 된다면 □은 증명될 수 없게 된다. 본 연구에서는 표준화 정리를 증명하는 것이 시간적 공간적 제약이 있기 때문에 증명하지 않겠지만, 소개 규칙들의 집합의 정당성은 다음과 같은 well-foundedness를 보면 명확해 진다. 즉 본 연구에서는 이미 정의된 작은 것에서부터 큰 개념들을 구축한다.

4.1 bool 타입

bool은 원자 타입이다. □은 명제이지만 bool은 아니다. 여기서 부터 일차논리를 벗어나고자 한다. 또 어떠한 타입에 대해서도 정량자(quantifier)를 사용할 수 있다.

4.1.1 소개규칙

[eqn: { } over {□true:bool } (intro-true)]	[eqn: { } over {□false:bool } (intro-false)]

LEGO에서는 다음과 같이 선언한다.

Inductive [bool:Prop]

Constructors [true:bool] [false:bool];

4.1.2 삭제규칙

전제가 없는 소개 규칙이 두 개가 있으므로 앞에서와 같이 하면

[eqn: { GAMMA □b:bool ~~ GAMMA □c1:C ~~ GAMMA □c2:C} over { GAMMA □boolrec(C, c1, c2, b):C} bool-elim]

4.1.3 bool 의 수축

각 bool-intro 규칙에 대해서 한 개의 수축이 있으므로 다음과 같이 하여 두 개의 수축이 있다.

[eqn: { { intro-true} over { GAMMA □true:bool} ~~ { □} atop { GAMMA □c1:C} ~~ { □} atop { GAMMA □c2:C}} over { GAMMA □boolrec(C, c1, c2, b):C} bool-elim ##~~~ RARROW { □} atop { GAMMA □c1:C}]

[eqn: { { intro-false} over { GAMMA □false:bool} ~~ { □} atop { GAMMA □c1:C} ~~ { □} atop { GAMMA □c2:C}} over { GAMMA □boolrec(C, c1, c2, b):C} bool-elim ## RARROW { □} atop { GAMMA □c2:C}]

즉 수축되는 소개규칙과 연관된 보조전제의 유도로 수축된다. 위에서 증명항만의 수축을 표현한다면

boolrec(C, c1, c2, true) □ c1

boolrec(C, c1, c2, false) □ c2

이된다. 즉 boolrec은 bool인 마지막 항에 대해 구조적 순환에 의해 bool을 파괴하고(케이스 분석에 의해서) 새로운 타입 C를 구축한다. boolrec은 명시적인 다형성(polymorphism)을 이용하여 임의의 타입을 갖는 새로운 개체를 구축한다. 따라서 가능한 출력인 c1 또는 c2의 타입 C가 주어져야 한다. 또 boolrec을 이용하여 새로운 객체를 구축할 수 있다.

4.1.4 bool 순환 함수

bool을 돌려주는 함수는 다음과 같이 정의할 수 있다.

not = [b:bool]boolrec(bool, false, true, b)

and = [a,b:bool]boolrec(bool, b, false, a)

만약 nat 타입이 있다면 bool을 nat으로 번역할 수 있다.

bool2nat = [b:bool]boolrec(nat, 1, 0, b).

이와 같은 함수의 타입은 예상과 같이 나온다.

[eqn: □"not"~:bool->bool]

[eqn: □and ~:bool->bool->bool]

[eqn: □bool2nat~:bool->nat]

여기서는 not의 타입만 고려한다면 이것이 bool negation이라는 것을 알 수는 없다.

4.1.5 bool의 의존적 삭제 규칙

앞에서 본 bool-elim 규칙은 만족할 만한 계산력을 제공하고 논리적으로도 정당하다고 할 수는 있으나 여전히 너무 약하다고 할 수 있다. 즉 bool에 관한 명제들은 증명할 수가 없다. 예를 들면,

[eqn: FORALL x^{bool} cdot (x=true VEE x=false)]

에서 bool-elim 규칙의 C는 닫힌 식이므로 구멍이 전혀 없다. 따라서 C를 삭제되는 타입에 의존이 되게 하면 위의 문제를 해결할 수 있다.

[eqn: { GAMMA □b:bool ~~ GAMMA □c1:C(true) ~~ GAMMA □c2:C(false)} over { GAMMA □boolrec(C, c1, c2, b):C(b)} bool-elim]

이렇게 한다면 bool을 위한 통상적인 귀납적 원칙이 된다. 한편 bool의 수축 규칙은 동일하다.

이제는

[eqn: FORALL x^{bool} cdot (x=true VEE x=false)]

을 [eqn: C(x)= (x=true VEE x=false)]로 하므로서 증명할 수 있다. 아직도 등호에 대해서 언급한 적은 없지만 우리가 요구하는 것은 최소한 등호가 reflexive하다는 것뿐이다. [eqn: GAMMA =x:bool] 이라고 하자.

[eqn: { { ass} over { GAMMA □x:bool} ~~ { { =-intro} over { GAMMA □refl(true):true=true} } over {GAMMA □inl(refl(true)):C(true) } ~~ { { =-intro} over { GAMMA □refl(false):false=false} } over {GAMMA □inr(refl(false)):C(false) }} over { { GAMMA □boolrec(C, inl(refl(true)), inr(refl(false)),x):C(x)} over { □[x:bool]boolrec(C, inl(refl(true)), inr(refl(false)),x): FORALL x ^{bool} cdot C(x)} FORALL -intro} bool-elim]

위에서 증명항은 다음과 같다. c 는 redex가 없는 표준

[eqn: c=[x:bool]boolrec(C, inl(refl(true)), inr(refl(false)),x)]

항이다. (c true)는 inl(refl(true)) 즉 C(true)의 증명으로 수축한다. 증명항은 데이터에 응용되면 증명을 계산한다. 본 연구에서는 명제와 타입을 같은 개념으로 고의적으로 혼용하므로 이러한 것들이 데이터를 계산하는 것으로 생각할 수도 있다.

4.2 자연수 nat

소개규칙은 다음과 같이 분명하다.

[eqn: { } over { GAMMA □0:nat} intro-zero]	[eqn: { GAMMA □n:nat} over {GAMMA □suc(n):nat } intro-suc]

LEGO에서는 다음과 같이 선언한다.

Inductive [nat:Prop]

Constructors [zero:nat] [suc:nat->nat];

삭제 규칙은 어떤 것이 되어야 할까? intro-suc 에는 여태까지 보지 않았던 그 무언가가 더 있다. 즉 순환(recursion)이다. 전제의 타입이 결론의 타입과 동일하다는 것이다. □-elim 규칙과 비교해서 생각한다면 비의존적인 elim 규칙은

[eqn: { GAMMA □n:nat ~~GAMMA □a:C ~~GAMMA, x:nat □b:C} over { GAMMA □nat"_"elim(C, a, b, n):C}]

라고 생각할 수도 있겠지만 이것은 물론 잘못된 것이다. 삭제규칙(즉 귀납법)은 모든 nat의 발생을 어떻게 C의 발생으로 치환하는가하는 규칙을 나타내는 것이라고 말할 수 있다. intro-suc의 순환적 전제 때문에 보조전제에 또 다른 가정이 필요하다.

[eqn: { GAMMA □n:nat ~~GAMMA □a:C ~~GAMMA, x:nat, p:C □b:C} over { GAMMA □nat"_"elim(C, a, b, n):C}]

이것을 좀더 쉽게 이해하기 위해서 먼저 가정을 방출시켜서 다음과 같은 의존적 nat-elim규칙으로 바꾸어 보면, 표준적인 귀납 규칙이 된다.

[eqn: { GAMMA □n:nat ~~GAMMA □a:C(0) ~~GAMMA □b: FORALL x^{nat} cdot C(x) ->C(suc (x))} over { GAMMA □nat"_"elim(C, a, b, n):C(n)}]

4.2.1 nat의 수축

H가 식 [eqn: FORALL x^{nat} cdot C(x) ->C(suc (x))]을 나타낸다면 각 nat-intro규칙에 대응하여 두 가지의 수축이 있다. intro-zero를 위한 수축은 쉽다. 다음과 같이 C(0)의 증명이 있다.

[eqn: { { intro-zero} over { GAMMA □0:nat} ~~{□ } atop {GAMMA □a:C(0)} ~~ {□ } atop { GAMMA □b: H} } over { GAMMA □nat"_"elim(C, a, b, 0):C(0)} nat-elim]

[eqn: RARROW ~~~~ { □} atop { GAMMA □a:C(0)}]

intro-suc을 위한 수축을 구하려면 다음과 같은 [eqn: C(suc(n))]의 증명을 보자.

[eqn: { { { □E} atop { GAMMA □n:nat} } over { GAMMA □suc(n):nat}intro-suc ~~{□ F} atop {GAMMA □a:C(0)} ~~ {□D } atop { GAMMA □b: H} } over { GAMMA □nat"_"elim(C, a, b, suc(n)):C(suc(n))} nat-elim]

nat-elim을 E, F 와 D에 응용하면 다음을 유도할 수 있다.

[eqn: GAMMA □nat"_"elim(C, a, b, n):C(n)]

다음으로 n에 [eqn: FORALL x^{nat} cdot C(x) ->C(suc (x))]의 증명 b를 응용하고 또 C(n)의 증명항에 응용하면 다음으로 수축된다는 것을 알 수 있다.

[eqn: { □~~D(n)(nat"_"elim(C, a, b, n))} atop { GAMMA □b(n, nat"_"elim(C, a, b, n)):C(suc(n))}]

수축을 증명항에 대한 연산으로 생각한다면 위의 두 가지 수축을 다음과 같이 정리할 수 있다.

nat_elim(C, a, b, 0) ==> a

nat_elim(C, a, b, suc(n) ) ==> b(n, nat_elim(C, a, b, n))

4.3 원시 순환(Primitive Recursion)과 nat_elim

h 가 수(number)이고 g(x, y)가 수치이론적 함수라면 다음과 같이 정의된 새로운 함수 PR(h, g)가 있다.

PR(h, g)(□, 0)	= h(□)

PR(h, g)(□, suc(n))	= g(□, n, PR(h, g)(□, n))

위의 PR 함수를 다음의 nat_elim과 비교한다면

nat_elim(C)(a, b)(0)   ==> a

nat_elim(C)(a,b)(suc(n))==>b(n, nat_elim(C)(a, b)(n))

nat_elim(C)가 바로 PR 연산자라는 것을 알 수 있다. 즉 a와 b를 받아서 증명에서 증명으로 가는 새로운 함수 nat_elim(C, a, b)를 돌려주는 함수이다. 본 연구에서는 타입과 명제를 고의로 혼용하므로 자연수, 불수 등은 증명과 같은 것이다. 입력되는 함수 a와 b는 실제로는 함수를 받아서 함수를 돌려주는 범함수(functional)일 수도 있다. 본 논문의 후반부에서 nat_elim가 PR보다 훨씬 더 많은 함수를 계산할 수 있다는 것을 보이겠다.

5. 건설적 계산법 CC[2]

CC(Calculus of Constructions)는 의존적 타입이론 시스템으로 대략 고차 논리를 확장한 것이지만 반드시 논리만 있는 것은 아니다. CC는 여러 가지가 있지만 본 논문에서는 순수 CC(LEGO에서는 PCC라 한다.)만 소개한다. PCC를 동일하지만 여러 가지 방향에서 소개할 수도 있겠지만 여기에서는 타입 합성 및 타입검사의 계산가능성을 제외하고 간단히 소개하고자 한다.

5.1 CC: 항의 구조

의존 타입에는 항이 포함되어 있으므로 CC에서 더 이상 항과 타입을 구분하는 것이 무의미하다.

5.1.1 종류(sort)

두 개의 종류가 있다. 종류를 s, t로 표시한다.

s ::= Prop | Type

5.1.2 항(term)

항은 a, b, c, A, B, C, M, N으로 표시한다.

M ::=	v	변수

|   s	종류

|   [x:M]M	람다 항

|   {x:M}M	PI

|   MM	응용

{x:A}B는 [eqn: PI_{x in A} B]의 LEGO의 표현이다. 따라서 다음을 의미한다.

1)[eqn: FORALL x^A cdot B] 이거나,

2) [eqn: A->B] (B가 x에 의존하지 않을 때)이다.

5.2 CC: 문맥(context)의 구조

문맥은  레이블이 붙어 있는 가정의 리스트이다. 문맥은 □로 표시한다.

□ ::= [] | □, x:A

가정의 레이블로 x, y, z를 사용하지만 이런 사항은 별로 중요하지 않다. 문맥

[eqn: GAMMA =x_1 :A_1 , cdots, x_n :A_n]

에서 레이블 [eqn: x_1 , cdots, x_n]들은 모두가 상이해야 한다. 이 전에는  가정 [eqn: A_1 , cdots, A_n]이 명제라고 했지만 이제는 명제라고만 할 수는 없다는 점에 유의해야 한다.

5.3 CC: 판단(judgement)의 구조

판단의 구조는 자연 추론의 그것과 같다.

[eqn: GAMMA □a:A]

여기에서 □는 문맥이고 a, A는 항이다. 이전과 같이 만약 [eqn: GAMMA □a:A]가 유도된다면 □는 유효(valid)하다.

5.4 CC: 유효 문맥의 규칙

[eqn: [] valid]	[eqn: { GAMMA ~valid ~~ GAMMA □A:s} over { GAMMA ,x:A ~valid} (x not in Gamma)]

s는 Prop이나 Type인 종류이다. valid가 □와 서로 순환적으로 정의된 점에 유의하자. 이것은 항과 타입을 합치는 타입의존의 결과이다. □를 유효하게 확장하고자 한다면 우선 A가 명제이거나 타입인 것이 입증되어야 한다. A가 □에서 명제이거나 타입인 것을 입증하려면 타입 판단 [eqn: GAMMA □A:s]가 필요한데 이것은 A가 잘 형성(well-formed)되었음을 의미한다. 이 타입 판단이 □의 유효성 판단에 의존하고 있다.

5.5 CC: 가정의 규칙

유효문맥에 있는 가정을 다음과 같이 접근할 수 있다.

[eqn: ass~~~~ { GAMMA valid} over { GAMMA □x:A} ~~x:A in Gamma]

유효성이 □와 동시에 순환적으로 정의되었으므로 [eqn: Gamma ~valid]가 측면 조건이 아닌 전제에 표시하였다. 이것이외는 ass 규칙은 다른 곳에서와 동일하다.

5.6 CC: [eqn: PI]의 소개 및 삭제 규칙

CC의 기본적 연산은 일반 곱 또는 의존 함수 공간인 □이다.

[eqn: PI-intro ~~~~ { Gamma , x:A□b:B} over { Gamma □ [x:A]b: "{x:A}"B} ~~~B not =Type]

[eqn: PI-elim~~~~ { GAMMA □b:"{x:A}B"~~GAMMA □a:A} over { GAMMA □ba:[a/x]B}]

이것은 □-규칙과 □-규칙을 비교해서 보면 이해가 쉽다. □-규칙과 다른 점은 B가 x에 의존가능성이다. □-intro에서 x가 새로운 변수라는 측면 조건은 [eqn: x not in Gamma]이고 [eqn: x not in FV(A)]이므로 [eqn: PI-intro]의 전제에 의해 보장된다. [eqn: ->-elim]에서 타입 검사를 한 것처럼 [eqn: PI-elim]의 전제 [eqn: Gamma □a:A]에 의해 타입이 검사된다.

5.7 CC: 종류의 규칙

지금까지 5개의 규칙을 제시하였는데 이것만으로는 어떠한 판단도 유도할 수 없다. 유일한 axiom은 [eqn: []valid]뿐이고, 모든 규칙의 전제에는 타입판단 또는 비어 있지 않은 문맥의 유효성이 있어야 하기 때문이다. 따라서 다음과 같이 시작할 수 있는 규칙이 필요하다.

[eqn: "start"~~~~ { GAMMA ~valid} over { GAMMA □Prop:Type}]

start 규칙이 있다면 이제는 유도를 시작할 수 있다.

5.8 CC: □형성 규칙

곱 타입이 잘 형성된 것인지를 판단할 수 있는 규칙을 아직은 제시하지 않았다. 따라서 곱 타입을 문맥에 넣을 수 없다. 이것을 위해 다음과 같은 형성 규칙이 있다.

[eqn: PI-"form" ~~~~ { GAMMA ,x:A□B:s} over { GAMMA □"{x:A}"B:s}]

이 규칙은 매우 강한 규칙이다. 예로 이 규칙을 이용하여 [eqn: bot ::="{A:Prop}"A]로 정의할 수 있다. □이 모든 명제 A의 증명을 돌려주므로 올바른 삭제 규칙이라고 할 수 있다. 그렇지만 모든 명제에 대해서 정량자를 붙인다면 어떠한 타입이 얻어지는 것일까? [eqn: PI-"form"]에 의하면 [eqn: □bot:"Prop"]이다.

[eqn: { { □} atop { "A:Prop□A:Prop"} } over {□"{A:Prop}A:Prop" }]

한편 타입 합성(검사)는 계산 가능하다. 쌍 [eqn: GAMMA , a]가 있다면, 다음과 같이 유도를 하려고 시도한다.

[eqn: { □?} atop { GAMMA □a:?}]

각 단계에서 한 단계 위로 나아가기 위해 적용 가능한 규칙은 한 개뿐이다. 이 규칙은 변수 명을 제외하고는 한 가지 방법만 적용 가능하다. 따라서 타입합성 함수 [eqn: TS( GAMMA )(a)]는 계산가능하고 [eqn: GAMMA , a]는 많아야 한 개의 타입을 갖는다.

5.9 CC: 변환

규칙 7개를 제시하였다. 하지만 여전히 중요한 것이 빠져 있다. 예를 들면 [eqn: x not in B]일 때 [eqn: "{x:A}B"]를 [eqn: A->B]로 해석할 수 있다. 논리 내부에서 다음과 같이 정의해 보자.

[eqn: arrow~::=[X,Y:"Prop"]"{x:X}Y:{X,Y:Prop]Prop"]

이렇게 정의했다면 arrow는 □와 같은 타입을 갖는다. Y는 항 [eqn: [X,Y:"Prop"]"{x:X}Y"]에서 변수이다. 또 x를 포함하지 않으므로 실제 Prop B가 Y대신 대입되더라도 변수명을 바꿈으로 인해서 속박변수 x에 의해 잡히지 않는다. 여기서

[eqn: GAMMA ="A,B:Prop, b:(arrow A B), a:A"]

라면 [eqn: GAMMA □(ba):B]라고 유도할 수 있을까? [eqn: PI-elim]에 의해

[eqn: { GAMMA □b:arrow~A~B ~~~ GAMMA □a:A} over { GAMMA □(ba):B} PI-elim]

일 것 같지만 다음과 같은 이유 때문에 그렇지 못하다.

[eqn: "arrow A B =([X, Y:Prop]{x:X}Y)A B" not = "{x:A}B"]

즉 여기서 필요한 것은 □-변환이다.

5.9.1 □-축소(reduction)

1단계 □-축소는 다음에 의해 정의된다.

[eqn: { } over { ([x:A]b)c ~>~ [c/x]b}]	[eqn: { a ~>~ a'} over { [x:B]a ~>~ [x:B]a'}]	[eqn: { a ~>~ a'} over {ab ~>~ a'b }]	[eqn: { a ~>~ a'} over {ba ~>~ ba' }]

□-축소 [eqn: >^*]는 >의 reflexive하고 전이적 닫힘이다. 변환은 □에 의해 유도된 동치관계이다.

즉 변환(conversion) [eqn: SIMEQ]은 >의 reflexive, 대칭적이고, 전이적 닫힘이다.

[eqn: { a ~>~ b} over { a SIMEQ b}]     [eqn: { } over {a SIMEQ a }]	[eqn: { a SIMEQ b} over { b SIMEQ a}]	[eqn: { a SIMEQ b ~~b SIMEQ c} over { a SIMEQ c}]

이렇게 정의한다면 변환은 다음과 같은 Church-Rosser 성질을 갖는다.

[eqn: a SIMEQ b]라면 [eqn: a SIMEQ c]와 [eqn: b SIMEQ c]를 만족하는 c가 존재한다.

[eqn: "([X, Y:Prop]{x:X}Y)A B" ~SIMEQ~ "{x:A}B"]를 만족시키기 위해 다음과 같은 변환규칙이 필요하다.

[eqn: conv ~~~~ { GAMMA □a:A ~~ GAMMA □B:s} over { GAMMA □a:B} ~~~~~~~A~ SIMEQ ~B]

이 규칙 때문에 논리에서 증명항을 계산하는 것이 중요해진다. 이제는 arrow 예를 유도할 수 있다.

[eqn: { { GAMMA □b:"arrow A B" ~~ GAMMA □"{x:A}B:Prop"} over { GAMMA □b:"{x:A}B"} conv~~~ GAMMA □a:A} over { GAMMA □(ba):B} PI-elim]

이제는 주제에 특정한 구축자가 없기 때문에 다른 7개 규칙처럼 언제 conv규칙을 적용할 수 있는지를 알 수 없다. 따라서 타입 합성이 계산가능한 지도 분명하지 않다.

5.10 CC의 모든 규칙

[eqn: [] valid]	[eqn: { GAMMA ~valid ~~ GAMMA □A:s} over { GAMMA ,x:A ~valid} (x not in Gamma)]

[eqn: ass~~~~ { GAMMA valid} over { GAMMA □x:A} ~~x:A in Gamma]

[eqn: PI-intro ~~~~ { Gamma , x:A□b:B} over { Gamma □ [x:A]b: "{x:A}"B} ~~~B not =Type]

[eqn: PI-elim~~~~ { GAMMA □b:"{x:A}B"~~GAMMA □a:A} over { GAMMA □ba:[a/x]B}]

[eqn: "start"~~~~ { GAMMA ~valid} over { GAMMA □Prop:Type}]

[eqn: PI-"form" ~~~~ { GAMMA ,x:A□B:s} over { GAMMA □"{x:A}"B:s}]

[eqn: conv ~~~~ { GAMMA □a:A ~~ GAMMA □B:s} over { GAMMA □a:B} ~~~~~~~A~ SIMEQ ~B]

CC에서 [eqn: GAMMA □a:A]의 모든 유도는 □ valid의 유도를 포함한다. Thinning, 대입, 주제축소 lemma는 성립한다. 또 일차논리에서는 문맥의 순서는 중요하지 않다. 그러나 CC에서는 [eqn: GAMMA ="A:Prop, x:A"]처럼 문맥 내에서 의존도가 있다. 그렇지만 문맥의 유효성 가정이 나쁜 문맥을 제외시키기 때문에 Thinning lemma는 여전히 성립한다. 또한 다음과 같은 타입의 정당성도 성립한다. 즉 [eqn: GAMMA □a:A]라면 [eqn: A=Type]이거나 [eqn: GAMMA □A:s]이다. CC는 표준화된다. [eqn: GAMMA □a:A]이라면 a, A는 표준화형으로 축소한다. 이것은 결코 단순한 결과가 아니다. 따라서 CC는 일관적이다. 즉 어떠한 a에 대해서도 [eqn: □a:bot]을 유도할 수 없다.

6. 순환함수와 정리증명

수축을 증명항에 대한 연산으로 생각한다면 nat_elim의 두 가지 수축을 다음과 같이 정리할 수 있다.

nat_elim(C, a, b, 0) ==> a

nat_elim(C, a, b, suc(n) ) ==> b(n, nat_elim(C, a, b, n))

plus 연산을 [4]와 같이 첫번째 아규먼트에 대해 순환적으로 정의하면 다음과 같다.

plus zero m=m

plus (suc n)=suc (plus n m)

따라서 nat_elim의 C:nat->Prop은 [_:nat]nat이고, C(n)=nat이 된다. 또 a=m이고, b y x=suc x이므로 b=[_, x:nat]suc x이다. LEGO에서는 다음과 같이 된다.

[plus [n, m:nat] :nat=nat_elim ([_:nat]nat) m

([_, x:nat]suc x) n];

같은 방법으로 times 연산도 첫 번째 아규먼트에 대해 순환적으로 정의하면 다음과 같다.

times zero m=zero

times (suc n) m=plus m (times n m)

그러므로 a=zero이고, b y x=plus m x이므로 LEGO에서는 다음과 같이 한다.

[times [n, m:nat] :nat=nat_elim ([_:nat]nat) zero

([_,x:nat]plus m x) n];

이렇게 plus와 times를 nat_elim을 이용하여 순환적으로 정의하였다면 이런 순환적 함수들이 만족해야 하는 기본적인 성질들이 있을 수 있다. 예를 들면, times가 plus에 대해 분배되는 다음과 같은 분배법칙을 LEGO애서 Goal로 설정하고 증명을 시도할 수 있다.

Goal times_plus_dist_r:

{i, j, k|nat} Eq (times (plus i j) k) (plus (times i k) (times j k))

이 Goal의 증명 세션을 부록에 기록하였다. 이 세션을 읽어 보면 이들 순환 함수들의 nat_elim에 의해 간접적으로 정의된 수축정의가 아주 요긴하게 이용되고 있다는 것을 알 수 있다.  한편 증명이 완료되면 증명항을 저장하여 후에 lemma로 이용하는 것이 가능하다. 본 Goal의 증명항과 그것의 타입은 다음과 같다.

value of times_plus_dist_r =

[i,j,k|nat]

nat_ind ([i'4:nat]{j'5,k'6|nat}

Eq (times (plus i'4 j'5) k'6)

(plus (times i'4 k'6) (times j'5 k'6)))

([j1,k1|nat]Eq_refl (times (plus zero j1) k1))

([n:nat]

[H:{j'5,k'6|nat}

Eq (times (plus n j'5) k'6)

(plus (times n k'6) (times j'5 k'6))]

[j1,k1|nat]

Eq_subst (Eq_sym (plus_assoc k1 (times n k1) (times j1 k1)))

([z:nat]Eq (times (plus (suc n) j1) k1) z)

(Eq_resp (plus k1) (H|j1|k1)))

i

type  of times_plus_dist_r =

{i,j,k|nat}Eq (times (plus i j) k) (plus (times i k) (times j k))

참고문헌

[1]Henk Barendregt. Introduction to Generalized Type Systems. J. Functional Programming, 1(2):125-154, April 1991.

[2]Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, Department of Computer Science, University of Edinburgh, June 1990.

[3]Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, Department of Computer Science, University of Edinburgh, 1994.

[4]Luis E. Sanchis. Recursive Functionals. North-Holland 1992.

부록: times_plus_dist_r 의 LEGO 증명 세션

Lego> Goal times_plus_dist_r

?0 : {i,j,k|nat}Eq (times (plus i j) k) (plus (times i k) (times j k))

Lego> intros (3)

i | nat

j | nat

k | nat

?1 : Eq (times (plus i j) k) (plus (times i k) (times j k))

Lego> Lego> Refine by

nat_ind ([i:nat]{j,k|nat}

Eq (times (plus i j) k) (plus (times i k) (times j k)))

?3 : {j,k|nat}Eq (times (plus zero j) k) (plus (times zero k) (times j k))

?4 : {n:nat}

({j,k|nat}Eq (times (plus n j) k) (plus (times n k) (times j k)))->

{j,k|nat}

Eq (times (plus (suc n) j) k) (plus (times (suc n) k) (times j k))

Lego> intros (2)

j1 | nat

k1 | nat

?8 : Eq (times (plus zero j1) k1) (plus (times zero k1) (times j1 k1))

Refine by  Eq_refl

Discharge..  k1 j1

i | nat

j | nat

k | nat

?4 : {n:nat}

({j,k|nat}Eq (times (plus n j) k) (plus (times n k) (times j k)))->

{j,k|nat}

Eq (times (plus (suc n) j) k) (plus (times (suc n) k) (times j k))

Lego> intros (4)

n : nat

H : {j,k|nat}Eq (times (plus n j) k) (plus (times n k) (times j k))

j1 | nat

k1 | nat

?11 : Eq (times (plus (suc n) j1) k1)

(plus (times (suc n) k1) (times j1 k1))

Lego> Qrepl  plus_assoc k1 (times n k1) (times j1 k1)

plus (plus k1 (times n k1)) (times j1 k1) =>

plus k1 (plus (times n k1) (times j1 k1))

?21 : Eq (times (plus (suc n) j1) k1)

(plus k1 (plus (times n k1) (times j1 k1)))

Lego> Refine by  Eq_resp (plus ?22)

?27 : Eq (nat_elim ([_:nat]nat) zero ([_:nat]plus k1)

(nat_elim ([_:nat]nat) j1 ([_:nat]suc) n))

(plus (times n k1) (times j1 k1))

Lego> Immediate

Discharge..  k1 j1 H n

Discharge..  k j i

*** QED ***   (* time= 0.230000  gc= 0.0  sys= 0.020000 *)

Lego> "times_plus_dist_r"  saved as global, unfrozen

Lego> Lego> times_plus_dist_r;

value of times_plus_dist_r =

[i,j,k|nat]

nat_ind ([i'4:nat]{j'5,k'6|nat}

Eq (times (plus i'4 j'5) k'6)

(plus (times i'4 k'6) (times j'5 k'6)))

([j1,k1|nat]Eq_refl (times (plus zero j1) k1))

([n:nat]

[H:{j'5,k'6|nat}

Eq (times (plus n j'5) k'6) (plus (times n k'6) (times j'5 k'6))]

[j1,k1|nat]

Eq_subst (Eq_sym (plus_assoc k1 (times n k1) (times j1 k1)))

([z:nat]Eq (times (plus (suc n) j1) k1) z) (Eq_resp (plus k1) (H|j1|k1)))

i

type  of times_plus_dist_r =

{i,j,k|nat}Eq (times (plus i j) k) (plus (times i k) (times j k))

Lego>