직관적 유형 이론

직관적 유형 이론(Martin-Löf 유형 이론)은 수학의 대안적 기초이자 유형 이론이다.직관적 유형 이론은 1972년에 처음 발표한 스웨덴의 수학자이자 철학자인 페르 마르틴 뢰프에 의해 만들어졌습니다.유형 이론에는 여러 가지 버전이 있다: 마틴-뢰프는 이론의 집중적 및 확장적 변형을 제안했고, 지라드의 역설에 의해 모순되는 것으로 보여지는 초기 추정 버전은 서술적 버전으로 대체되었다.그러나 모든 버전은 종속 유형을 사용하여 구성 로직의 핵심 설계를 유지합니다.

설계.

마틴-뢰프는 수학적 구성주의의 원리에 대한 유형 이론을 설계했다.구성주의는 "증인"을 포함하기 위해 어떤 존재 증거도 필요로 한다.따라서 "1000보다 큰 소수가 존재한다"는 증거는 모두 소수와 1000보다 큰 특정 숫자를 식별해야 합니다.직관적 유형 이론은 BHK 해석을 내면화함으로써 이러한 설계 목표를 달성했습니다.흥미로운 결과는 증명들이 검사, 비교, 조작될 수 있는 수학적 개체가 된다는 것이다.

직관적 유형 이론의 유형 생성자는 논리적 연결과 일대일 대응 관계를 따르도록 만들어졌습니다.예를 들어 논리접속형 시사(${\displaystyle }$ ${\displaystyle ⟹}$ \ $displaystyle$A \ $implies$B$$)는 함수 유형(${\displaystyle }$ ${\displaystyle \to }$ \ $displaystyle$A \ $to$B $$)에 대응합니다.이 대응관계는 Curry-Howard 동형사상이라고 불립니다.이전의 유형 이론들 또한 이 동형성을 따랐지만, 마틴-뢰프의 것이 종속 유형을 도입함으로써 그것을 술어 논리로 확장한 최초의 이론이었다.

유형 이론

직관적 유형 이론은 3가지 유한 유형을 가지고 있으며, 5가지 다른 유형 생성자를 사용하여 구성됩니다.정형 이론과 달리 유형 이론은 프레지 이론과 같은 논리 위에 구축되지 않습니다.그래서 유형 이론의 각각의 특징은 수학과 논리의 특징으로서 두 가지 역할을 한다.

유형 이론에 익숙하지 않고 집합 이론을 알고 있는 경우 간단한 요약은 다음과 같습니다.집합이 요소를 포함하는 것과 마찬가지로 유형에도 항이 포함됩니다.항은 한 가지 유형에만 속합니다.2${\displaystyle }$+ $(디스플레이 스타일$ 2$+2)$ $및$ 2${\displaystyle }$†$$($디스플레이 스타일$ 2$\cdot$2)와$$ $같은{\displaystyle \mathrm{}}$ 용어는 4와 같은 표준 용어로 계산됩니다.자세한 내용은 유형 이론 문서를 참조하십시오.

0타입, 1타입, 2타입

3가지 유한 타입이 있습니다.0 유형에는 0개의 항이 포함됩니다.1 유형에는 1개의 표준 항이 포함됩니다.그리고 2타입에는 2개의 표준항이 포함되어 있습니다.

0 유형은 0개의 항을 포함하므로 빈 유형이라고도 합니다.그것은 존재할 수 없는 것을 나타내기 위해 사용된다.또한 $§$ (\$displaystyle$ \bot$)$이라고 쓰여져 있으며 입증할 수 없는 모든 것을 나타냅니다.(즉, 그 증거는 존재할 수 없습니다.)그 결과 부정은 해당 함수로 정의됩니다.${\displaystyle \mathrm{}a}$ ${\displaystyle A}$ : ${\displaystyle \to }$ ${\$ \$display$ \$neg$ A$$:=$A\to\$bot$$$}.$

마찬가지로 1타입에는 1개의 표준항이 포함되어 존재감을 나타냅니다.유닛 타입이라고도 불립니다.이는 종종 입증될 수 있는 제안을 나타내며, 따라서 때로는${\displaystyle \mathrm{}}$"\$displaystyle$\top$"$이라고 쓰여집니다$.$

마지막으로, 2가지 유형은 2개의 표준 항을 포함합니다.이것은 두 값 사이의 확실한 선택을 나타냅니다.부울 값에는 사용되지만 명제에는 사용되지 않습니다.명제는 1가지 유형으로 간주되며, 증명되지 않거나(0가지 유형) 어느 쪽이든 증명되지 않을 수 있습니다(제외 중간 법칙은 직관적 유형 이론에서 명제를 지원하지 않습니다).

σ형 컨스트럭터

δ타입에는 순서쌍이 포함되어 있습니다.일반적인 순서쌍(또는 2-튜플) 타입과 마찬가지로, δ타입은 A$(\displaystyle$A$$\$times$ B$)$와$$B(\$displaystyle$ B$)$의 2가지 다른 유형의 데카르트 $제품$인 A(\displaystyle A\times B)를 설명할 수 있습니다.논리적으로 이러한 순서쌍은 $A(\displaystyle$ B$)$의 증명과 B(\displaystyle B$)$을 보유합니다.에는 A$$ B ( \ $displaystyle$A \$wedge$B )라고 쓰여진 타입이 표시될 수 있습니다.

δ타입은 타입에 의존하기 때문에 일반적인 순서쌍 타입보다 강력합니다.순서쌍에서 두 번째 항의 유형은 첫 번째 항의 값에 따라 달라질 수 있습니다.예를 들어 쌍의 첫 번째 항은 자연수이고 두 번째 항의 유형은 첫 번째 항과 같은 길이의 벡터일 수 있습니다.이러한 유형은 다음과 같이 기술됩니다.

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

집합이론 용어를 사용하면 집합의 색인화된 분리 결합과 유사하다.일반적으로 순서가 매겨진 쌍의 경우 두 번째 항의 유형은 첫 번째 항의 값에 의존하지 않습니다.따라서 데카르트 $곱{\displaystyle \mathbb{}}$N ×$$ {\$displaystyle${\$mathbb${$N}\times${\$mathbb {R}}$을(를) 기술하는 유형은 다음과 같습니다.

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

여기서 주의할 점은 첫 번째 용어 ${displaystyle$ n$\}$의 값은 두 번째 $용어$인 R${$의 유형에 따라 달라지지 않는다는 것입니다.

δ 타입은 수학에서 사용되는 보다 긴 의존형 튜플과 대부분의 프로그래밍 언어에서 사용되는 레코드 또는 구조를 구축하기 위해 사용할 수 있습니다.의존형 3태플의 예로는 2개의 정수를 들 수 있습니다.첫 번째 정수가 두 번째 정수보다 작다는 증명은 다음과 같습니다.

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

의존형 타입을 사용하면 δ타입이 존재 수량자 역할을 수행할 수 있습니다."$P{\displaystyle \mathbb{}}$$)\displaystyle$$P$$(n)$가 $증명$됨$\$$displaystyle$ n$"$이라는 문장은 순서쌍의 유형이 됩니다.첫 번째 항목은 $(\$의 값$$n(\$displaystyle$n})이고$$$$ 두 번째 항목은 프로입니다./${\displaystyle P}$ (${\displaystyle }$n$$) { $display style P$( n )$$。두 번째 항목의 유형${\displaystyle (P}$( n$$)의 증명){ $display p$ ($n$ )$$） 。주문된 쌍의 첫 부분 값($$ { $display style$ n$$})에 따라 달라집니다.유형은 다음과 같습니다.

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

π형 컨스트럭터

δ타입에는 함수가 포함되어 있습니다.일반적인 기능 타입과 마찬가지로 입력 타입과 출력 타입으로 구성됩니다.그러나 반환 유형은 입력 값에 따라 달라질 수 있다는 점에서 일반적인 함수 유형보다 강력합니다.유형 이론의 함수는 집합 이론과 다르다.집합론에서는 순서쌍 집합에서 인수의 값을 검색합니다.유형 이론에서, 인수는 항으로 대체되고 그 항에 계산("축소")이 적용됩니다.

예를 들어 $자연수{\displaystyle }$ n$${\$displaystyle$ n$\}$이 지정되면$n$ {\$displaystyle$ n$}$개의$$ $실수$가 포함된 벡터를 반환하는 함수의 유형이 다음과 같습니다.

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

출력 유형이 입력 값에 따라 달라지지 않는 경우 함수 유형은$\to {\displaystyle }$(\$displaystyle$\to$$})로 간단하게 작성되는 경우가 많습니다. 따라서 N ${\displaystyle \to }$ {\$style {\mathbb {N}$~ {\$mathbb {R}}}$은 자연수에서 실수까지의 함수 유형입니다.이러한 δ타입은 논리적인 의미에 대응합니다.$논리명제{\displaystyle }$ A ${\displaystyle ⟹}$ ${\displaystyle B}$( \ $displaystyle$A \ $implies$B )는 타입 A ${\displaystyle \to }$ ( \ $displaystyle$A \ $to$B $)$에 대응하고$$ 있으며, 여기에는 증명서를 취득하여 증명서를 반환하는 함수가 포함되어 있습니다.이 유형은 다음과 같이 보다 일관되게 작성될 수 있습니다.

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

δ타입은 범용정량화를 위한 로직에도 사용된다."$n타입 N$의 $n개$$(\displaystyle$ {N$\},$ $P$(n)\$displaystyle$P$(n$$)$ is provided"라는 문장은 $N$의$n개$(\displaystyle ${N})$부터 P의 $증명{\displaystyle (n})$까지 함수가 된다.따라서 n$${$displaystyle$ n$}$ $값$이 지정되면 함수는 해당 값에 대해 P$($ ) {$displaystyle$ P$()$가 $보유$하고 있다는 증거를 생성합니다.유형은 다음과 같습니다.

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

= 유형 생성자

=-type은 두 가지 용어로 작성됩니다.$2{\displaystyle \mathrm{}}$+$$ ( $displaystyle$2 +$2$ )$및$ 2${\displaystyle 2}$2 ( $displaystyle$2 \ $cdot 2$)의 2개의 용어를 지정하면 새로운 $타입2{\displaystyle \mathrm{}}$ ${\displaystyle +}$ ${\displaystyle 2}$ ${\displaystyle 2}$ ( $displaystyle$2 + 2$= 2$ \ $cdot$2$$)를 작성할 수 있습니다.이 새로운 유형의 항은 쌍이 동일한 표준 항으로 축소되는 증거를 나타냅니다.따라서 2${\displaystyle }$+ $(디스플레이 스타일$ 2$+2$)와 2$$$style$ $2($디스플레이 $스타일$ 2\$cdot$2)는 $모두$ $표준{\displaystyle \mathrm{}}$ 용어$$4$($스타일 4)로 ${\displaystyle \mathrm{계산}}$되므로, ${\displaystyle 2}$ + 2${\displaystyle =}$ ${\$ 2($디스플레이$ 스타일$2+2=2\cdot$ 2$)$의 용어가 있을 것이다. 직관적 유형 이론에서는 =의 용어와 반사율이라는 용어가 있다.

${\displaystyle\operatorname{refl}{mathbin {:}}\cisco_{a{\mathbin {:}}A}(a=a).}$

1 ${\displaystyle =}$ {$displaystyle$ 1$=2}$와 $같은{\displaystyle \mathrm{}}$ = 유형을 생성할 수 있지만, 이 경우 새로운 유형의 용어를 만들 수 없습니다.실제로 1 $= 2$의 $항$을 만들 수 있다면, $"\displaystyle \bot$의 항을 만들 수 있습니다. 이를 함수에 넣으면 $유형{\displaystyle \mathrm{}}$ 1 ${\displaystyle =}$ ${\displaystyle 2}$ ${\displaystyle \to }$ $⊥$ \$displaystyle$ 1 $= 2 \to$ \bot $\}$의 함수가 생성됩니다. 왜냐하면 $→$ $display$ style $\ldots \to$ \to \bot 이론이란 직관이론을 정의하기 때문입니다$.$부정에는, 「$」({displaystyle \neg$ ($1=2)})$ 또는$$ 마지막으로 「$1{\displaystyle \mathrm{}2}$2$」(\{$$displaystyle$ 1$\neq$ 2$)$가 됩니다.

증명의 평등은 증명 이론의 활발한 연구 분야이며 호모토피 유형 이론과 다른 유형 이론의 발전을 이끌었다.

유도형

유도 유형을 사용하면 복잡한 자기 참조 유형을 생성할 수 있습니다.예를 들어, 자연수의 링크 리스트는 빈 리스트이거나 자연수와 다른 링크 리스트의 쌍입니다.유도 유형을 사용하여 트리, 그래프 등과 같은 무한 수학 구조를 정의할 수 있습니다.실제로 자연수 유형은 0$(\displaystyle$ 0$)$ $또는$ 다른 자연수의 후속인 유도 유형으로 정의할 수 있습니다.

유도형에는 $0{\displaystyle \mathrm{}}$: N$$(\$displaystyle$ 0$math$ mathbin ${:}}$ {\$mathbb${$N}}}$과${\displaystyle (}와{\displaystyle }$) 후속 ${\displaystyle 함수\mathbb{}}$ S : N$$ ${\displaystyle N\mathbb{}}$ (\$displaystyle$S {\$mathbbin {:}}} {\mathbbb${N$\}\}\}\}\}$과(와) 같은 새로운 상수가 정의됩니다. S {\$displaystyle$ S$}$에는 정의되지 않기 $때문$입니다.${\displaystyle \mathrm{S}}$ 0$(\displaystyle S0)$ 및$$ ${\displaystyle S}$ ${\displaystyle S}$ $(\displaystyle SSS0)$과 같은 ms는 자연수의 표준 용어가 됩니다.

유도형에 대한 증명은 유도에 의해 가능하다.각각의 새로운 귀납 유형에는 고유한 귀납 규칙이 있습니다.$모든$ 자연수의 $술어{\displaystyle }$ P${\displaystyle ()}$를$증명$하려면 다음 규칙을 사용합니다.

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

직관적 유형 이론에서 귀납적 유형은 잘 기반을 둔 나무의 유형인 W-타입의 관점에서 정의된다.나중에 유형 이론에서 더 불분명한 종류의 자기 참조성을 가진 유형에서 작업할 수 있도록 유도 유형, 유도-재귀 및 유도-유도를 생성했다.유도 유형이 높을수록 항 간에 동일성을 정의할 수 있습니다.

우주형

우주 유형을 사용하면 다른 유형 생성자를 사용하여 생성된 모든 유형에 대한 증명을 작성할 수 있습니다.우주의 모든 ${\displaystyle {유형}_{\mathrm{}}}$U 0$({$$displaystyle$${U}}_{$0$$})은 0${\displaystyle ,1}$, $2,$,,${\displaystyle }$,, {\,$=,$ \$sigma,$ \$Pi$, =} 및$$ 유도 $유형$ 생성자의 조합으로 생성된 유형에 매핑할 수 있습니다.단, 패러독스를 피하기 위해 ${\displaystyle U_{\mathrm{}}}$ 0$($표시 ${\displaystyle {스타일}_{\mathrm{}}}$ {$U{\displaystyle {\mathcal{}}_{}}$}$_{0})$에는 U 0$($ 스타일 ${U}_{0$에 매핑되는 용어가 없습니다.

모든 "작은 유형" $및{\displaystyle {\mathcal{}}_{}}$ ${\displaystyle U_{\mathrm{}}}$ 0$({$에 대한 증명을 작성하려면 ${\displaystyle U_{\mathrm{}}}$ 1$({$을 $사용$해야 합니다. U $({displaystyle$ {$U}_0$은 U $($유형 {$displaystyle {U})$에 대한 용어를 포함하지만 U 1(유형 {\displaystyle {$0$은 비슷하지 않습니다.$({$2$\}).$ 우주에는 서술적 계층구조가 있으므로 $고정{\displaystyle }$상수 k({$displaystyle$k$$}) 우주에 대한 증거를 수량화하기 위해 ${\displaystyle {Uk}_{}}$ ${\displaystyle {+}_{}}$ $({$1})을 사용할 수 ${\displaystyle {\mathcal{있습니다}}_{}}$.

우주형은 유형 이론의 까다로운 특징이다.마르틴-뢰프의 원래 유형 이론은 지라드의 역설에 대해 설명하기 위해 바뀌어야 했다.이후 연구는 "슈퍼 우주", "마흘로 우주", 그리고 추정 우주와 같은 주제들을 다루었다.

판단

직관적 유형 이론의 공식적인 정의는 판단을 사용하여 작성된다.예를 들어,$$"$A{\displaystyle }$\$displaystyle$$A$\$displaystyle$B$$$\$displaystyle\${$$a$: $:$ ${\displaystyle \underset{}{}}$\$displaystyle$\displaystyle$\sum:$$A}B}$는 유형이다" "유형", "and" 및 "만약..."의 판단이 있다.그럼..."식 $"{\displaystyle \underset{a}{}}$:$$ \ $displaystyle$\$textstyle \ sum$ _ {$a$:$A}B}$는 판단이 아니라 정의되는 유형입니다.

유형 이론의 이 두 번째 수준은 특히 평등에 관한 한 혼란스러울 수 있습니다.4 ${\displaystyle =2}$ +$$ ({$displaystyle$ 4$=2+2$)$$라고 $하는{\displaystyle \mathrm{}}$ 용어 균등성에 대한 판단이 있습니다.이것은 두 항이 같은 표준 항으로 환원된다는 진술이다.A$$${\displaystyle =}$ $($$표시$ $스타일$ A$$$= B$의 $모든{\displaystyle }$ 요소가 B$(표시 스타일$ B$)$의 요소이며, 그 반대도 마찬가지라는 판단도 있다.유형 레벨에는 $유형{\displaystyle \mathrm{}}$ 4 ${\displaystyle =2}$ +$$ ({$displaystyle$ 4$=$$2+2$)가$$ 있으며$,$ 4 ({$displaystyle$ 4}) $및$ 2 +$$ ({$displaystyle$ 2$+2})$가 같은 값으로 감소한다는 $증거$가 있는 경우 용어를 포함합니다.(이 유형의 용어는 균등성 판단을 사용하여 생성됩니다.)마지막으로 영어 수준의 평등성이 있습니다.${\displaystyle 이}$는 정식 용어 SS S $(\displaystyle SSS0$을 나타낼 때 4(\$displaystyle$ 4$)$와 4$(\$displaystyle 4)를 사용하기 때문입니다.Martin-Löf는 이와 같은 동의어를 "definitally equal"이라고 부릅니다.

아래의 판결에 대한 설명은 Nordström, Petersson 및 Smith의 논의를 기반으로 한다.

형식 이론은 유형 및 대상과 함께 작동합니다.

유형은 다음과 같이 선언됩니다.

• ${\displaystyle A\\mathsf {Type}}$

개체가 존재하며 다음과 같은 경우 유형입니다.

• ${\displaystyle a440mathbin {:}}A}$

오브젝트는 같게 할 수 있습니다.

• ${\displaystyle a=b}$

또한 유형은 동일할 수 있습니다.

• ${\displaystyle A=B}$

다른 유형의 개체에 종속된 유형이 선언되었습니다.

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

치환에 의해 제거됨

• ${\displaystyle B}$[${\displaystyle x}$ / $]{$ $displaystyle$B [$x$ / $a$$변수{\displaystyle }$ x$${ $displaystyle$ x$$}를$$ B {$displaystyle$B $\}$의 객체$$a { $displaystyle$ a$$}로$$ 바꿉니다.

다른 유형의 개체에 의존하는 개체는 두 가지 방법으로 수행할 수 있습니다.오브젝트가 "추출"된 경우, 다음과 같이 기록됩니다.

• ${\displaystyle [x]b}$

치환에 의해 제거됨

• ${\displaystyle b}$[${\displaystyle x}$ / $]{$ $displaystyle$$$b [$x$ / $a$ $변수{\displaystyle }$x {\$displaystyle$ x$}$를 b$${\$displaystyle$ b$\}$의 $객체{\displaystyle }$a {\$displaystyle$ a$}$로 바꿉니다.

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

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

여기서 S$(\displaystyle$ S$)$는 객체에 따라 일정한 객체입니다.이것은 추상화와 관련이 없습니다.S$(\displaystyle$ S$)$와 $같은{\displaystyle }$ 상수는 등식을 정의하여 제거할 수 있습니다.여기서 덧셈과의 관계는 동등성과 패턴 매칭을 사용하여$S$의 재귀적 측면을 처리하도록 정의됩니다.\ $displaystyle$S$$:

${\displaystyle {displaystyle}\operatorname {add}&{\mathbin {:}\(\mathbb {N} \times \mathbb {N} )\to \\operatorname {add} (0,b)&\operatorname {add} (S(S(a),\operatorname {add})\s})\opername {add} \mathb} \mathb} \mathb} \mathb} \mathb} \mathb} \math$

$(\displaystyle$ S$)$는 불투명 상수로 조작되며 내부 치환 구조가 없습니다.

그래서 사물이나 유형, 이런 관계들은 이론에서 공식을 나타낼 때 사용합니다.기존 객체, 유형 및 관계에서 새 객체, 유형 및 관계를 작성하기 위해 다음과 같은 판단 스타일이 사용됩니다.

$\displaystyle \Gamma \vdash \sigma \\mathsf {Type}}$	「」는, 콘텍스트 「」의 적절한 형식입니다.
$\displaystyle \Gamma \vdash t{\mathbin {:}}\sigma }$	t는 컨텍스트I에서 타입 '의 적절한 형식 용어입니다.
$\displaystyle \Gamma \vdash \sigma \equiv \tau }$	「」와「」는, 컨텍스트 「」에서 같은 타입입니다.
$\displaystyle \Gamma \vdash t\equiv u {\mathbin {:}}\sigma }$	t와 u는 컨텍스트I에서 타입I 의 조건이 판별적으로 동일합니다.
$\displaystyle \vdash \Gamma \\mathsf {Context}}$	γ는 입력 전제 조건의 적절한 컨텍스트입니다.

관례상 다른 모든 유형을 나타내는 유형이 있습니다.U${$${\displaystyle \mathrm{displaystyle}}$ {$U}}(또는$ Set\displaystyle \$$operatorname ${Set})$라고 $합니다{\displaystyle \mathcal{}}$.U${$는 타입이기 $때문$에 멤버는 오브젝트입니다.각 오브젝트를 대응하는 타입에 매핑하는 ${\displaystyle \mathrm{의존형}}$ El$\displaystyle\operatorname{El}$이 있습니다.대부분의 ${\displaystyle \mathrm{텍스트}}$에서 El$(표시$ 스타일$)$은 사용되지$$ 않습니다$.$문맥에서 독자는 거의 항상 A$(\displaystyle$ A$)$가 유형을 지칭하는지, 또는 U$(\$에서 해당 유형에 해당하는 개체를 지칭하는지 알 수 있습니다.

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

논리를 구현하기 위해 각 제안에는 고유한 유형이 지정됩니다.이러한 유형의 개체는 제안을 증명할 수 있는 여러 가지 가능한 방법을 나타냅니다.제안에 대한 증거가 없는 경우, 그 유형에는 객체가 없습니다.명제에서 작업하는 "and" 및 "또는"와 같은 연산자는 새로운 유형 및 새로운 개체를 도입합니다.$따라서{\displaystyle }$A × $($$디스플레이$ $스타일$ A$\$$times$ B$)$는 $유형{\displaystyle }$A(\$displaystyle$ A)와$$유형 B(\$display$ style B$)$에 따라 달라집니다.해당 종속 유형의 개체는 A$(\displaystyle$ A$)$와$$B(\$displaystyle$ B$)$의 모든 개체 쌍에 대해 존재하도록 정의됩니다. A$(\displaystyle$ A$}$ $또는$ B$(\$$displaystyle$ B$)$가 증거가 없고 빈 유형인 $경우{\displaystyle }$ A$displaystyle$ A$\times$ B$)$를 $나타내는{\displaystyle }$ 새로운 유형도 비어 있습니다.

이 작업은 다른 유형(부울란, 자연수 등)과 해당 연산자에 대해 수행할 수 있습니다.

유형 이론의 범주 모형

범주 이론의 언어를 사용하여, R. A. G. 실리씨는 유형 이론의 기본 모델로서 국소적 데카르트 닫힌 범주(LCCC)의 개념을 도입했습니다.이것은 Hofmann과 Dybjer에 의해 Categories with Familys 또는 Cartmell의 ^[1]초기 연구에 기초하여 Categories with Attributes로 개선되었습니다.

패밀리가 있는 범주는 펑터 T : C^op → Fam(Set)과 함께 컨텍스트의 범주 C(개체가 컨텍스트이고 컨텍스트 형태소가 치환)이다.

Fam(Set)은 집합의 범주이며, 개체는 "색인 집합" A와 함수 B: X → A의${\displaystyle }$쌍${\displaystyle (A}$${\displaystyle ,}$ $){style (A, B)}{$style (A, B)})이고, 형태론은 함수 f: A = A'와 g: X → X'의 쌍이며, 다른 B = X'는 다음과_° 같다.

펑터 T는 컨텍스트 G에 ${\displaystyle \mathrm{Ty}}$($G)\displaystyle$ Ty$(G$${\displaystyle )\backslash }$displaystyle Ty(G$)\displaystyle$ A$:Ty(G$$displaystyle$ $(G,A)\displaystyle$ Tm(G$,$)\ty(G$$)\displaysty($G{\displaystyle }$)\displaysty(G)\displaysty${\displaystyle \backslash }$ty\ty\ty\ty\ty\ty\displaysty\ty\를 할당합니다.함수자에 대한 공리는 이러한 것들이 치환과 조화롭게 작동하도록 요구한다.치환은 보통 Af 또는 af 형식으로 작성됩니다.A는 $G)\displaystyle$Tm(G,$)\displaystyle$ Tm$(G,A$$displaystyle{\displaystyle }$ Tm(G,A)\displaystyle Tm(G,A$)\$displaystyle Tm(G,A)\displaystyle Tm(G)\displate)\disple Tm${\displaystyle (}$G)\disple Tm)\disple Tm(D)\$disple$ Tm)\disple${\displaystyle \mathrm{여기}}$서 A${\displaystyle }$$f$ :${\displaystyle T}$ ${\displaystyle y}$ ( D )$$$a$ a f : $Ty ( D$ ) 、 ${\displaystyle f}$: ${\displaystyle \mathrm{Tm}}$ ${\displaystyle (}$ ${\displaystyle D}$, ${\displaystyle \mathrm{Af}}$ )$$、 $f$: $Tm ( D$ , $Af$)$$。

카테고리 C에는 단말 객체(빈 컨텍스트)와 오른쪽 요소가 왼쪽 요소의 컨텍스트 유형인 이해(context extension)라는 제품 형식의 최종 객체가 포함되어야 합니다.G가 $콘텍스트$이고${\displaystyle A}$ : ${\displaystyle Ty}$ ($$G ) \ $displaystyle A$ :$Ty$ ( G$$)$$\ displaystyle ( G , $A$)$$\ $displaystyle$ ($G$ , A$$) \ displaystyle ( G , A ) ${\displaystyle \mathrm{final}}$ 이 매핑p : D → G ,${\displaystyle }$q : Tm ( D , Ap ) $。{\displaystyle }$

Martin-Löf와 같은 논리적 프레임워크는 문맥 의존형 유형 및 용어 집합의 폐쇄 조건의 형태를 취한다. 즉, 집합이라고 하는 유형이 있어야 하며, 각 집합에는 종속합 및 곱의 형태로 유형이 폐쇄되어야 한다는 것이다.

서술 집합론과 같은 이론은 집합의 종류와 그 요소에 대한 폐쇄 조건을 표현한다: 종속합과 곱을 반영하는 연산과 다양한 형태의 귀납적 정의 하에서 폐쇄되어야 한다.

확장과 집중

근본적인 차이는 확장형과 집중형 이론이다.확장형 이론에서 정의적 (즉, 계산적) 평등은 명제적 평등과 구별되지 않으며, 이것은 증거를 필요로 한다.그 결과 확장형 이론에서는 이론의 프로그램이 종료되지 않을 수 있기 때문에 유형 확인을 결정할 수 없게 됩니다.예를 들어, 그러한 이론은 Y-컴비네이터에게 활자를 줄 수 있게 한다; 이것의 자세한 예는 마틴-뢰프의 활자 ^[2]이론의 노드스툼과 피터슨 프로그래밍에서 찾을 수 있다.그러나 이것이 확장형 이론이 실용적인 도구의 기반이 되는 것을 막지는 않는다. 예를 들어 NuPRL은 확장형 이론을 기반으로 한다.

반면, 집중형 이론의 유형 확인은 결정 가능하지만, 집중형 추론은 세토이드나 유사한 구조를 사용해야 하기 때문에 표준 수학 개념의 표현은 다소 더 번거롭다.예를 들어 정수, 유리수, 실수와 같이, 이것 없이는 표현하기 어렵거나 표현할 수 없는 많은 일반적인 수학적 객체들이 있다.정수와 유리수는 세토이드 없이 표현할 수 있지만, 이 표현은 사용하기 어렵다.코시 실수는 ^{[3][full citation needed]}이것 없이는 나타낼 수 없다.

호모토피 타입 이론은 이 문제를 해결하는 데 효과가 있습니다.이를 통해 1차 생성자(값 또는 점)뿐만 아니라 고차 생성자(즉, 요소(경로) 간의 동등성, 등가(호모토피) 간의 동등성, 무한)를 정의할 수 있습니다.

유형 이론의 구현

여러 증명 보조자의 기초가 되는 공식 시스템으로서 다양한 형태의 유형 이론이 구현되어 왔다.많은 것들이 Per Martin-Löf의 아이디어에 기초하고 있지만, 많은 것들이 특징을 추가하거나, 더 많은 공리 또는 다른 철학적 배경을 가지고 있다.예를 들어, NuPRL 시스템은 계산 유형^[4] 이론에 기초하고 Coq는 유도 구조의 미적분에 기초한다.종속 유형은 ATS, 카이엔, 에피그램, 아그다 ^[5]및 이드리스와 ^[6]같은 프로그래밍 언어 설계에도 적용됩니다.

마르틴-뢰프 유형 이론

마르틴-뢰프는 여러 시기에 출판된 여러 가지 유형 이론을 구성했는데, 그 중 일부는 전문가들(장 이브 지라르 및 조반니 삼빈)이 그 서문에 접근할 수 있게 된 시점보다 훨씬 늦은 시점이었다.아래 목록에서는 인쇄된 형태로 설명된 모든 이론을 나열하고 서로 구별되는 주요 특징을 개략적으로 설명합니다.이러한 모든 이론은 종속적 산물, 종속적 합계, 불연속 결합, 유한형 및 자연수를 가지고 있었다.모든 이론은 종속제품 또는 종속합계에 대해 δ-감소를 포함하지 않는 동일한 감소 규칙을 가지고 있었다. 단, 종속제품에 대한 δ-감소가 추가된 MLT79는 예외였다.

MLT71은 Per Martin-Löf에 의해 만들어진 최초의 유형 이론이다.1971년에 프리프린트에 실렸습니다.하나의 우주가 있었지만 이 우주에는 그 자체가 이름이 있었다. 즉, 오늘날 "Type in Type"이라고 불리는 유형 이론이었다.Jean-Yves Girard는 이 시스템이 일관성이 없고 프리프린트가 발행되지 않았음을 보여주었다.

MLTT72는 1972년에 ^[7]출판된 프리프린트로 제시되었다.그 이론은 하나의 우주 V를 가지고 있고 정체성은 ^{[definition needed]}없다.우주는 예를 들어 V 자체에 없는 개체와 같이 V에 있지 않은 개체에 대한 V의 개체군의 종속 곱이 V에 있지 않다고 가정한다는 점에서 "사전적"이었습니다.우주는 러셀의 프린키피아 매스매티카(Principia Mathmatica)로, 즉 "T"V"와 "TtT"를 직접 쓴다(Martin-Löf는 "El"과 같은 추가 생성자 없이 현대의 ":" 대신 """ 기호를 사용한다).

MLTT73은 Per Martin-Löf가 발표한 유형 이론의 첫 번째 정의였다. (그것은 로직 콜로키움 '73에서 발표되었고 1975년에^[8] 출판되었다.)그가 "제안"이라고 부르는 정체성 유형이 있지만, 명제와 나머지 유형의 실질적인 구분이 소개되지 않았기 때문에 이것의 의미는 명확하지 않다.나중에 J-엘리미네이터라는 이름을 얻었지만 이름이 없는 것이 있다(94-95페이지 참조).이 이론에는 무한한 우주₀ V, ..., V_n, ...의 배열이 있다. 우주들은 서술적, 라 러셀 그리고 비누적이다.실제로 115페이지의 Collarary 3.10은 A와_m B가 변환_n 가능한 경우 m = n이라고 말한다.예를 들어, 이것은 이 이론에서 일가성을 공식화하기 어렵다는 것을 의미한다. 즉, 각 V에는_i 수축 가능한 유형이 있지만 i j j에 대해 V와_j V를 연결하는_i 동일성 유형이 없기 때문에 어떻게 그것들을 동등하다고 선언하는지가 불분명하다.

MLT79는 1979년에 발표되었고 ^[9]1982년에 출판되었다.이 논문에서, 마틴-뢰프는 종속 유형 이론에 대한 네 가지 기본적인 판단 유형을 소개했는데, 이는 이후 그러한 시스템의 메타 이론 연구에 기초가 되었다.그는 또한 문맥을 별도의 개념으로 도입하였다(p.16 참조).J-엘리미네이터(MLT73에 이미 등장했지만 이 이름은 없었다)뿐만 아니라 이론을 "확장"으로 만드는 규칙도 있다(p.169).W타입이 있습니다.누적된 서술적 우주들의 무한한 시퀀스가 있다.

Bibliopolis: 1984년부터^[10] Bibliopolis 책에서 유형 이론에 대한 논의가 있었지만, 그것은 다소 개방적이고 특정한 선택 세트를 나타내는 것처럼 보이지 않기 때문에 그것과 관련된 특정한 유형 이론은 없다.

「 」를 참조해 주세요.

• 직관적 논리
• 유형 람다 미적분

메모들

레퍼런스

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

추가 정보

• Giovanni Sambin(1980년)이 기록한 Martin-Löf의 주석
• 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일 John Baez와 James Dolan이 Ross Street에 보낸 편지