정의 : 어떠한 항 (Term)에 대해서, 그 항은 타입을 가지고 있고 그 항의 입력과 결과는 그 타입으로 제한된다.
표기 M : A 는, M이 A라는 타입을 가지고 있다는 의미이다.
예를 들어, Integer List라는 타입은 다음과 같이 귀납적으로 정의할 수 있다 : type IntList = Empty | Int ** IntList.
타입 체킹은 크게 두가지 종류로 나눌 수 있다.
- Static Type Checking : 프로그램이 컴파일되는 시점에서 타입을 체킹한다.
- Dynamic Type Checking : 프로그램이 실행되는 시점에서 타입을 체킹한다. 잘 안씀.
타입 체킹을 할 땐, Sound한 타입 체킹을 할지 Dynamic한 타입 체킹을 할 지 결정해야 한다.
이를 위해선, 먼저 다음과 같은 이론전산학적 지식이 필요하다.
Turing Equivalence (튜링 동치)
: 시스템 A가 시스템 B를 시뮬레이션할 수 있고, 시스템 B가 시스템 A를 시뮬레이션할 수 있으면 두 시스템은 튜링 동치라고 부른다.
Universal Turing Machine (UTM, 보편적 튜링 머신)
: 임의의 입력과 출력을 가진 튜링 머신을 시뮬레이팅할 수 있는 튜링 머신을 말한다. 프로그램 저장형 컴퓨터의 기초가 된다.
프로그램 저장형 컴퓨터의 시초라고 불린다.
Turing Completeness
: 어떤 시스템 P가 보편적 튜링 머신과 튜링 동치라면, 그 시스템 P는 튜링 완전하다고 한다.
타입 체킹이 Sound할지, Complete할지 결정하는건 해당 언어의 설계 목적에 따라서 정해야 한다.
- 항상 문제없는 안정성이 필요하면 Sound하게 설계한다던가
- 뭐 에러 한두번쯤 용인할 수 있고 Sound하게 코딩하는게 너무 빡빡하면 Complete하게 설계한다던가
그럼 동시에 Sound하고 Complete한 Type Checker를 만들면 안되나?
A. 안된다.
예시 1) Diophantine Equation (디오판토스 방정식)
- Q. polynomial한 부정방정식의 정수해를 구할 수 있는가?
- A. 프로그램으론 짤 수 없다. 심지언 짤 수 있는지 없는지조차 제대로 모른다.
예시 2) Halting Problem (정지 문제)
- Q. 임의의 프로그램에 대해 이 프로그램이 실행이 끝나는지 끝나지 않는지 판별하는 프로그램이 존재하는가?
- A. 불가능하다.
- H(p,x)라는, p(x)가 끝나는지 안끝나는지 판별하는 함수가 있다고 하자.
- ∀p let H(p,x) = { yes if p(x) terminates, otherwise no }
- Such H is incomputable.
- 증명) let f(x) = if H(f,x) then loop() else 1 라고 하자.
- 해석 : f(x)는, 만약 f(x)가 끝난다면 loop돌리니까 안끝난다. 아니면(안끝나면) 이 프로그램은 끝난다!
- ?? 모순이네?
- H(p,x)라는, p(x)가 끝나는지 안끝나는지 판별하는 함수가 있다고 하자.
- 한편, 만약 Sound & Complete한 TC(Type Checker)가 있다는 건 정지문제도 해결할 수 있다는거 아닌가?
- 근데 위에서 정지문제는 해결할 수 없댔잖아?
- 따라서 그딴 타입체커는 존재하지 않는다.
Type Checking Rule에 대해 들어가기 앞서, Type Checking Rule과 Type Checker를 확실히 구분지을 필요성이 있다. TC Rule은 논리적인 영역에 해당하고, TC (혹은 TC Procedure)는 그것이 실체화된 구현의 영역에 해당한다.
이렇게 Logic과 Computation을 구분하는 데는 이 밖에도 다양한 예시가 존재하는데,
| Logic | Computation |
|---|---|
| Syntax definition | Parser |
| Semantic definition | Interpreter |
| TC rules | TC procedure |
문제에 무작정 접근하지 말고 상위적 레벨인 Logic 단에서 논리 시스템을 만든 후, 어떻게 알고리즘을 만들까 생각해봐야 한다. 실제 문제해결(구현의 세계, Computation)과 논리 (Logic)의 세계를 자유자재로 넘나들 수 있도록 하자.
위 x + 1 = odd? 문제처럼, 어떤 x가 타입이 없으면 (Free Type)
Assumption에 의해서 E의 타입을 결정한다. (Assumption = 추론규칙)
x: odd ⊢ x + 1 : even
x: even ⊢ x + 1 : odd
위와 같은 추론규칙이 있다면,
X: even ∈ Г
–––––––––––––––
Г ⊢ X: even
X: even이란 추론규칙이 Г 집합에 포함될 때,
Г를 전제하면 X: even이다. 이게 뭔 이야기인지 정리해보면,
Г 의 의미는 Assumption의 집합 (추론규칙 집합)이다.
해석: 추론규칙들 Г을 전제로, Expression이 Type이란 것을 증명 가능하다.
