직관주의 유형 이론(直觀主義 類型 理論, Intuitionistic Type Theory)은 스웨덴의 수학자이자 철학자인 페르 마르틴-뢰프(Per Martin-Löf)가 1970년대에 개발한 논리 체계이자 수학적 기초 이론이다. 이 이론은 수학적 구성주의(constructivism)와 직관주의 직관(intuitionism)의 원리를 형식화하여, 수학적 대상의 존재 증명이 해당 대상의 구체적인 구성(construction)이나 알고리즘을 제공해야 한다는 원칙을 엄격하게 준수한다.
주요 특징
- 커리-하워드 대응(Curry-Howard Correspondence)의 구현: 이 이론은 논리적 명제(proposition)와 자료형(type)을 동일시하며, 명제의 증명(proof)을 해당 자료형의 항(term, element) 또는 프로그램(program)으로 해석한다. 즉, '명제 A의 증명'은 '자료형 A의 원소'와 같다.
- 종속 유형(Dependent Types): 자료형이 값(value)에 의존할 수 있도록 허용한다. 이를 통해 '자연수 n의 길이를 가진 벡터'와 같이 값에 따라 정교하게 제약되는 자료형을 표현할 수 있으며, 정리의 명세(specification)를 자료형 수준에서 매우 정밀하게 기술할 수 있다.
- 직관주의 논리 준수: 배중율(Law of Excluded Middle, $P \lor eg P$)이나 이중 부정 제거(Double Negation Elimination)와 같은 고전 논리의 공리들을 일반적인 증명 규칙으로 채택하지 않는다. 존재 양화자($\exists$)를 증명하려면 구체적인 예시(witness)를 구성해야 한다.
- 귀납적 정의(Inductive Definitions): 자연수, 리스트, 트리 등 수학적 구조를 귀납적으로 정의하고, 이에 대한 귀납법과 재귀 함수를 기본 연산으로 제공한다.
- 우주 계층(Universe Hierarchy): 러셀의 역설(Russell's Paradox) 등 자기 지시적 모순을 피하기 위해, 유형의 유형(Type of Types)을 계층적 우주($U_0, U_1, U_2, \dots$)로 나누어 관리한다.
역사적 배경 및 변형
마르틴-뢰프는 1971년 처음 이 이론을 발표했으며, 이후 모순이 발견되어(예: 기라르의 역설) 수정된 버전들을 발표했다. 주요 변형으로는 예외적 유형 이론(Extensional Type Theory, ETT)과 강화된 유형 이론(Intensional Type Theory, ITT)이 있다. ETT는 정의적 동치(definitional equality)와 명제적 동치(propositional equality)를 동일시하여 증명이 용이하지만 타입 검사가 결정 불가능(undecidable)해진다. ITT는 이 둘을 구분하여 타입 검사의 결정 가능성을 보장하며, 현대의 증명 보조 도구(Coq, Agda, Lean, Idris 등)의 이론적 기반이 되었다. 이후 블라디미르 보예보츠키(Vladimir Voevodsky) 등에 의해 호모토피 유형 이론(Homotopy Type Theory, HoTT)으로 발전하였다.
의의 및 응용
직관주의 유형 이론은 수학의 기초 논리로서 집합론(ZFC)의 대안으로 연구되는 동시에, 컴퓨터 과학 분야에서 증명 보조 도구(Proof Assistants)와 함수형 프로그래밍 언어의 핵심 이론적 토대를 제공한다. 프로그램이 곧 증명이라는 관점 아래, 소프트웨어의 정확성을 수학적으로 검증하는 형식적 검증(Formal Verification) 분야에서 필수적인 도구로 활용되고 있다.
