직관주의 유형 이론

직관주의 유형 이론(Intuitionistic type theory, 直觀主義類型理論), 직관주의 유형론, 구성주의 유형 이론 또는 마르틴뢰프 유형 이론(Martin-Löf type theory, MLTT)은 유형 이론이자 수학의 기초에 대한 대안이다. 직관주의 유형 이론은 스웨덴의 수학자이자 철학자인 페르 마르틴뢰프가 만들었으며, 1972년에 처음 발표했다. 이 유형 이론에는 여러 버전이 있는데, 마르틴뢰프는 이론의 내포적 및 외연적 변형과 초기의 비예측적 버전을 모두 제안했지만, 지라르의 역설로 인해 모순이 있는 것으로 나타나 예측적 버전으로 대체되었다. 그러나 모든 버전은 의존형을 사용하는 구성주의 논리의 핵심 설계를 유지한다.

설계

마르틴뢰프는 수학적 구성주의의 원리에 따라 유형 이론을 설계했다. 구성주의는 모든 존재 증명이 "증거"를 포함해야 한다고 요구한다. 따라서 "1000보다 큰 소수가 존재한다"는 증명은 소수이면서 1000보다 큰 특정 숫자를 식별해야 한다. 직관주의 유형 이론은 BHK 해석을 내면화함으로써 이러한 설계 목표를 달성했다. 유용한 결과는 증명이 검사, 비교 및 조작될 수 있는 수학적 객체가 된다는 것이다.

직관주의 유형 이론의 유형 생성자는 논리적 연결사와 일대일 대응을 따르도록 구축되었다. 예를 들어, 함의( $A\implies B$ )라는 논리적 연결사는 함수의 유형( $A\to B$ )에 해당한다. 이 대응을 커리-하워드 동형이라고 한다. 이전 유형 이론도 이 동형을 따랐지만, 마르틴뢰프의 이론은 의존형을 도입하여 술어 논리로 확장한 최초의 이론이었다.

유형 이론

유형 이론은 존재하는 근본적인 객체를 설명하는 일종의 수학적 존재론 또는 기초론이다. 표준 기초인 집합론과 수리 논리학이 결합된 경우, 근본적인 객체는 요소를 포함하는 컨테이너인 집합이다. 유형 이론에서 근본적인 객체는 용어이며, 각 용어는 오직 하나의 유형에 속한다.

직관주의 유형 이론은 세 가지 유한 유형을 가지며, 이들은 다섯 가지 다른 유형 생성자를 사용하여 구성된다. 집합론과는 달리, 유형 이론은 프레게의 논리처럼 논리 위에 구축되지 않는다. 따라서 유형 이론의 각 기능은 수학과 논리 모두의 기능으로 두 가지 역할을 한다.

0 유형, 1 유형 및 2 유형

세 가지 유한 유형이 있다. 0 유형은 용어를 포함하지 않는다. 1 유형은 하나의 표준 용어를 포함한다. 2 유형은 두 개의 표준 용어를 포함한다.

0 유형은 용어를 포함하지 않으므로 공 유형이라고도 불린다. 존재할 수 없는 모든 것을 나타내는 데 사용된다. 또한 $\bot$ 으로도 쓰이며 증명 불가능한 모든 것(즉, 그것의 증명이 존재할 수 없음)을 나타낸다. 결과적으로 부정은 그것에 대한 함수로 정의된다. $\neg A:=A\to \bot$ .

마찬가지로, 1 유형은 하나의 표준 용어를 포함하며 존재를 나타낸다. 또한 단위 유형이라고도 불린다.

마지막으로, 2 유형은 두 개의 표준 용어를 포함한다. 이것은 두 값 사이의 명확한 선택을 나타낸다. 불 값에 사용되지만 명제에는 사용되지 않는다.

명제는 대신 특정 유형으로 표현된다. 예를 들어, 참 명제는 1 유형으로 표현될 수 있고, 거짓 명제는 0 유형으로 표현될 수 있다. 그러나 이것들이 유일한 명제라고 단언할 수는 없으며, 즉 직관주의 유형 이론에서 명제에 대해 배중률은 성립하지 않는다.

Σ 유형 생성자

Σ-유형은 순서쌍을 포함한다. 일반적인 순서쌍(또는 2-튜플) 유형과 마찬가지로, Σ-유형은 두 다른 유형 $A$ 와 $B$ 의 카르테시안 곱, $A\times B$ 를 설명할 수 있다. 논리적으로, 그러한 순서쌍은 $A$ 의 증명과 $B$ 의 증명을 포함하므로, 그러한 유형은 $A\wedge B$ 로 쓰이는 것을 볼 수 있다.

Σ-유형은 의존적 유형화 때문에 일반적인 순서쌍 유형보다 더 강력하다. 순서쌍에서 두 번째 용어의 유형은 첫 번째 용어의 값에 따라 달라질 수 있다. 예를 들어, 쌍의 첫 번째 용어가 자연수이고 두 번째 용어의 유형이 첫 번째 용어의 길이와 같은 실수의 수열일 수 있다. 그러한 유형은 다음과 같이 쓰일 것이다.

$\sum _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)$

집합론 용어를 사용하면, 이것은 집합의 인덱스화된 분리합집합과 유사하다. 일반적인 카르테시안 곱의 경우, 두 번째 용어의 유형은 첫 번째 용어의 값에 따라 달라지지 않는다. 따라서 카르테시안 곱 ${\mathbb {N} }\times {\mathbb {R} }$ 을 설명하는 유형은 다음과 같이 쓰인다.

$\sum _{n{\mathbin {:}}{\mathbb {N} }}{\mathbb {R} }$

여기서 첫 번째 용어의 값인 $n$ 은 두 번째 용어의 유형인 ${\mathbb {R} }$ 에 의존하지 않는다는 점에 유의해야 한다.

Σ-유형은 수학에서 사용되는 더 긴 의존적 튜플과 대부분의 프로그래밍 언어에서 사용되는 레코드 또는 구조체를 구성하는 데 사용될 수 있다. 의존적 3-튜플의 예로는 두 정수와 첫 번째 정수가 두 번째 정수보다 작다는 증명이 있으며, 이는 다음 유형으로 설명된다.

$\sum _{m{\mathbin {:}}{\mathbb {Z} }}{\sum _{n{\mathbin {:}}{\mathbb {Z} }}((m<n)={\text{True}})}$

의존적 유형화는 Σ-유형이 존재 양화사의 역할을 수행하도록 허용한다. "유형 ${\mathbb {N} }$ 의 $n$ 이 존재하고, $P(n)$ 이 증명된다"는 문장은 첫 번째 항목이 유형 ${\mathbb {N} }$ 의 값 $n$ 이고 두 번째 항목이 $P(n)$ 의 증명인 순서쌍의 유형이 된다. 두 번째 항목( $P(n)$ 의 증명)의 유형이 순서쌍의 첫 번째 부분( $n$ )의 값에 의존한다는 점에 주목하라. 그 유형은 다음과 같을 것이다.

$\sum _{n{\mathbin {:}}{\mathbb {N} }}P(n)$

Π 유형 생성자

Π-유형은 함수를 포함한다. 일반적인 함수 유형과 마찬가지로, 입력 유형과 출력 유형으로 구성된다. 그러나 반환 유형이 입력 값에 따라 달라질 수 있다는 점에서 일반적인 함수 유형보다 더 강력하다. 유형 이론의 함수는 집합론과 다르다. 집합론에서는 순서쌍 집합에서 인수의 값을 찾는다. 유형 이론에서는 인수가 용어에 대입된 다음, 용어에 대한 계산("환원")이 적용된다.

예를 들어, 자연수 $n$ 이 주어지면 $n$ 개의 실수를 포함하는 벡터를 반환하는 함수의 유형은 다음과 같이 쓰인다.

$\prod _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)$

출력 유형이 입력 값에 의존하지 않을 때, 함수 유형은 종종 단순히 $\to$ 로 쓰인다. 따라서 ${\mathbb {N} }\to {\mathbb {R} }$ 은 자연수에서 실수로 가는 함수의 유형이다. 이러한 Π-유형은 논리적 함의에 해당한다. 논리적 명제 $A\implies B$ 는 $A$ 의 증명을 받아 $B$ 의 증명을 반환하는 함수를 포함하는 유형 $A\to B$ 에 해당한다. 이 유형은 다음과 같이 더 일관성 있게 쓸 수 있다.

$\prod _{a{\mathbin {:}}A}B$

Π-유형은 또한 보편 양화를 위한 논리에도 사용된다. "모든 유형 ${\mathbb {N} }$ 의 $n$ 에 대해 $P(n)$ 이 증명된다"는 문장은 유형 ${\mathbb {N} }$ 의 $n$ 에서 $P(n)$ 의 증명으로 가는 함수가 된다. 따라서 $n$ 에 대한 값이 주어지면 함수는 해당 값에 대해 $P(\,\cdot \,)$ 가 성립한다는 증명을 생성한다. 이 유형은 다음과 같을 것이다.

$\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)$

= 유형 생성자

=-유형은 두 개의 용어로부터 생성된다. $2+2$ 와 $2\cdot 2$ 와 같은 두 용어가 주어지면, 새로운 유형 $2+2=2\cdot 2$ 를 생성할 수 있다. 그 새로운 유형의 용어들은 그 쌍이 동일한 표준 용어로 축소된다는 증명을 나타낸다. 따라서 $2+2$ 와 $2\cdot 2$ 모두 표준 용어 $4$ 로 계산되므로, 유형 $2+2=2\cdot 2$ 의 용어가 존재할 것이다. 직관주의 유형 이론에서는 =-유형을 도입하는 단일한 방법이 있으며, 그것은 반사성에 의한 것이다.

$\operatorname {refl} {\mathbin {:}}\prod _{a{\mathbin {:}}A}(a=a).$

용어가 동일한 표준 용어로 축소되지 않는 $1=2$ 와 같은 =-유형을 생성하는 것이 가능하지만, 그 새로운 유형의 용어를 생성할 수는 없다. 사실, 만약 $1=2$ 의 용어를 생성할 수 있었다면, $\bot$ 의 용어를 생성할 수 있었을 것이다. 그것을 함수에 넣으면 $1=2\to \bot$ 유형의 함수가 생성될 것이다. $\ldots \to \bot$ 는 직관주의 유형 이론이 부정을 정의하는 방식이므로, $\neg (1=2)$ 또는 최종적으로 $1\neq 2$ 를 가질 것이다.

증명의 등식은 증명 이론에서 활발히 연구되는 분야이며 호모토피 유형 이론 및 다른 유형 이론의 발전을 이끌었다.

귀납 유형

귀납 유형은 복잡한 자기 참조 유형을 생성할 수 있도록 한다. 예를 들어, 자연수의 연결 리스트는 빈 리스트이거나 자연수와 또 다른 연결 리스트의 쌍이다. 귀납 유형은 나무, 그래프 등과 같은 무한 수학적 구조를 정의하는 데 사용될 수 있다. 사실, 자연수 유형은 귀납 유형으로 정의될 수 있는데, 이는 $0$ 이거나 다른 자연수의 다음수이다.

귀납 유형은 $0{\mathbin {:}}{\mathbb {N} }$ 와 같은 새로운 상수와 다음수 함수 $S{\mathbin {:}}{\mathbb {N} }\to {\mathbb {N} }$ 를 정의한다. $S$ 는 정의를 가지고 있지 않고 대체(substitution)를 사용하여 평가될 수 없으므로, $S0$ 와 $SSS0$ 와 같은 용어는 자연수의 표준 용어가 된다.

귀납 유형에 대한 증명은 귀납법을 통해 가능하다. 각 새로운 귀납 유형은 고유한 귀납 규칙과 함께 제공된다. 모든 자연수에 대해 술어 $P(\,\cdot \,)$ 를 증명하려면 다음 규칙을 사용한다.

${\operatorname {{\mathbb {N} }-elim} }\,{\mathbin {:}}P(0)\,\to \left(\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)\to P(S(n))\right)\to \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)$

직관주의 유형 이론의 귀납 유형은 잘 정돈된 트리의 유형인 W-유형으로 정의된다. 유형 이론의 후속 연구는 보다 모호한 종류의 자기 참조성을 가진 유형에 대한 코귀납 유형, 귀납-재귀 및 귀납-귀납을 생성했다. 고차 귀납 유형은 용어 간의 등식을 정의할 수 있도록 한다.

전체 유형

전체 유형은 다른 유형 생성자로 생성된 모든 유형에 대한 증명을 작성할 수 있도록 한다. 전체 유형 ${\mathcal {U}}_{0}$ 의 모든 용어는 $0,1,2,\Sigma ,\Pi ,=,$ 및 귀납 유형 생성자의 모든 조합으로 생성된 유형에 매핑될 수 있다. 그러나 역설을 피하기 위해, 어떤 ${\mathcal {n}}\in \mathbb {N}$ 에 대해서도 ${\mathcal {U}}_{n}$ 에 ${\mathcal {U}}_{n}$ 으로 매핑되는 용어는 없다.^[1]

모든 "작은 유형"과 ${\mathcal {U}}_{0}$ 에 대한 증명을 작성하려면 ${\mathcal {U}}_{1}$ 을 사용해야 한다. 이 유형은 ${\mathcal {U}}_{0}$ 에 대한 용어를 포함하지만, 자체 ${\mathcal {U}}_{1}$ 에 대한 용어는 포함하지 않는다. 마찬가지로, ${\mathcal {U}}_{2}$ 도 그렇다. 예측적 계층의 전체가 존재하므로, 고정된 상수 $k$ 전체에 대한 증명을 정량화하려면 ${\mathcal {U}}_{k+1}$ 을 사용할 수 있다.

전체 유형은 유형 이론의 까다로운 기능이다. 마르틴뢰프의 원래 유형 이론은 지라르의 역설을 설명하기 위해 변경되어야 했다. 후속 연구는 "초 전체", "말로 전체" 및 비예측적 전체와 같은 주제를 다루었다.

판단

직관주의 유형 이론의 형식적 정의는 판단을 사용하여 작성된다. 예를 들어, "만약 $A$ 가 유형이고 $B$ 가 유형이면 $\textstyle \sum _{a:A}B$ 는 유형이다"라는 문장에는 "는 유형이다", "그리고", "만약...이면..."이라는 판단이 있다. 표현 $\textstyle \sum _{a:A}B$ 는 판단이 아니다; 그것은 정의되는 유형이다.

유형 이론의 이 두 번째 수준은 특히 등식과 관련하여 혼란스러울 수 있다. 용어 등식에 대한 판단이 있으며, 예를 들어 $4=2+2$ 라고 말할 수 있다. 이것은 두 용어가 동일한 표준 용어로 축소된다는 진술이다. 유형 등식에 대한 판단도 있으며, 예를 들어 $A=B$ 라고 말하면, $A$ 의 모든 요소가 유형 $B$ 의 요소이며 그 반대도 마찬가지라는 의미이다. 유형 수준에서는 유형 $4=2+2$ 가 있으며, $4$ 와 $2+2$ 가 동일한 값으로 축소된다는 증명이 있다면 이 유형에는 용어가 포함된다. (이 유형의 용어는 용어 등식 판단을 사용하여 생성된다.) 마지막으로, 영어 수준의 등식이 있는데, 이는 우리가 "four"라는 단어와 " $4$ "라는 기호를 사용하여 표준 용어 $SSSS0$ 를 참조하기 때문이다. 이러한 동의어는 마르틴뢰프에 의해 "정의적으로 동일하다"고 불린다.

아래 판단에 대한 설명은 노르드스트롬, 페테르손, 스미스의 논의를 기반으로 한다.

형식 이론은 유형과 객체를 다룬다.

유형은 다음과 같이 선언된다.

$A\ {\mathsf {Type}}$

객체가 존재하며 유형에 속하는 경우는 다음과 같다.

$a{\mathbin {:}}A$

객체는 같을 수 있다.

$a=b$

그리고 유형은 같을 수 있다.

$A=B$

다른 유형의 객체에 의존하는 유형은 다음과 같이 선언된다.

$(x{\mathbin {:}}A)B$

그리고 대입으로 제거된다.

$B[x/a]$ , $B$ 에서 변수 $x$ 를 객체 $a$ 로 대체한다.

다른 유형의 객체에 의존하는 객체는 두 가지 방법으로 수행될 수 있다. 객체가 "추상화"된 경우, 다음과 같이 쓰인다.

$[x]b$

그리고 대입으로 제거된다.

$b[x/a]$ , $b$ 에서 변수 $x$ 를 객체 $a$ 로 대체한다.

객체에 의존하는 객체는 재귀 유형의 일부로 상수로 선언될 수도 있다. 재귀 유형의 예는 다음과 같다.

$0{\mathbin {:}}\mathbb {N}$
$S{\mathbin {:}}\mathbb {N} \to \mathbb {N}$

여기서 $S$ 는 상수 객체 의존 객체이다. 추상화와 관련이 없다. $S$ 와 같은 상수는 등식을 정의하여 제거할 수 있다. 여기서 덧셈과의 관계는 등식과 $S$ 의 재귀적 측면을 처리하기 위한 패턴 매칭을 사용하여 정의된다.

{\begin{aligned}\operatorname {add} &{\mathbin {:}}\ (\mathbb {N} \times \mathbb {N} )\to \mathbb {N} \\\operatorname {add} (0,b)&=b\\\operatorname {add} (S(a),b)&=S(\operatorname {add} (a,b)))\end{aligned}}

$S$ 는 불투명한 상수로 조작된다. 즉, 대체할 내부 구조가 없다.

따라서 객체와 유형, 그리고 이러한 관계는 이론에서 공식을 표현하는 데 사용된다. 다음 스타일의 판단은 기존 객체, 유형 및 관계에서 새로운 객체, 유형 및 관계를 생성하는 데 사용된다.

$\Gamma \vdash \sigma \ {\mathsf {Type}}$	σ는 컨텍스트 Γ에서 잘 형성된 유형이다.
$\Gamma \vdash t{\mathbin {:}}\sigma$	t는 컨텍스트 Γ에서 유형 σ의 잘 형성된 용어이다.
$\Gamma \vdash \sigma \equiv \tau$	σ와 τ는 컨텍스트 Γ에서 동일한 유형이다.
$\Gamma \vdash t\equiv u{\mathbin {:}}\sigma$	t와 u는 컨텍스트 Γ에서 유형 σ의 판단적으로 동일한 용어이다.
$\vdash \Gamma \ {\mathsf {Context}}$	Γ는 유형화 가정을 잘 형성한 컨텍스트이다.

관례상, 다른 모든 유형을 나타내는 유형이 있다. 이를 ${\mathcal {U}}$ (또는 $\operatorname {Set}$ )라고 한다. ${\mathcal {U}}$ 는 유형이므로, 그 구성원들은 객체이다. 각 객체를 해당 유형에 매핑하는 의존 유형 $\operatorname {El}$ 이 있다. 대부분의 텍스트에서는 $\operatorname {El}$ 이 작성되지 않는다. 진술의 문맥상 독자는 $A$ 가 유형을 나타내는지, 아니면 유형에 해당하는 ${\mathcal {U}}$ 의 객체를 나타내는지를 거의 항상 알 수 있다.

이것이 이론의 완전한 기초이다. 다른 모든 것은 파생된다.

논리를 구현하기 위해 각 명제는 고유한 유형을 갖는다. 해당 유형의 객체는 명제를 증명하는 다양한 가능한 방법을 나타낸다. 명제에 대한 증명이 없으면 해당 유형에는 객체가 없다. 명제에 작용하는 "그리고" 및 "또는"과 같은 연산자는 새로운 유형과 새로운 객체를 도입한다. 따라서 $A\times B$ 는 유형 $A$ 와 유형 $B$ 에 의존하는 유형이다. 해당 의존 유형의 객체는 $A$ 와 $B$ 의 모든 객체 쌍에 대해 존재하도록 정의된다. $A$ 또는 $B$ 중 하나가 증명이 없고 빈 유형이면 $A\times B$ 를 나타내는 새 유형도 비어 있다.

이것은 다른 유형(부울, 자연수 등) 및 해당 연산자에 대해서도 수행될 수 있다.

유형 이론의 범주적 모형

범주론의 언어를 사용하여 R. A. G. 실리는 유형 이론의 기본 모형으로 국소 카르테시안 닫힌 범주 (LCCC)의 개념을 도입했다. 이것은 호프만과 딥비르에 의해 카트멜의 이전 작업을 기반으로 패밀리가 있는 범주 또는 속성이 있는 범주로 정교화되었다.^[2]

패밀리가 있는 범주는 문맥의 범주 C(여기서 객체는 문맥이고, 문맥 사상은 대입이다)와, 반변함자 T : C^op → Fam(Set)으로 구성된다.

Fam(Set)은 집합의 패밀리 범주이며, 객체는 "인덱스 집합" A와 함수 B: X → A의 쌍 $(A,B)$ 이고, 사상은 함수 f : A → A' 와 g : X → X' 의 쌍으로, B' _° g = f _° B를 만족한다. 즉, f는 B_a를 B_g(a)로 매핑한다.

함자 T는 문맥 G에 대해 유형 집합 $Ty(G)$ 를 할당하고, 각 $A:Ty(G)$ 에 대해 용어 집합 $Tm(G,A)$ 를 할당한다. 함자에 대한 공리는 이들이 대입과 조화롭게 작동하도록 요구한다. 대입은 일반적으로 Af 또는 af 형태로 쓰며, 여기서 A는 $Ty(G)$ 의 유형이고 a는 $Tm(G,A)$ 의 용어이며, f는 D에서 G로의 대입이다. 여기서 $Af:Ty(D)$ 이고 $af:Tm(D,Af)$ 이다.

범주 C는 종단 객체(빈 문맥)와, 오른쪽에 있는 원소가 왼쪽 원소의 문맥에 있는 유형인 포괄(comprehension) 또는 문맥 확장이라는 형태의 곱에 대한 최종 객체를 포함해야 한다. G가 문맥이고 $A:Ty(G)$ 이면, 매핑 p : D → G, q : Tm(D,Ap)를 갖는 문맥 D 중에서 최종적인 객체 $(G,A)$ 가 있어야 한다.

마르틴뢰프의 것과 같은 논리적 프레임워크는 문맥 의존적인 유형 및 용어 집합에 대한 닫힘 조건의 형태를 취한다. 즉, Set이라는 유형이 있어야 하고, 각 Set에 대해 유형이 있어야 하며, 유형은 의존 합 및 곱의 형태와 다양한 형태의 귀납적 정의에 대해 닫혀 있어야 한다.

예측적 집합론과 같은 이론은 집합의 유형과 그 원소에 대한 닫힘 조건을 표현한다. 즉, 의존 합 및 곱을 반영하는 연산과 다양한 형태의 귀납적 정의에 대해 닫혀 있어야 한다.

외연적 대 내포적

근본적인 구분은 외연적 유형 이론 대 내포적 유형 이론이다. 외연적 유형 이론에서는 정의적(즉, 계산적) 동등성과 증명을 필요로 하는 명제적 동등성이 구별되지 않는다. 결과적으로 유형 이론 내의 프로그램이 종료되지 않을 수 있으므로 외연적 유형 이론에서는 유형 검사가 결정 불가능해진다. 예를 들어, 이러한 이론은 Y 콤비네이터에 유형을 부여하는 것을 허용한다. 이에 대한 자세한 예시는 Nordstöm과 Petersson의 "Programming in Martin-Löf's Type Theory"에서 찾을 수 있다.^[3] 그러나 이것이 외연적 유형 이론이 실용적인 도구의 기반이 되는 것을 막지는 못한다. 예를 들어, 누프르 시스템은 계산 유형 이론에 기반을 두고 있다.^[4] 그리고 Coq는 귀납적 구성의 계산에 기반을 두고 있다.

반면, 내포적 유형 이론에서는 유형 검사가 결정 가능하지만, 표준 수학적 개념의 표현은 다소 번거롭다. 내포적 추론은 집합동치 또는 유사한 구성을 사용해야 하기 때문이다. 정수, 유리수, 실수와 같이 이 없이는 다루기 어렵거나 표현할 수 없는 공통 수학적 객체가 많이 있다. 정수와 유리수는 집합동치 없이도 표현할 수 있지만, 이러한 표현은 다루기 어렵다. 코시 실수는 이 없이는 표현할 수 없다.^[5]

호모토피 유형 이론은 이 문제를 해결하기 위해 노력한다. 이는 고차 귀납 유형을 정의할 수 있게 하는데, 이는 1차 생성자(값 또는 점)뿐만 아니라 고차 생성자, 즉 요소 간의 등식(경로), 등식 간의 등식(호모토피), 그리고 무한히 계속되는 등식을 정의한다.

유형 이론의 구현

다양한 형태의 유형 이론이 여러 증명 보조기의 기반이 되는 형식 시스템으로 구현되었다. 많은 시스템이 페르 마르틴뢰프의 아이디어를 기반으로 하지만, 많은 시스템은 추가 기능, 더 많은 공리 또는 다른 철학적 배경을 가지고 있다. 예를 들어, 누프르 시스템은 계산 유형 이론에 기반을 두고 있으며^[6] Coq는 (공)귀납적 구성의 계산에 기반을 두고 있다. 의존형은 또한 ATS, 카옌, 에피그램, 아그다,^[7] 및 아이드리스와 같은 프로그래밍 언어의 설계에도 특징적으로 나타난다.^[8]

마르틴뢰프 유형 이론

페르 마르틴뢰프는 여러 유형 이론을 구축하여 다양한 시기에 발표했는데, 일부는 그의 설명이 담긴 사전 인쇄물이 전문가들(특히 장 이브 지라르와 조반니 삼빈)에게 공개된 시점보다 훨씬 늦게 발표되었다. 아래 목록은 인쇄된 형태로 설명된 모든 이론을 나열하고 서로를 구별하는 주요 특징을 간략하게 설명하려고 한다. 이 모든 이론은 종속 곱, 종속 합, 분리 합집합, 유한 유형 및 자연수를 가지고 있었다. 모든 이론은 종속 곱 또는 종속 합에 대한 η-환원을 포함하지 않는 동일한 환원 규칙을 가졌으며, 종속 곱에 대한 η-환원이 추가된 MLTT79는 예외였다.

MLTT71은 페르 마르틴뢰프가 만든 최초의 유형 이론이다. 1971년 사전 인쇄물로 등장했다. 하나의 전체를 가지고 있었지만, 이 전체는 그 자체로 이름을 가지고 있었다. 즉, 오늘날 "유형 안의 유형(Type in Type)"이라고 불리는 유형 이론이었다. 장 이브 지라르는 이 시스템이 불일치함을 보여주었고, 사전 인쇄물은 출판되지 않았다.

MLTT72는 1972년 현재 출판된 사전 인쇄물에서 발표되었다.^[9] 이 이론은 하나의 전체 V를 가지고 있었고 동일성 유형 (=-유형)은 없었다. 이 전체는 예측적이었는데, 이는 V에 있지 않은 객체(예를 들어 V 자체)에 대한 V의 객체들의 패밀리의 종속 곱이 V에 있다고 가정되지 않았다는 의미이다. 이 전체는 버트런드 러셀의 수학 원리와 유사했는데, 즉 "T∈V"와 "t∈T" (마르틴뢰프는 현대의 ":" 대신 "∈" 기호를 사용했다)를 추가적인 생성자 "El" 없이 직접 작성했을 것이다.

MLTT73은 페르 마르틴뢰프가 처음으로 출판한 유형 이론의 정의였다(1973년 논리 콜로퀴엄에서 발표되었고 1975년에 출판되었다^[10]). 그는 "명제"라고 설명하는 동일성 유형이 있지만, 명제와 다른 유형 간의 실제 구별이 도입되지 않았기 때문에 그 의미는 불분명하다. 나중에 J-소거자라는 이름을 얻게 되는 것이 있지만 아직 이름이 없다(pp. 94–95 참조). 이 이론에는 V₀, ..., V_n, ...와 같은 무한한 전체 시퀀스가 있다. 이 전체는 예측적이고, 러셀 스타일이며, 누적되지 않는다. 사실, p. 115의 따름정리 3.10은 A∈V_m이고 B∈V_n이 A와 B가 변환 가능하면 m=n이라고 말한다.

MLTT79는 1979년에 발표되었고 1982년에 출판되었다.^[11] 이 논문에서 마르틴뢰프는 종속 유형 이론의 네 가지 기본 판단 유형을 도입했는데, 이는 그 이후 이러한 시스템의 메타 이론 연구에서 기본이 되었다. 그는 또한 컨텍스트를 별도의 개념으로 도입했다(p. 161 참조). J-소거자(MLTT73에도 나타났지만 그때는 이 이름이 없었다)를 가진 동일성 유형이 있었지만, 이론을 "외연적"으로 만드는 규칙도 있었다(p. 169). W-유형도 있었다. 누적되는 예측적 전체의 무한 시퀀스가 있었다.

비블리오폴리스(Bibliopolis): 1984년 비블리오폴리스 책에는^[12] 유형 이론에 대한 논의가 있지만, 다소 개방적이며 특정 선택 집합을 나타내는 것 같지 않으므로 그와 관련된 특정 유형 이론은 없다.

같이 보기

내용주

↑ Bertot, Yves; Castéran, Pierre (2004). 《Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions》. Texts in theoretical computer science. Berlin Heidelberg: Springer. ISBN 978-3-540-20854-9.
↑ Clairambault, Pierre; Dybjer, Peter (2014). 《The biequivalence of locally cartesian closed categories and Martin-Löf type theories》. 《Mathematical Structures in Computer Science》 (영어) 24. arXiv:1112.3456. doi:10.1017/S0960129513000881. ISSN 0960-1295. S2CID 416274.
↑ Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in Martin-Löf's Type Theory. Oxford University Press, p. 90.
↑ Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; L.; E. (2006). 《Innovations in computational type theory using Nuprl》. 《Journal of Applied Logic》 4. 428–469쪽. doi:10.1016/j.jal.2005.10.005.
↑ Altenkirch, Thorsten; Anberrée, Thomas; Li, Nuo. Definable Quotients in Type Theory (PDF) (보고서). 2024년 4월 19일에 원본 문서 (PDF)에서 보존된 문서.
↑ Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; L.; E. (2006). 《Innovations in computational type theory using Nuprl》. 《Journal of Applied Logic》 4. 428–469쪽. doi:10.1016/j.jal.2005.10.005.
↑ Norell, Ulf (2009). 〈Dependently typed programming in Agda〉. 《Proceedings of the 4th international workshop on Types in language design and implementation》. TLDI '09. New York, NY, USA: ACM. 1–2쪽. CiteSeerX 10.1.1.163.7149. doi:10.1145/1481861.1481862. ISBN 9781605584201. S2CID 1777213.
↑ Brady, Edwin (2013). 《Idris, a general-purpose dependently typed programming language: Design and implementation》. 《Journal of Functional Programming》 23. 552–593쪽. doi:10.1017/S095679681300018X. ISSN 0956-7968. S2CID 19895964.
↑ Martin-Löf, Per (1998). 《An intuitionistic theory of types, Twenty-five years of constructive type theory (Venice,1995)》. Oxford Logic Guides 36. New York: Oxford University Press. 127–172쪽.
↑ Martin-Löf, Per (1975). 〈An intuitionistic theory of types: predicative part〉. 《Studies in Logic and the Foundations of Mathematics》. Logic Colloquium '73 (Bristol, 1973). Amsterdam: North-Holland. 73–118쪽.
↑ Martin-Löf, Per (1982). 〈Constructive mathematics and computer programming〉. 《Studies in Logic and the Foundations of Mathematics》. Logic, methodology and philosophy of science, VI (Hannover, 1979). Amsterdam: North-Holland. 153–175쪽.
↑ Martin-Löf, Per (1984). 《Intuitionistic type theory, Studies in Proof Theory (lecture notes by Giovanni Sambin)》 1. Bibliopolis. iv, 91쪽.

각주

Martin-Löf, Per; Sambin, Giovanni (1984). 《Intuitionistic type theory》 (PDF). Napoli: Bibliopolis. ISBN 978-8870881059. OCLC 12731401.

추가 읽을거리

페르 마르틴뢰프의 노트, 조반니 삼빈 기록 (1980)
Nordström, Bengt; Petersson, Kent; Smith, Jan M. (1990). 《Programming in Martin-Löf's Type Theory》. Oxford University Press. ISBN 9780198538141.
Thompson, Simon (1991). 《Type Theory and Functional Programming》. Addison-Wesley. ISBN 0-201-41667-0.
Granström, Johan G. (2011). 《Treatise on Intuitionistic Type Theory》. Springer. ISBN 978-94-007-1735-0.

외부 링크

EU 유형 프로젝트: 튜토리얼 – Types Summer School 2005 강의록 및 슬라이드
n-범주 - 정의 개요 – 존 바에즈와 제임스 돌란이 로스 스트리트에게 보낸 편지, 1995년 11월 29일

[1] Bertot, Yves; Castéran, Pierre (2004). 《Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions》. Texts in theoretical computer science. Berlin Heidelberg: Springer. ISBN 978-3-540-20854-9.

[2] Clairambault, Pierre; Dybjer, Peter (2014). 《The biequivalence of locally cartesian closed categories and Martin-Löf type theories》. 《Mathematical Structures in Computer Science》 (영어) 24. arXiv:1112.3456. doi:10.1017/S0960129513000881. ISSN 0960-1295. S2CID 416274.

[3] Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in Martin-Löf's Type Theory. Oxford University Press, p. 90.

[4] Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; L.; E. (2006). 《Innovations in computational type theory using Nuprl》. 《Journal of Applied Logic》 4. 428–469쪽. doi:10.1016/j.jal.2005.10.005.

[5] Altenkirch, Thorsten; Anberrée, Thomas; Li, Nuo. Definable Quotients in Type Theory (PDF) (보고서). 2024년 4월 19일에 원본 문서 (PDF)에서 보존된 문서.

[6] Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; L.; E. (2006). 《Innovations in computational type theory using Nuprl》. 《Journal of Applied Logic》 4. 428–469쪽. doi:10.1016/j.jal.2005.10.005.

[7] Norell, Ulf (2009). 〈Dependently typed programming in Agda〉. 《Proceedings of the 4th international workshop on Types in language design and implementation》. TLDI '09. New York, NY, USA: ACM. 1–2쪽. CiteSeerX 10.1.1.163.7149. doi:10.1145/1481861.1481862. ISBN 9781605584201. S2CID 1777213.

[8] Brady, Edwin (2013). 《Idris, a general-purpose dependently typed programming language: Design and implementation》. 《Journal of Functional Programming》 23. 552–593쪽. doi:10.1017/S095679681300018X. ISSN 0956-7968. S2CID 19895964.

[9] Martin-Löf, Per (1998). 《An intuitionistic theory of types, Twenty-five years of constructive type theory (Venice,1995)》. Oxford Logic Guides 36. New York: Oxford University Press. 127–172쪽.

[10] Martin-Löf, Per (1975). 〈An intuitionistic theory of types: predicative part〉. 《Studies in Logic and the Foundations of Mathematics》. Logic Colloquium '73 (Bristol, 1973). Amsterdam: North-Holland. 73–118쪽.

[11] Martin-Löf, Per (1982). 〈Constructive mathematics and computer programming〉. 《Studies in Logic and the Foundations of Mathematics》. Logic, methodology and philosophy of science, VI (Hannover, 1979). Amsterdam: North-Holland. 153–175쪽.

[MartinLöf1984-12] Martin-Löf, Per (1984). 《Intuitionistic type theory, Studies in Proof Theory (lecture notes by Giovanni Sambin)》 1. Bibliopolis. iv, 91쪽.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]