유형 이론

수학, 논리학, 컴퓨터 과학에서, 유형 이론은 특정 유형 시스템의 공식적인 표현이고, 일반 유형 이론은 유형 시스템의 학문적 연구입니다.어떤 유형 이론은 이론을 수학의 기초로서 설정하기 위한 대안으로 작용한다.알론조 처치의 유형 δ-calculus와 Per Martin-Löf의 직관적 유형 이론 두 가지가 기초가 되었다.대부분의 컴퓨터화된 교정 시스템은 그 기초에 활자 이론을 사용한다.일반적인 것은 티에리 코캉의 귀납적 구성 미적분이다.

역사

유형 이론은 순진한 집합론과 형식 논리에 기초한 수학적 기초에서의 역설을 피하기 위해 만들어졌다.버트런드 러셀이 발견한 러셀의 역설은 자신을 포함한 "모든 가능한 집합"을 사용하여 집합을 정의할 수 있었기 때문에 존재했다.1902년과 1908년 사이에 버트랜드 러셀은 이 문제를 해결하기 위해 다양한 "유형 이론"을 제안했다.1908년까지 러셀은 1910년에서 1913년 사이에 출판된 화이트헤드와 러셀의 프린키피아 매스매티카에서 두드러지게 특징지어진 "환원성의 축"과 함께 "미화된" 유형 이론에 도달했습니다.이 시스템은 유형의 계층을 만들고 각각의 구체적인 수학적 실체를 유형에 할당함으로써 러셀의 역설을 피했다.특정 유형의 엔티티는 해당 ^[a]유형의 하위 유형으로만 구축되므로 엔티티가 자체를 사용하여 정의되는 것을 방지합니다.러셀의 유형 이론은 집합이 그 자체의 구성원이 될 가능성을 배제했다.

타입이 항상 논리적으로 사용되는 것은 아니다.러셀의 ^[3]역설을 피할 수 있는 다른 기술들이 있었다.알론조 교회의 람다 미적분이라는 특정 논리와 함께 사용했을 때 타입은 확실히 인기를 얻었다.

가장 유명한 초기 예는 처치의 단순형 람다 미적분이다.처치의 유형 이론은^[4] 형식 체계가 원래의 비정형 람다 미적분을 괴롭힌 클린-로저 역설을 피하는 데 도움을 주었다.처치는 그것이 수학의 기초가 될 수 있다는 것을 증명했고 그것은 고차 논리로 언급되었다.

"유형 이론"이라는 말은 일반적으로 람다 미적분학을 기반으로 한 유형 체계를 가리킨다.영향력 있는 시스템 중 하나는 건설적 수학의 기초로서 제안된 페르 마르틴-뢰프의 직관적 유형 이론이다.또 다른 하나는 티에리 코캉의 구성 미적분학으로 Coq, Lean, 그리고 다른 "증명서 작성 프로그램"에 의해 기초가 된다.유형 이론은 호모토피 유형 이론에서 입증되었듯이 활발한 연구 분야이다.

서론

많은 유형 이론이 있어 포괄적인 분류법을 제시하기가 어렵다. 이 논문은 완전한 분류법이 아니다.다음은 주요 접근법 중 몇 가지를 다루는 유형 이론에 익숙하지 않은 사람들을 위한 소개입니다.

기본

용어와 종류

유형 이론에서는 모든 용어에 유형이 있습니다.용어와 그 유형은 종종 "term: type"으로 함께 쓰여집니다.형식 이론에 포함되는 일반적인 유형은 자연수이며, 종종 "$\$ 또는 "nat"로 표기됩니다.다른 하나는 부울 로직 값입니다.그 종류에는 다음과 같은 매우 간단한 용어가 있습니다.

• 0 : nat
• 42 : nat
• true : bool

함수 호출을 사용하여 다른 용어로 용어를 작성할 수 있습니다.유형 이론에서 함수 호출은 "함수 응용 프로그램"이라고 불립니다.함수 어플리케이션은 특정 유형의 용어를 사용하고 다른 유형의 용어를 생성합니다.함수 어플리케이션은 기존의 "function(argument, argument, ...)" 대신 "function argument ..."로 표기된다.자연수의 경우 두 개의 자연수를 사용하는 "더하기"라는 함수를 정의할 수 있습니다.따라서 그 유형에 대한 몇 가지 용어가 더 있습니다.

• add 0 0 : nat
• add 2 3 : nat
• add 1 (add 1 (add 1 (add 1 0)): nat

마지막 용어에서는 작업 순서를 나타내기 위해 괄호가 추가되었습니다.기술적으로, 대부분의 유형 이론은 괄호가 모든 작업에 존재해야 하지만, 실제로 괄호는 쓰여지지 않고, 저자들은 독자들이 그들이 어디에 있는지 알기 위해 우선 순위와 연관성을 사용할 수 있다고 가정합니다.마찬가지로 "$add{\displaystyle }$x {$display style$ x$}$$$$y$${\displaystyle }$ {$display style$ y$}$ 대신 "${\displaystyle }$ ${\displaystyle +}$ {$displaystyle$x+$y$로 표기하는 것이 일반적입니다.따라서 위의 용어는 다음과 같이 고쳐 쓸 수 있습니다.

• 0 + 0 : nat
• 2 + 3 : nat
• 1 + (1 + (1 + 0 ) : nat

항에 변수가 포함될 수도 있습니다.변수에는 항상 유형이 있습니다.따라서 "x"와 "y"가 유형 "nat"의 변수라고 가정하면 다음 용어도 유효합니다.

• x : nat
• x + 2 : nat
• x + (x + y) : nat

"nat"과 "bool"보다 더 많은 종류가 있습니다."add"라는 용어는 "nat"가 아니라 두 "nat"에 적용하면 "nat"에 계산되는 함수입니다."추가" 유형은 나중에 설명하겠습니다.우선, 「컴퓨터의 대상」에 대해 설명할 필요가 있습니다.

계산

유형 이론은 내장된 계산 표기법을 가지고 있다.다음 용어는 모두 다릅니다.

• 1 + 4 : nat
• 3 + 2 : nat
• 0 + 5 : nat

그러나 모두 "5: nat"라는 용어로 계산됩니다.유형 이론에서, 우리는 계산을 언급하기 위해 "축소"와 "축소"라는 단어를 사용합니다.따라서 "0 + 5 : nat"은 "5 : nat"로 감소합니다."0 + 5 : nat$${\ {\ （ \ $displaystyle$ \ $twohead$ right arrow$$$$} 5 : nat" 이라고 쓸 수 있습니다.계산은 기계적인 것으로, 용어의 구문을 고쳐 쓰는 것에 의해서 행해집니다.

변수를 포함하는 항도 줄일 수 있습니다.따라서 "x + (1 + 4) : nat"이라는 용어는 "x + 5 : nat"으로 감소한다. (Church-Rosser 정리 덕분에 한 기간 내의 모든 하위 항을 줄일 수 있다.)

더 이상 줄일 수 없는 변수가 없는 항은 "표준 항"입니다.위의 모든 용어는 정규 용어인 "5 : nat"로 축소됩니다.자연수의 표준항은 다음과 같습니다.

• 0 : nat
• 1 : nat
• 2 : nat
• 기타.

분명히 같은 항으로 계산되는 항은 동일합니다.따라서 "x : nat"을 가정하면 "x + (1 + 4 ) : nat" 및 "x + (4 + 1) : nat"은 둘 다 "x + 5 : nat"로 감소하기 때문에 동일합니다.두 항이 같으면 서로 대체할 수 있습니다.평등은 유형 이론에서 복잡한 주제이고 많은 종류의 평등들이 있다.두 개의 항이 같은 항으로 계산되는 이러한 종류의 평등을 "판결 평등"이라고 합니다.

기능들

유형 이론에서 함수는 용어이다.함수는 람다 항이거나 "규칙에 따라" 정의될 수 있습니다.

람다항

람다 용어는 "(변수 이름: type1 . term)"과 비슷하며 "type1 $→$ {$style$ \$to }$ type2$$"를 가집니다.유형 1 $→$ {\$displaystyle \to }$ type2는 람다 항이 유형 "type1"의 매개변수를 취하고 유형 "type2"의 항으로 계산하는 함수임을 나타냅니다.람다 항 내부의 항은 변수의 유형이 "type1"이라고 가정할 때 "type2" 값이어야 합니다.

람다 항의 예로는 인수를 두 배로 하는 이 함수가 있습니다.

• (x: nat . (x 추가) : nat $→$ \$displaystyle \to$ $}$ nat

변수 이름은 "x"이고 변수 유형은 "nat"입니다.용어(x 추가)는 "x : nat"로 가정할 때 "nat" 유형입니다.따라서 람다 용어의 유형은 "nat $→\displaystyle \to }$ nat$$"입니다. 즉, "nat"을 인수로 지정하면 "nat"로 계산됩니다.람다 항에 대해 감소(일명 계산)가 정의됩니다.함수를 적용(호출)하면 파라미터 대신 인수가 사용됩니다.

앞에서 함수 적용은 함수 용어 뒤에 매개변수를 넣어 작성하는 것을 보았습니다.따라서 "nat" 유형의 파라미터 "5"를 사용하여 위의 함수를 호출하려면 다음과 같이 입력합니다.

• (x : nat . (x x 추가) 5 : nat

lamda 용어는 type "nat$→$ {\$displaystyle$ \to$$$$} nat"로, "nat"을 인수로 지정하면 type "nat"의 항이 생성됩니다.인수 "5"를 지정했으므로 위의 용어는 유형 "nat"를 가집니다.축소는 변수 "x"의 인수 "5"를 용어 "(추가 x")의 "x"로 대체함으로써 작동하므로, 이 용어는 다음과 같이 계산됩니다.

• (5 5 추가): nat

분명히 계산하면

• 10 : nat

람다 항에는 이름이 없기 때문에 종종 "익명 함수"라고 합니다.읽기 쉽게 하기 위해 람다 용어에 이름을 붙이는 경우가 많습니다.이것은 단지 표기법일 뿐 수학적 의미는 없다.몇몇 작가들은 이것을 "국가적 평등"이라고 부른다.위의 함수에 다음 표기를 사용하여 이름을 지정할 수 있습니다.

• double : nat $→$ \$displaystyle \to$} nat$$ : : = (x : nat . (x 추가))

이것은 위와 같은 기능으로, 단지 다른 방법으로 쓸 수 있습니다.그래서 이 용어는

• double 5 : nat

아직도 계산하다

• 10 : nat

종속 유형

종속 유형은 함수에 의해 반환되는 유형이 인수 값에 따라 달라지는 경우입니다.예를 들어, 유형 이론이 유형 "bool"을 정의하는 규칙을 가지고 있는 경우, 함수 "if"도 정의합니다.함수 "if"는 3개의 인수를 사용하고 "if true b c"는 "b"로 계산되며 "if false b c"는 "c"로 계산됩니다.하지만 "if a b c"의 유형은 무엇일까요?

"b"와 "c"가 같은 유형일 경우, "b c"가 "b" 및 "c"와 같은 유형일 경우 명백합니다.따라서 "a: bool"을 가정하면,

• a 2 4의 경우 : nat
• 거짓일 경우: bool

그러나 "b"와 "c"의 유형이 다를 경우 "if a b c"의 유형은 "a"의 값에 따라 달라집니다.기호는 인수를 사용하여 유형을 반환하는 함수를 나타낼 때 사용합니다."B"와 "C"와 "a: bool", "b: B"와 "c: C"의 유형이 있다고 가정하면,

• a c의 경우 : (ol a : bool . B $→$ {$displaystyle$ \$to$$$} C $→$ {$displaystyle$ \to$$$$} B C의 경우)

즉, "if" 용어의 유형은 첫 번째 인수의 값에 따라 두 번째 또는 세 번째 인수의 유형입니다.실제로는 "if"를 사용하여 "if"를 정의하지 않지만, 이 소개에서는 너무 복잡합니다.

이 타입은 연산을 포함할 수 있기 때문에 의존형 타입은 놀라울 정도로 강력합니다.수학자가 "x$${\$displaystyle$ x$$$}$가 소수인 $숫자{\displaystyle }$x {\$displaystyle$ x$}$가 존재한다" 또는 "x$${\$displaystyle$ P$(x)}$가 ${\displaystyle \mathrm{유지}}$되는 숫자$x{\displaystyle }$ {\$displaystyle$x}가$$ 존재한다"라고 하면 종속형이라고 표현할 수 있습니다.즉, 이 특성은 특정 "${\displaystyle }"$에 대해 입증되었으며 결과 유형으로 볼 수 있습니다.

종속 입력에는 많은 세부 사항이 있습니다.이 서론에서는 너무 길고 복잡합니다.자세한 내용은 종속 유형 및 람다 큐브에 대한 문서를 참조하십시오.

유니버스

δ-terms는 유형을 반환합니다.그렇다면 수익률의 유형은 무엇일까요?글쎄요, 활자가 들어 있는 활자가 있을 거예요.다른 유형을 포함하는 유형을 "유니버스"라고 합니다.흔히 U$(디스플레이$ 스타일 U$)$라는 기호로 쓰입니다.때로는 U ${\displaystyle {}_{}}$$($$디스플레이{\displaystyle {}_{}}$ $스타일$ U_${0})$ :$$ 1($디스플레이$ 스타일$U_{$1}),$$ ${\displaystyle {U\mathrm{}}_{}}$$$1($디스플레이 스타일 U_{$$1{\displaystyle {}_{}}$})$$$$: U 2($디스플레이$ 스타일$U_{$2}} 등 우주 계층이 존재합니다.

우주는 복잡해만약 우주가 자신을 포함한다면, 그것은 지라드의 패러독스 같은 역설로 이어질 수 있다.이 도입부에는 우주의 세부사항들이 너무 길고 복잡하다.

일반적인 "규칙에 따른" 유형 및 용어

유형 이론은 추론 규칙에 의해 정의된다.위에서 설명한 "기능 코어" 규칙과 유형 및 용어를 작성하는 규칙이 있습니다.다음은 일반적인 유형 및 관련 용어 목록입니다.

목록은 "유도적 유형"으로 끝납니다. 이는 목록의 다른 모든 유형을 구성할 수 있는 강력한 기술입니다.증명 보조자 "Coq"와 "Lean"이 사용하는 수학적 기초는 "귀납적 구성 계산"에 기초한다. "귀납적 구성 계산"(그 "기능적 핵심")은 귀납적 유형의 "구성 계산"이다.

빈 타입

빈 형식에는 항이 없습니다.이 타입은 보통$"\displaystyle$ \bot$"$ ${\displaystyle \mathbb{}}$"$0\$displaystyle $\mathbb${$0}"$으로 표기됩니다.

그것은 무엇인가를 계산할 수 없다는 것을 보여주기 위해 사용된다.유형 "A"의 경우 유형 "A $displaystyle\to\bot"$의 함수를 만들 수 있습니다. "A"에는 항이 없습니다.유형 "A"의 예로는$$"$x{\displaystyle }$$(\displaystyle$x)가 짝수이고 x$(\displaystyle$x)가$$ 홀수인 x(\$displaystyle$ x$)$가 있다"가 있습니다(예 "A"의 구성에 대해서는 아래의 "제품 유형"을 참조하십시오).어떤 타입에 용어가 없는 경우는, 「무인」이라고 합니다.

유닛 타입

단위 유형에는 정확히 1개의 표준 항이 있습니다.유형은 $"\displaystyle \top$ 또는 "${\displaystyle \mathbb{}}${\$displaystyle \mathbb {1}$로 표기되며, 단일 표준 용어는 "*"로 표기됩니다.

단위 유형은 무언가가 존재하거나 계산할 수 있음을 나타내기 위해 사용됩니다.유형 "A"의 경우 유형 " $→$ \$displaystyle \top$\to $}$ A$$"의 함수를 만들 수 있습니다. "A"에는 하나 이상의 항이 있습니다.어떤 타입에 적어도1개의 항이 있는 경우는, 「인재」라고 합니다.

부울형

Boolean 유형에는 정확히 2개의 표준 항이 있습니다.이 유형은 보통 "bool" 또는 "$\$ 또는 "$\$로 표기됩니다.표준 용어는 보통 "참"과 "거짓"입니다.

부울 유형은 다음과 같이 제거기 함수 "if"로 정의됩니다.

• true b c c $↠$ { $displaystyle$ \ $twohead$ right arrow$$$$} b의 경우
• false b c c $↠$ { $displaystyle$\ $twohead$ right arrow$$} c의$$ 경우

제품 종류

제품 유형에는 순서가 매겨진 쌍이 있습니다.유형 "A" 및 "B"의 경우 제품 유형은 "A$$× \$displaystyle \times }$ B$$"로 표기됩니다.표준 항은 생성자 함수 "쌍"에 의해 생성됩니다.조건은 "쌍 a b"입니다. 여기서 "a"는 유형 "A"의 용어이고, "b"는 유형 "B"의 용어입니다.제품 유형은 다음과 같이 제거기 기능 "첫 번째" 및 "두 번째"로 정의됩니다.

• first (a) (a) ${\$ { $display$style \ $twohead$ right arrow$$}a$$
• second (a를 참조)${\$ { $display$style \ $twohead$ right arrow$$} b$$

순서쌍 외에 이 타입은 논리연산자 "and"에 사용됩니다.이는 "A"와 "B"를 포함하기 때문입니다.두 가지 유형 중 하나를 수용하기 때문에 교차로에도 사용됩니다.

유형 이론이 종속적 유형을 갖는 경우 종속적 쌍을 가집니다.종속 쌍에서 두 번째 유형은 첫 번째 항의 값에 따라 달라집니다.따라서 "${\displaystyle \mathrm{}}$\$displaystyle \Sigma }$ a$$:A . B(a)"로 표기되며, "B"의 유형은 "A $→$ \$displaystyle \to }$ U$$"이다.속성 "B(a)"를 가진 "a"의 존재를 나타낼 때 유용합니다.

합계형

합계 유형은 "태그 부착 유니언"입니다.즉, 유형 "A"와 "B"의 경우 유형 "A + B"는 유형 "A" 또는 유형 "B"의 항을 가지며 어느 항을 보유하는지 알고 있다.이 유형은 생성자 "injectionLeft" 및 "injectionRight"와 함께 제공됩니다.호출 "injectionLeft a"는 "a : A"를 사용하여 "A + B" 유형의 정규 용어를 반환합니다.마찬가지로 injectionRight b는 "b : B"를 사용하고 "A + B" 유형의 정규 용어를 반환합니다.유형은 유형 "C"에 대해 제거기 함수 "일치"로 정의되며, "f : A$\to {\displaystyle }$ \displaystyle $\$to } $C"$ 및 "g : B $→$ \displaystyle \to } C$$$$":

• match (injection Left a) C f g ${\$ { $displaystyle$\ $twohead$ right arrow $}$ (f a )
• match (injection Right b) C f g ${\$ { $displaystyle$\ $twohead$ right arrow $}$ (g b )

합계 유형은 논리 또는 합계에 사용됩니다.

자연수

자연수는 보통 페아노 산술 형식으로 구현됩니다.0을 가리키는 표준 용어 "0 : nat"가 있습니다.0보다 큰 표준 값은 생성자 함수 "S : nat $→$ \$displaystyle \to$ $}$ nat"을 사용합니다.즉, "S 0"은 1이고, "S (S 0)"는 2이다."S(S(S 0)"는 3이다.기타. 10진수는 단지 그 용어와 공적으로 동일하다.

• 1 : nat ::= S 0
• 2 : nat ::= S (S 0)
• 3 : nat ::= S (S (S 0))
• ...

자연수는 재귀를 사용하여 모든 nat에 대한 함수를 정의하는 제거기 함수 "R"로 정의됩니다.정의할 함수의 유형인 "P : nat $→$ \$displaystyle \to }$ U$$" 함수를 사용합니다.또한 0의 값인 "PZ : P 0"과 "n"의 값을 "n + 1"의 값으로 변환하는 방법을 나타내는 함수 "PS : P n $→$ {$displaystyle \to }$ P$$ (S n)"가 필요합니다.따라서 계산 규칙은 다음과 같습니다.

• R PZ PS 0 ${\$ ( \ $displaystyle$\ $twohead$ right arrow )$$PZ$$
• R PZ PS ( $S{\displaystyle }$n \ $displaystyle$n$$) ${\$ {\ （ \ $displaystyle$\$twohead$ right arrow $）$PS$$ ( R PZ $PS{\displaystyle }$n \ $displaystyle$n$$)

앞서 사용한 함수 "add"는 "R"을 사용하여 정의할 수 있습니다.

• add : nat $→$ {\$displaystyle \to$$$} nat$$ $→$ {\$displaystyle \to$ $}$ nat : = {\displaystyle \to } nat （ n:nat $→$ {$displaystyle \to$$$} nat ） （ n:nat ） ） 。

아이덴티티 타입

동일 유형은 유형 이론에서 평등에 대한 세 번째 개념입니다.첫 번째는 "notational equality"로, "2 : nat : = (S 0)"와 같이 수학적 의미는 없지만 독자들에게 유용한 정의를 말한다.두 번째는 "판정 평등"으로, 두 항이 "x + (1 + 4)"와 "x + (4 + 1)"과 같이 같은 항으로 계산될 때, 둘 다 "x + 5"로 계산됩니다.그러나 유형 이론은 "정체성 유형" 또는 "제안적 평등"으로 알려진 다른 형태의 평등을 필요로 합니다.

ID 유형이 필요한 이유는 일부 동일한 항이 동일한 항으로 계산되지 않기 때문입니다."x : nat"을 가정하면 "x + 1"과 "1 + x"라는 용어는 같은 항으로 계산되지 않습니다."+"는 "추가" 함수의 표기법이며, "R" 함수의 표기법입니다.「x」의 값이 지정될 때까지 「R」로 계산할 수 없습니다.이 값이 지정될 때까지, 「R」에 대한 2개의 다른 콜은 같은 용어로 계산되지 않습니다.

동일 유형에는 동일한 유형의 두 개의 용어 "a"와 "b"가 필요하며 "a = b"로 표기됩니다.따라서 "x + 1" 및 "1 + x"의 경우 유형은 "x+1 = 1+x"가 됩니다.표준 항은 생성자 "반사성"을 사용하여 생성됩니다.호출 "a"는 "a"라는 용어를 사용하며 "a = a" 유형의 표준 용어를 반환합니다.

아이덴티티 타입을 사용한 연산은 엘리미네이터 함수 "J"를 사용하여 이루어집니다.함수 "J"는 "a", "b" 및 유형 "a = b"의 항에 의존하는 항을 "b"가 "a"로 대체되도록 다시 쓸 수 있도록 한다."J"는 "b"를 "a"로 대체할 수 있는 한 방향이지만, 동일 유형은 반사적이고 대칭적이며 전이적이라는 것을 증명할 수 있다.

표준 항이 항상 "a=a"이고 "x+1"이 "1+x"와 같은 항으로 계산되지 않는다면, 어떻게 "x+1 = 1+x"의 항을 만들 수 있을까요?우리는 "R" 함수를 사용합니다.(위의 '내추럴 넘버'를 참조해 주세요."R" 함수의 인수 "P"는 "(x:nat . x+1 = 1+x)로 정의됩니다.다른 인수는 유도 증명의 일부와 같이 작용하며, 여기서 "PZ : P 0"은 베이스 케이스 "0+1 = 1+0"이 되고 "PS : P n$\to {\displaystyle }$ {$display style$\to$$ } P (S n)"는 유도 증명이 됩니다.기본적으로, 이것은 "x+1 = 1+x"가 "x"를 표준값으로 치환했을 때, 식은 "x+1"과 동일할 것이라고 말한다.이 함수 "R"의 적용 유형은 "x : nat $→$ {\$displaystyle \to }$ x$$+1 = 1+x"입니다.어떤 용어로든 "x+1"을 "1+x"로 대체하기 위해 "J" 함수를 사용할 수 있습니다.이와 같이 아이덴티티 유형은 판단적 평등으로는 불가능한 평등을 포착할 수 있다.

분명히 하자면, "0 = 1" 유형을 생성할 수는 있지만 해당 유형의 항을 생성할 방법은 없습니다.유형 "0 = 1"의 항이 없으면 함수 "J"를 사용하여 다른 항에서 "1"을 "0"으로 대체할 수 없습니다.

유형 이론에서 평등의 복잡성은 그것을 활발한 연구 영역으로 만듭니다. 호모토피 유형 이론을 참조하십시오.

유도형

유도형은 다양한 유형을 만드는 방법입니다.실제로 위에서 설명한 모든 유형 및 그 이상의 유형은 귀납 유형의 규칙을 사용하여 정의할 수 있습니다.유형의 생성자를 지정하면 제거기 함수 및 계산이 구조 재귀에 의해 결정됩니다.

유사하고 더 강력한 활자 제작 방법이 있습니다.여기에는 유도-재귀 및 유도-유도가 포함됩니다.Scott 인코딩이라고 불리는 람다 용어만을 사용하여 유사한 유형을 생성하는 방법도 있습니다.

(주: 유형 이론은 보통 공유도 유형을 포함하지 않습니다.이러한 유형은 무한 데이터 유형을 나타내며 대부분의 유형 이론은 정지된 것으로 입증될 수 있는 함수로 제한됩니다.)

집합론과의 차이점

수학의 전통적인 기초는 논리와 짝을 이룬 이론이다.가장 일반적으로 인용되는 것은 Zermelo-Fraenkel 집합 이론으로, "ZF" 또는 "ZFC"로 알려져 있다.유형 이론은 여러 가지 면에서 이 기초와 다릅니다.

• 집합론은 규칙과 공리를 모두 가지고 있는 반면, 유형론은 규칙만을 가지고 있다.정해진 이론들은 논리 위에 세워져 있다.따라서 ZFC는 1차 로직의 규칙과 그 자체의 공리 양쪽에 의해 정의됩니다.(공리란 논리적 도출 없이 참으로 받아들여지는 논리적 진술입니다.)유형 이론은 일반적으로 공리를 가지고 있지 않고 그들의 추론 규칙에 의해 정의된다.
• 집합론과 논리는 배제된 중간 법칙을 가지고 있다.즉, 모든 정리가 참이거나 거짓이다.유형 이론이 "and"와 "or"의 개념을 유형으로 정의할 때, 그것은 배제의 법칙을 가지지 않는 직관적인 논리로 이어진다.하지만, 그 법은 일부 유형에서 입증될 수 있다.
• 집합론에서는 요소가 하나의 집합으로 제한되지 않는다.요소는 하위 집합 및 다른 집합과의 결합에 나타날 수 있습니다.유형 이론에서 항은 (일반적으로) 한 가지 유형에만 속합니다.서브셋을 사용하는 경우 유형 이론은 술어 함수를 사용할 수도 있고 의존형 곱 유형을 사용할 수도 있습니다.여기서 각 $요소{\displaystyle }$x {\$displaystyle$x}는$$ 서브셋 속성이 x$${\$displaystyle$x$\}$에 대해 유지된다는 증거와 쌍을 이룹니다.유형이 사용되는 경우 유형 이론은 새로운 표준 용어를 포함하는 합체 유형을 사용합니다.
• 유형 이론에는 계산의 개념이 내재되어 있다.따라서 "1+1"과 "2"는 유형 이론에서 서로 다른 용어이지만 같은 값으로 계산됩니다.또한 함수는 람다 항으로 계산적으로 정의됩니다.집합론에서, "1+1=2"는 "1+1"이 값 "2"를 참조하는 또 다른 방법임을 의미한다.유형 이론의 계산은 평등의 복잡한 개념을 필요로 한다.
• 집합론은 보통 숫자를 집합으로 인코딩합니다.(0은 빈 세트, 1은 빈 세트 등을 포함한 세트)자연수의 이론적 정의를 참조하십시오.)유형 이론은 Church 인코딩을 사용하여 함수로 숫자를 인코딩하거나 귀납적 유형으로 보다 자연스럽게 인코딩할 수 있습니다.유도형에 의해 만들어진 생성자 "0"과 "S"는 페아노의 공리와 매우 유사하다.
• Set Theory에는 Set-Builder 표기법이 있습니다.정의할 수 있는 모든 세트를 작성할 수 있습니다.이를 통해 셀 수 없는 집합을 만들 수 있습니다.유형 이론은 통사적이어서 셀 수 없을 정도로 무한한 항으로 제한된다.또한 대부분의 유형 이론은 항상 중단하고 재귀적으로 생성 가능한 항으로 스스로를 제한하기 위해 연산이 필요합니다.그 결과, 대부분의 유형 이론은 실수가 아닌 계산 가능한 숫자를 사용합니다.
• 집합론에서, 선택 공리는 공리이며, 특히 셀 수 없는 집합에 적용될 때 논란이 된다.유형 이론에서 등가 진술은 정리(유형)이며 증명 가능하다.
• 유형 이론에서 증명은 수학적 대상이다."x+1 = 1+x" 유형은 해당 유형의 용어가 없는 한 사용할 수 없습니다.이 항은 "x+1 = 1+x"라는 증거를 나타냅니다.그러므로 유형 이론은 수학적 개체로서 연구될 증거를 열어준다.

유형 이론의 지지자들은 또한 BHK 해석을 통한 구성 수학과의 연관성, Curry-Howard 동형사상에 의한 논리와의 연관성, 범주 이론과의 연관성을 지적할 것이다.

기술적 세부사항

유형 이론은 수학적 논리이다.그것은 판단을 낳는 추론 규칙의 집합이다.대부분의 로직에는 "x$(x)$라는 $용어$는 참" 또는 "x$(x)$라는 $용어$는 올바른 공식"^[5]이라는 판단이 있습니다.유형 이론에는 유형을 정의하고 용어와 유형을 관련짓는 추가 판단이 있습니다.

조건.

논리학의 용어는 상수 기호, 변수 또는 함수 어플리케이션으로 재귀적으로 정의되며, 여기서 용어는 다른 용어에 적용된다.일부 상수 기호는 자연수의 "0", "참", "S" 및 "if"와 같은 함수가 됩니다.따라서 일부 용어는 "0", "S 0", "S x" 및 "참인 경우 0(S 0)"입니다.

판단

대부분의 유형 이론에는 4가지 판단이 있습니다.

• "$\displaystyle$T는$$ 유형입니다."
• ${\displaystyle }$$\displaystyle$t는 $type{\displaystyle }$ T$\displaystyle$T의 용어입니다.$$
• "$Type{\displaystyle {}_{}}$ $($ T_${1})$은 $($ T_${2})$와 동일합니다."
• "t $({$과 ${\displaystyle {t\mathrm{}}_{}}$ 2$({$는 둘 다 $Type{\displaystyle }$T({$displaystyle$T})이며$$ 동일합니다."

그 판단은 가정하에 내려질 수 있다.따라서 "x$\displaystyle$ x$"$는 "bool" $타입$의 용어이고$$y\$display y는$$$"nat" 타입의 용어이며 (x y의 경우)"는 "nat 타입의 용어라고 $가정$할 수 있습니다.가정에 대한 수학적 표기법은 턴스타일 기호 $"\displaystyle \vdash$" 앞에 $$쉼표로 구분된 "term : type$"$ 목록입니다.따라서 예제 문장은 공식적으로 작성됩니다.

• x:bool, y:nat $©$ { $displaystyle$\ $vdash$}$$ (x y의 경우): nat

추측이 없으면 개찰구 왼쪽에 아무것도 없습니다.

• $§$ ${\displaystyle\vdash}$ S$$ :$nat →$ ${\displaystyle$\to$$$}$ nat

전제 조건의 리스트를 「콘텍스트」라고 부릅니다.일부 또는 모든 가정을 나타내기 위해 사용되는 기호$$'$display\displaystyle$ \Gamma$\text{'}$는 매우 흔합니다.따라서 4가지 판단을 위한 공식 표기법은 일반적으로 다음과 같습니다.

판단을 위한 형식 표기법	묘사
${\displaystyle \gamma }$t T \ display $style$\ $Gamma$ \$$vdash T$$ }	$(\displaystyle$ T$)$는 유형입니다(전제조건$\gamma {\displaystyle \mathrm{}}$ { $displaystyle$\ $Gamma$} $$） 。
$\displaystyle \Gamma \vdash t:T}$	${\displaystyle t}$ ${$ $display style$ t$$}는$$ $타입{\displaystyle }$T { $display style$ T$}$의 용어입니다( 전제 조건$\gamma {\displaystyle \mathrm{}}$ { $display$style \ $Gamma$} $$） 。
$\displaystyle \Gamma \vdash T_{1}=T_{2}}$	${\displaystyle {Type\mathrm{}}_{}}$ T1$({$은 $({$와 동일합니다( 전제조건 $\gamma {\displaystyle \mathrm{}}${ \ $displaystyle$\$Gamma$}$$ ） 。
$\displaystyle \Gamma \vdash t_{1}=t_{2}:T}$	$({$ $및$ $({$$displaystyle$$t_{2})$는 모두$T형$이며 동일하다( 전제조건$\gamma {\displaystyle \mathrm{}}$ {\$displaystyle \Gamma$} $$） 。

(주: 용어 평등에 대한 판단은 "판결 평등"이라는 문구가 유래한 것이다.)

판결은 모든 용어에는 유형이 있다고 강제한다.이 유형은 용어에 적용할 수 있는 규칙을 제한합니다.

규칙.

유형 이론의 규칙은 다른 판단의 존재에 근거하여 어떤 판단을 내릴 수 있는지를 말한다.규칙은 수평선을 사용하여 표현되며, 필요한 입력 판단은 라인 위에, 결과 판단은 라인 아래에 있다.람다 항을 생성하는 규칙은 다음과 같습니다.

람다 항을 생성하는 데 필요한 판단이 선을 초과합니다.이 경우, 하나의 판단만 필요하다.즉, "A" 타입의 "a$"$라는 용어와 "${\displaystyle \mathrm{}}$$\$$displaystyle$\Gamma$"$라는 다른 전제조건이 있다고 가정할 때, "B" 타입의 "b$"$라는 용어가 모두 메타 AVARI에 있다고 가정한다.그 결과로 나온 판단은 선을 밑돌고 있다.이 규칙의 결과는 다른 전제 $조건{\displaystyle \mathrm{}}$δ\$displaystyle$$Gamma$에서 새로운 람다 항이 "A $→\displaystyle\to}$B$$"를 갖는다는 것을 나타냅니다.

규칙은 통사적이며 다시 쓰기로 작동합니다.따라서 " $\displaystyle\Gamma"$ ",$$ "a", "A" 등과 같은 메타 변수들은 실제로는 단일 기호뿐만 아니라 많은 기능 애플리케이션을 포함하는 복잡한 용어로 구성될 수 있습니다.

유형 이론에서 특정 판단을 도출하기 위해서는 그것을 도출하는 규칙이 있어야 한다.그런 다음 해당 규칙에 필요한 입력을 모두 생성하는 규칙이 있어야 합니다.그리고 그 규칙에 대한 모든 입력에 대한 규칙입니다.적용된 규칙이 증명 트리를 형성합니다.이것은 보통 Gentzen ^[6]스타일로 그려집니다.여기서 타겟 판단(루트)은 맨 아래에 있고 입력(리브)이 필요 없는 규칙은 맨 위에 있습니다(자연적 감점 #Proofs_and_type_이론 참조).입력이 필요 없는 규칙의 예로는 "nat" 유형의 용어 "0"이 있음을 나타내는 규칙이 있습니다.

유형 이론에는 보통 다음과 같은 몇 가지 규칙이 있습니다.

• 콘텍스트를 작성하다
• 문맥에 가정을 추가하다('전제')
• 가정을 재정비하다
• 변수를 작성하기 위해 가정을 하다
• 판단적 평등을 위한 반사성, 대칭성 및 전이성을 정의한다.
• 람다 항 적용을 위한 대체 정의
• 평등, 치환 등의 모든 상호작용
• 우주를 정의하다

또한 "규칙에 따른" 유형별로 4가지 다른 규칙이 있습니다.

• "type formation" 규칙에서는 유형을 작성하는 방법을 설명합니다.
• "항 소개" 규칙은 "쌍" 및 "S"와 같은 표준 용어와 생성자 함수를 정의합니다.
• "term elimination" 규칙은 "first", "second" 및 "R"과 같은 다른 함수를 정의합니다.
• "계산" 규칙은 유형별 함수를 사용하여 계산을 수행하는 방법을 지정합니다.

규칙의 예:

• 마르틴 뢰프의 직관적 유형 이론의 규칙
• 호모토피 유형 이론서 부록 A.2

유형 이론의 특성

항은 일반적으로 단일 유형에 속합니다.그러나 "서브타이핑"을 정의하는 정해진 이론이 있습니다.

계산은 규칙을 반복적으로 적용하여 이루어집니다.많은 유형 이론들이 강하게 정규화되고 있는데, 이것은 규칙을 적용하는 어떤 순서도 항상 같은 결과로 끝난다는 것을 의미합니다.하지만 일부는 그렇지 않다.정규화 유형 이론에서, 단방향 계산 규칙은 "축소 규칙"이라고 불리며 규칙을 적용하는 것은 용어를 "축소"한다.규칙이 단방향 규칙이 아닌 경우 "변환 규칙"이라고 합니다.

일부 유형의 조합은 다른 유형의 조합과 동일합니다.함수가 "개요"로 간주될 때, 유형의 조합은 대수적 ^[7]항등식과 유사하게 작성될 수 있다.$따라서{\displaystyle \mathbb{}}$ 0${\displaystyle }$+ ${\displaystyle Aa}$A \ $displaystyle$\ $mathbb$${ 0 }$ +$A$ \ $cong$$$$A$$$${\displaystyle 、}1{\displaystyle \mathbb{}}$ × $a A$\ $times$ A$、$${\displaystyle }1{\displaystyle \mathbb{}}$ + ${\displaystyle 1\mathbb{}}$ 2 \ $display$\ $mathbb { 1 }$ + \ $mathbb${ 1 } \ $mathbbb 2$ \ $con 2 。$$(\$ A$^{B\times$ C$}\cong(A^{B})^{C$

악리

대부분의 유형 이론은 공리를 가지고 있지 않다.이것은 유형 이론이 추론 규칙에 의해 정의되기 때문이다.(위의 "규칙" 참조).이것은 집합론에 익숙한 사람들에게 혼란의 원천이며, 여기서 이론은 논리(예: 1차 논리)에 대한 추론 규칙과 집합에 대한 공리 둘 다에 의해 정의된다.

때때로 유형 이론은 몇 가지 공리를 추가할 것이다.공리는 추론 규칙을 사용하여 도출되지 않고 받아들여지는 판단이다.규칙을 통해 새로 추가할 수 없는 속성을 보장하기 위해 종종 추가됩니다.

공리는 계산 방법 없이 용어를 도입하면 문제를 일으킬 수 있습니다.즉, 공리는 유형 ^[8]이론의 정규화 특성을 방해할 수 있습니다.

일반적으로 볼 수 있는 공리는 다음과 같습니다.

• "Axiom K"는 "신분증명의 고유성"을 보장합니다.즉, 아이덴티티 타입의 모든 용어는 반사성과 ^[9]동등합니다.
• "일치주의"는 활자의 동등성은 활자의 평등이라고 주장한다.이 성질에 대한 연구는 그 성질이 ^[10]공리 없이도 유지되는 입방체형 이론을 이끌었다.
• "제외된 중간 법칙"은 직관적인 논리 대신 고전적인 논리를 원하는 사용자를 만족시키기 위해 종종 추가된다.

대부분의 유형 이론에서는 추론 규칙에서 도출될 수 있기 때문에 선택 공리는 유형 이론에 추가될 필요가 없습니다.이것은 어떤 값이 존재한다는 것을 증명하기 위해서는 그 값을 계산하는 방법이 필요한 유형 이론의 건설적 특성 때문이다.선택 공리는 유형 이론에서 대부분의 집합 이론보다 덜 강력합니다. 왜냐하면 유형 이론의 함수는 계산 가능해야 하고, 구문 중심적이기 때문에, 유형 내 용어의 수는 셀 수 있어야 하기 때문입니다.(건설 수학은 선택 공리 ① 참조).

의사결정 문제

유형 이론은 자연스럽게 유형 ^[11]거주 결정 문제와 관련된다.

유형 거주

유형 거주 결정 문제(약칭 ${\displaystyle .}$ ${\displaystyle e}$ . ${\displaystyle \gamma }$e : ?$$\ $display$style \ $exists$e )$\Gamma \vdash$ e$:\tau$ $?\}$ )는 다음과 같습니다.

Given a type environment ${\displaystyle \Gamma }$ and a type ${\displaystyle \tau }$, decide whether there exists a term ${\displaystyle e}$ that can be assigned the type ${\displaystyle \tau }$ in the type environment ${\displaystyle \Gamma }$.

지라드의 역설은 유형 거주가 카레-하워드 대응과 유형 시스템의 일관성과 강하게 관련되어 있음을 보여준다.건전하기 위해서는 이러한 시스템은 무인도형이어야 한다.

용어 및 유형의 반대는 구현 및 사양의 하나로 볼 수도 있습니다.프로그램 합성(의 연산 대응물)에 의해, 타입 ^[12]정보의 형태로 주어진 사양으로부터(아래를 참조) 프로그램을 구축하기 위해서(또는 일부) 사용할 수 있다.

유형 추론

유형 이론(예를 들어 인터랙티브 정리 프로버)으로 작동하는 많은 프로그램도 유형 회의를 수행합니다.이를 통해 사용자가 원하는 규칙을 더 적은 수의 작업으로 선택할 수 있습니다.

연구 분야

호모토피 유형 이론은 대부분 등식 유형을 다루는 점에서 직관적인 유형 이론과 다르다.2016년에는 정규화를 ^[13][10]수반하는 호모토피형 이론인 입방체형 이론이 제안되었다.

해석

유형 이론은 수학의 다른 분야와 관련이 있다.유형 이론의 지지자들은 종종 이러한 연관성을 그 사용의 정당화라고 언급한다.

유형은 명제이고 용어는 증거이다.

근거로 사용할 때, 특정 유형은 제안(증명할 수 있는 진술)으로 해석되며, 유형의 용어는 해당 제안의 증거이다.따라서 "δ x:nat . x+1=1+x" 유형은 "nat" 유형의 "x"에 대해 "x+1"과 "1+x"가 동일함을 나타냅니다.그리고 그런 종류의 용어가 그 증거를 나타냅니다.

Curry-Howard 대응

Curry-Howard 대응은 로직과 프로그래밍 언어 간에 관찰된 유사성입니다.논리학에서 "A $→$ ${\displaystyle$ \to$$$$} B"는 유형 "A"에서 유형 "B"까지의 함수와 유사합니다.다양한 로직에서 규칙은 프로그래밍 언어 유형의 식과 유사합니다.규칙의 적용은 프로그래밍 언어의 프로그램과 유사하기 때문에 유사성은 더욱 커집니다.따라서 대응은 종종 "프로그램으로서의 증명"으로 요약된다.

논리 연산자 "for all"과 "exists"는 Per Martin-Löf가 의존형 이론을 발명하도록 이끌었다.

일부 유형이 명제로 해석될 때, 유형을 로직으로 만들기 위해 이들을 연결하기 위해 사용할 수 있는 일련의 공통 유형이 있습니다.그러나 그 논리는 고전적인 논리가 아니라 직관적인 논리이다.즉, 배제된 중간 부정의 법칙이나 이중 부정의 법칙이 없다.

논리적 명제와 유형에는 자연스러운 관계가 있습니다."A"가 명제를 나타내는 유형인 경우, $→$ \$displaystyle \top$ \to$$$$} A"의 함수를 생성할 수 있다는 것은 A가 증거를 가지고 있음을 의미하며, "A $\to {\displaystyle }$ ${\$ \$displaystyle \to$\bot $"$ 함수를 생성할 수 있다는 것은 A가 증거를 가지고 있지 않음을 의미한다.즉, 거주할 수 있는 유형은 증명되고, 거주할 수 없는 유형은 증명되지 않습니다.

경고: 이 해석은 많은 혼란을 초래할 수 있습니다. 유형 이론은 부울 로직과 같은 "bool" 유형의 "true" 및 "false" 용어를 가질 수 있으며, 동시에 "true"(제공 가능) 및 "false"(확실하지 않음)를 나타내는 유형$${\(\$displaystyle$\$top$)$$및$$${\(\displaystyle$\bot$)$을 가질 수 있다.

.

( )		표기법	입력
	$}{\displaystyle\top}$	$}{\displaystyle\top}$	타입 " " "
	$\displaystyle \bot }$	$\displaystyle \bot }$	타입 빈
.	$A(\displaystyle\neg A)$	$\bot) (\displaystyle A\to\bot)$	는 빈
★★★	${\displaystyle A\to B}$	${\displaystyle A\to B}$	★★
★★★★★★★★★★★★★★★★★.	$A B\displaystyle A\land B)$	$A B}(\displaystyle A\times B)$	타입 ★★★★★
	${\displaystyle A\lor B}$	${\displaystyle A+B}$	Type ( 타입)
★★★★★★	$adisplaystyle\forall a,P(a))$	a : ( a ) a a : A . P ( a )	함수 ★★★★★
	$adisplaystyle \exists a,P(a)}$	a : ( a ) a a : A . P ( a )	제품 ★★★★★★

그러나 이 해석에 따르면, 제외 중간 법칙은 없다.즉, 타입 A. A + (A $→$ \$display \to \bot$)라는 용어는 없습니다.

마찬가지로 이중 부정은 없다.유형 π A . ( A $→$ \ $displaystyle$\$to$\ $bot$) $\to {\displaystyle }$ ${\displaystyle \mathrm{\to }}$\ $displaystyle$\$to$ \ $bot$ ）$$$→$ \ $displaystyle$\$to }$ A$$. (주의:직관적인 논리에 따라$(\$$displaystyle$$\lnot$ A$\lnot$ A\lnot A\$to\lnot$ A$)$가 허용되며, 유형에는 (((((A $\to {\displaystyle }$\$displaystyle$$\to$$\bot$$$}) $\to {\displaystyle }$$$$display$ style \$to \display$$→)$가 있습니다.

그러므로 유형논리는 직관적인 논리이다.유형 이론은 종종 브루어(Brower)의 구현으로 인용된다.Heyting-Kolmogorov 해석

규칙이나 가정에 의해 배제된 중간 부정과 이중 부정의 법칙을 유형 이론에 포함시킬 수 있다.그러나 항은 표준 항으로 계산되지 않을 수 있으며 두 항이 서로 판단적으로 동일한지 여부를 결정하는 능력에 방해가 됩니다.

마틴-뢰프는 그의 직관적인 유형 이론을 건설적인 수학의 기초로서 제안했다.계산에서는 속성$$P(x {$displaystyle$ x$})$를 가진 x$({displaystyle$ x$})$가 존재함을 증명할 때 $특정{\displaystyle }$x({$displaystyle$ x$})$와 속성 P를 가지고 있다는 증거가 있어야 합니다.유형 이론에서, 존재는 종속 제품 유형을 사용하여 달성되며, 그 증거는 그러한 유형의 용어를 요구한다.$용어{\displaystyle }$t\$displaystyle$t의 경우, "$first{\displaystyle }$ $t\displaystyle$t$"$는 x\$displaystyle$x를$$ 생성하고, "$second{\displaystyle }$t\$displaystyle$ t$"$는 P$(x\displaystyle$ x$)$의 증명을 생성합니다.

비건설적 증거의 예로는 "반대에 의한 증명"이 있다.첫 번째 단계는$x$가 $존재$하지 않는다고 가정하고 모순으로 반박하는 것입니다.이 단계의 결론은 "x$\displaystyle$x가$$ $존재$하지 않는 경우가 아니다"입니다.마지막 단계는 이중 부정을 통해 x$${\$displaystyle$ x$}$가 $존재$한다고 결론짓는 것입니다.확실히 하자면, 건설적인 수학은 여전히 "반대에 의한 반박"을 허용한다."x$\displaystyle$ x$"$가 $존재$하지 않는 경우"를 증명할 수 있습니다.그러나 건설적인 수학에서는 이중 부정을 제거하는 마지막 단계가 x$${\$displaystyle$ x$}$^[14]가 존재한다고 결론짓는 것을 허용하지 않습니다.

건설 수학은 브루어(Brower)에 의해 증명된 것처럼 종종 인텐션 논리를 사용해 왔다.Heyting-Kolmogorov 해석

기초로서 제안된 유형 이론의 대부분은 건설적이다.여기에는 교정 보조원이 사용하는 대부분의 기능이 포함됩니다.

규칙 또는 가정에 따라 유형 이론에 비건설적 특징을 추가할 수 있습니다.여기에는 현재 계속 통화와 같은 계속 통화 중인 작업자가 포함됩니다.그러나 이러한 측정 시스템은 카노닉성 및 모수성과 같은 바람직한 속성을 손상시키는 경향이 있습니다.

범주론에 대한 초기 동기는 근본주의와는 거리가 멀었지만, 두 분야는 깊은 연관성을 가지고 있는 것으로 드러났다.존 레인 벨이 쓰듯이: "사실 범주 자체는 특정한 종류의 유형 이론으로 볼 수 있다; 이 사실만으로도 유형 이론이 설정 이론보다 범주 이론과 훨씬 더 밀접하게 관련되어 있다는 것을 보여준다."간단히 말해서, 범주는 그 대상을 유형(또는 종류)으로 간주함으로써 유형 이론으로 볼 수 있다. 즉, "대략적으로 말하면, 범주는 그 구문을 빼앗긴 유형 이론으로 생각할 수 있다."다음과 같은 ^[15]중요한 결과를 얻을 수 있습니다.

• 데카르트 닫힌 범주는 유형 δ-calculus에 해당한다(Lambek, 1970).
• C-모노이드(제품과 지수를 가진 범주 및 하나의 비말단 개체)는 유형화되지 않은 γ-calculus(1980년경 Lambek와 Dana Scott에 의해 독립적으로 관찰됨)에 해당한다.
• 국소적으로 닫힌 범주는 마틴-뢰프 유형 이론에 해당한다(Seely, 1984).

범주형 논리로 알려진 상호작용은 그 이후로 활발한 연구의 주제가 되어왔다. 예를 들어 제이콥스(1999)의 논문을 참조하라.

호모토피 유형 이론은 유형 이론과 범주 이론을 결합하려고 시도합니다.그것은 평등, 특히 유형 간의 평등에 초점을 맞춘다.

이론

• 고차 논리인 단순형 람다 미적분
• 유형
• F 스 F
• LF는 종종 다른 유형 이론을 정의하기 위해 사용됩니다.
• 구성 및 그 도함수의 미적분

★★★★

• ST ★★★
• UTT(Luo's Unified Types)
• 조합 논리의 어떤 형태
• 람다 입방체(순수형 시스템이라고도 함)에 정의된 기타 항목
• 람다 미적분이라는 이름의 다른 것

인 연구

• 호모토피 타입이론은 타입의 평등을 탐구한다.
• 입방체형 이론은 호모토피형 이론을 구현한 것입니다.

프로그램

이 섹션은 확장해야 합니다.추가함으로써 도움이 될 수 있습니다. (2008년 5월)

오토매스라고 불리는 최초의 컴퓨터 증명 보조자는 컴퓨터로 수학을 인코딩하기 위해 활자 이론을 사용했다.마틴-뢰프는 모든 수학이 수학의 새로운 기초가 될 수 있도록 부호화하는 직관적 유형 이론을 특별히 개발했습니다.호모토피 유형 이론을 이용한 수학적 기초에 대한 연구가 진행 중이다.

범주 이론에서 일하는 수학자들은 이미 널리 받아들여진 체르멜로-프랭켈 집합 이론의 기초와 함께 일하는 데 어려움을 겪었습니다.이것은 Lawvere의 집합 범주 기본 이론(^[16]ETCS)과 같은 제안으로 이어졌다.호모토피 타입이론은 타입이론을 사용하여 이 행에서 계속된다.연구자들은 종속형(특히 동일형)과 대수적 위상(특히 호모토피) 사이의 연관성을 탐색하고 있다.

유형 이론에 대한 현재 연구의 대부분은 증명 검사기, 대화형 증명 보조기, 자동화된 정리 검증기에 의해 추진된다.이러한 시스템의 대부분은 형식 이론과 프로그래밍 언어 사이의 밀접한 연관성을 고려할 때, 형식 이론을 증명 부호화의 수학적 기반으로 사용합니다.

• LF는 Twelf에 의해 사용되며, 종종 다른 유형 이론을 정의하기 위해 사용됩니다.
• 고차 논리에 해당하는 많은 유형 이론은 프로버 및 PVS의 HOL 패밀리에 의해 사용된다.
• 계산형 이론은 NuPRL에 의해 사용된다.
• 구성 및 그 도함수의 미적분은 Coq, Matita 및 Lean에 의해 사용된다.
• UTT(Luo's Unified Theory of Dependent Types)는 프로그래밍 언어이자 증명 보조인 Agda에 의해 사용됩니다.

많은 유형 이론들이 레고와 이자벨에 의해 뒷받침된다.Isabelle은 ZFC와 같은 유형 이론 외에도 기초를 지지합니다.미자르는 집합론만을 지원하는 증명 시스템의 한 예다.

컴파일러의 의미 분석 국면의 유형 확인 알고리즘과 같은 정적 프로그램 분석은 유형 이론과 관련이 있습니다.대표적인 것이 아그다(Agda)로, 아그다(UTT)는 UTT(Luo's Unified Theory of Dependent Types)를 사용하는 프로그래밍 언어이다.

프로그래밍 언어 ML은 유형 이론을 조작하기 위해 개발되었으며(LCF 참조), 자체 유형 시스템은 유형 이론의 영향을 많이 받았습니다.

유형 이론은 또한 자연 ^[17][18]언어의 의미론, 특히^[19] 몬태규 문법과 그 후손들의 공식 이론에서 널리 사용된다.특히, 범주형 문법 및 프리그룹 문법은 단어의 유형(명사, 동사 등)을 정의하기 위해 유형 생성자를 광범위하게 사용합니다.

가장 일반적인 구조에서는 개인 및 참값에 대해 각각 기본 $유형{\displaystyle }$ e$\displaystyle$e와$$ $\displaystyle$t를 사용하며$$ 다음과 같이 유형 집합을 재귀적으로 정의합니다.

• $\$$displaystyle$$a$와 b$\displaystyle$b가$$ 유형인 $경우{\displaystyle }$${\displaystyle }$\$displaystyle a, b\rangle$도 ${\displaystyle \mathrm{유형}}$입니다$.$
• 기본 유형 및 이전 절에 의해 그것들로부터 구성될 수 있는 것 외에는 아무것도 유형이다.

complex type${\displaystyle a,}$ ${\displaydisplay$ （ \ $displaystyle$ \$langle$a$$,$b$$$\ $rangle$$）$는$$a $타입$의 엔티티에서$$b $타입$의 엔티티까지의 함수 유형입니다.따라서 엔티티에서 참값까지의 함수 집합의 요소, 즉 엔티티 집합의 지시기 함수로 해석되는 $⟨{\displaystyle e}$, t ${\$ \$displaystyle$ \ $langle e,$ t\$rangle$등의 유형이$$ 있습니다.유형${\displaystyle }$⟨${\displaystyle 、}$ ${\displaystyle e、}$ t 、 ${\displaystyle t}$ ${\$ ${\displaystyle （}$ \ $displaystyle \langle \langle$e ,$t$ \$rangle$ , t \$rangle$} ）의 식은 엔티티 집합에서 참값 집합까지의 함수, 즉 (a의 표시기 함수) 집합입니다.이 후자의 유형은 일반적으로 모두 또는 노바디처럼 자연어 수량화 유형으로 간주된다(Montague 1973, Barwise 및 Cooper 1981).^{[full citation needed]}

사회과학

그레고리 베이슨은 사회과학에 논리유형 이론을 도입했다; 이중 구속과 논리수준에 대한 그의 개념은 러셀의 유형 이론에 기초한다.

「 」를 참조해 주세요.

• 수학의 기초

추가 정보

메모들

레퍼런스

외부 링크

입문 자료

• 다양한 주제에 대한 기사가 있는 nLab의 유형 이론.
• 스탠퍼드 철학 백과사전의 직관적 유형 이론 논문
• Henk Barendregt의 Lambda 미적분 책
• Per Martin-Löf의 직관적 유형 이론 노트
• Martin-Löf의 유형 이론 책에서의 프로그래밍
• 수학적 기초로서 호모토피 타입 이론을 제안한 호모토피 타입 이론서.

고급 재료

• Robert L. Constable (ed.). "Computational type theory". Scholarpedia.
• TYPES 포럼 - 1987년부터 운영되고 있는 컴퓨터 사이언스 유형 이론에 초점을 맞춘 모델레이트 이메일 포럼.
• Nuprl Book: "타입 이론의 입문"
• 2005~2008년 여름학교 유형 프로젝트 강의 노트
  • 2005년 여름 학교에는 입문 강의가 있다.
• 오리건 주 프로그래밍 언어 여름 학교, 많은 강의와 약간의 노트.
  • Robert Harper의 YouTube 강연 등 2013년 여름 강연
  • 2015년 여름 유형, 논리, 의미론 및 검증
• Andrej Bauer 블로그