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는 의 LEGO의 표현이다. 따라서 다음을 의미한다.
1) 이거나,
2) (B가 x에 의존하지 않을 때)이다.
5.2 CC: 문맥(context)의 구조
문맥은 레이블이 붙어 있는 가정의 리스트이다. 문맥은 Γ로 표시한다.
Γ ::= [] | Γ, x:A
가정의 레이블로 x, y, z를 사용하지만 이런 사항은 별로 중요하지 않다. 문맥
에서 레이블 들은 모두가 상이해야 한다. 이 전에는 가정 이 명제라고 했지만 이제는 명제라고만 할 수는 없다는 점에 유의해야 한다.5.3 CC: 판단(judgement)의 구조
판단의 구조는 자연 추론의 그것과 같다.
여기에서 Γ는 문맥이고 a, A…(생략)
|
[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.
|