유형 이론

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요

유형 이론은 수학적 논리의 한 분야로, 1900년대 초 러셀의 역설을 해결하기 위해 제시되었다. 앨론조 처치의 람다 대수를 통해 발전되었으며, 현대에는 마틴-뢰프의 직관주의적 유형 이론과 코캉의 구성 계산법 등이 구성주의 수학의 기초로 연구되고 있다. 유형 이론은 프로그래밍 언어, 자연 언어의 형식 의미론, 사회 과학 등 다양한 분야에 응용되며, 증명 보조자 및 자동 정리 증명기 개발에도 활용된다. 유형 이론은 논리적 틀이 직관주의 논리와 유사하며, 커리-하워드 대응을 통해 논리와 프로그래밍 언어 간의 연결을 보여준다.

더 읽어볼만한 페이지

유형 이론 - 형 변환
형 변환은 프로그래밍에서 변수의 데이터 타입을 변경하는 것으로, 암시적 형 변환과 명시적 형 변환으로 나뉘며, 객체 지향 프로그래밍에서는 업캐스팅과 다운캐스팅이 발생하고, 각 언어는 고유한 규칙과 방법을 제공하며 잘못된 형 변환은 오류를 유발할 수 있다.
유형 이론 - 대수적 자료형
대수적 자료형은 합 타입과 곱 타입을 조합하여 새로운 자료형을 정의하는 방법으로, 단일 연결 리스트나 이진 트리와 같은 자료 구조를 표현하고 패턴 매칭을 통해 자료형의 구조를 분해 및 처리하는 데 유용하며, 함수형 프로그래밍 언어에서 널리 사용된다.
수리논리학 - NAND 게이트
NAND 게이트는 모든 입력이 1일 때 0을 출력하고 그 외에는 1을 출력하는 논리 게이트로서, 다양한 기호로 표현되며, AND 연산의 결과를 부정하는 연산을 수행하고, 여러 방식으로 구현될 수 있으며, 기능적으로 완전하여 디지털 회로 설계에 필수적이다.
수리논리학 - 셈
셈은 대상의 개수를 파악하는 기본적인 행위로, 수학에서는 집합의 원소 개수를 파악하는 과정으로 정의되며, 셈의 방식에 따라 결과가 달라질 수 있고, 셈을 배우는 과정은 아동의 교육 및 발달에 중요한 역할을 한다.

유형 이론

2. 역사

버트런드 러셀은 러셀의 역설을 해결하기 위해 1902년부터 1908년까지 다양한 유형 이론을 제시했다.^[3] 1908년, 러셀은 분지된 유형 이론과 환원 공리를 제시했으며, 이는 화이트헤드와 함께 저술한 ''수학 원리''(1910년, 1912년, 1913년)에 나타났다. 이 시스템은 각 수학적 실체를 특정 유형에 할당하고, 유형의 계층 구조를 만들어 러셀의 역설에서 제기된 모순을 피했다. 주어진 유형의 실체는 해당 유형의 서브타입으로만 구성되므로,^[1]^[2] 실체가 자기 자신을 사용하여 정의되는 것을 방지한다.

앨론조 처치는 람다 대수와 함께 유형 이론을 발전시켰다. 처치의 단순 유형 람다 대수는 유형 이론의 초기 예시 중 하나이다. 처치의 유형 이론^[4]은 형식 시스템이 원래의 유형이 없는 람다 대수를 괴롭힌 클레니-로저 역설을 피하게 했다. 처치는 이것이 수학의 기초 역할을 할 수 있음을 보여주었고,^[4]^[5] 이것을 고차 논리라고 불렀다.

현대에는 페르 마틴-뢰프의 직관주의적 유형 이론과 티에리 코캉의 구성 계산법 등이 구성주의 수학의 기초로 제안되고 연구되고 있다. 호모토피 유형 이론은 유형 이론의 활발한 연구 분야 중 하나이다.

3. 응용

형 이론은 프로그래밍 언어의 컴파일러에서 의미론적 분석 부분의 타입 체크 알고리즘 구축에 사용된다.^[7] Agda는 UTT(Luo의 종속 타입 통합 이론)를 타입 시스템으로 사용하는 프로그래밍 언어의 예시이다. ML은 타입 이론 조작을 위해 개발되었으며, 자체 타입 시스템은 타입 이론의 영향을 크게 받았다.

형 이론은 자연 언어의 형식 의미론 이론, 특히 몬테규 문법과 그 후계자에서 널리 사용된다.^[7]^[8]^[9] 몬터규 문법의 내포 논리에서는 $e$ (사물)와 $t$ (진리값)를 기본적인 형으로 사용하며, 다음 규칙으로 형의 집합을 정의한다.

# $a$ 와 $b$ 가 형일 때, $\langle a,b\rangle$ 도 형이다.

# $a$ 가 형일 때, $\langle s,a\rangle$ 도 형이다. ( $s$ 는 지표)

$\langle a,b\rangle$ 는 $a$ 의 요소에서 $b$ 의 요소로의 함수형이다. $\langle e,t\rangle$ 는 '사물'에서 진리값으로의 함수이며, 집합의 지시 함수이다. $\langle\langle e,t\rangle,t\rangle$ 는 집합의 집합이다. 범주 문법과 전군 문법은 단어의 유형을 정의하기 위해 유형 생성자를 사용한다. 레코드 유형 이론은 레코드를 사용하여 형식 의미론을 표현한다.^[11]^[12]

그레고리 베이트슨은 사회 과학에 논리형식 이론을 도입했으며, 그의 이중 구속 개념은 러셀의 형식 이론에 기초한다.^[13]

3. 1. 수학적 기초

최초의 컴퓨터 증명 보조 도구인 오토매스(Automath)는 컴퓨터에서 수학을 인코딩하기 위해 유형 이론을 사용했다. 마틴-뢰프는 모든 수학을 인코딩하기 위해 직관적 유형 이론을 개발했다. 호모토피 유형 이론을 사용한 수학적 기초 연구가 진행 중이다.

범주론 연구자들은 체르멜로-프렝켈 집합론의 대안으로 유형 이론을 사용하기도 한다.^[6]

3. 2. 증명 보조자

LF는 Twelf에서 다른 유형 이론을 정의하기 위해 사용된다.^[1] HOL 계열 증명기 및 PVS는 고차 논리에 속하는 유형 이론을 사용한다.^[1] NuPRL은 계산적 유형 이론을 사용한다.^[1] Coq, Matita, Lean은 구성의 미적분과 그 파생물을 사용한다.^[1] Agda는 UTT(Luo의 종속 유형 통합 이론)를 사용한다.^[1] LEGO 및 Isabelle은 다양한 유형 이론을 지원한다.^[1] Mizar는 집합론만 지원하는 증명 시스템이다.^[1]

3. 3. 프로그래밍 언어

정적 프로그램 분석은 컴파일러의 의미 분석 단계에 있는 타입 검사 알고리즘과 관련이 있다.^[7] 대표적인 예로, 타입 시스템으로 UTT(Luo의 종속 타입 통합 이론)를 사용하는 프로그래밍 언어인 Agda가 있다.

ML은 타입 이론 조작을 위해 개발되었으며(LCF 참조), 자체 타입 시스템은 타입 이론의 영향을 크게 받았다.

3. 4. 언어학

유형 이론은 자연 언어의 형식 의미론 이론, 특히 몬테규 문법과 그 후계자에서 널리 사용된다.^[7]^[8]^[9] 범주 문법과 전군 문법은 단어의 유형('명사', '동사' 등)을 정의하기 위해 유형 생성자를 사용한다.

가장 일반적인 구성은 개별자에 대해 기본 유형

e

와 진리값에 대해

t

를 사용하며, 다음과 같이 재귀적으로 유형 집합을 정의한다.

$a$ 와 $b$ 가 유형이면, $\langle a,b\rangle$ 도 유형이다.
기본 유형과 이전 절에 의해 구성될 수 있는 것을 제외하고는 아무것도 유형이 아니다.

복합 유형

\langle a,b\rangle

는 유형

a

의 엔터티에서 유형

b

의 엔터티로의 함수 유형이다.

\langle e,t\rangle

와 같은 유형은 엔터티 집합에서 진리값으로의 함수 집합의 원소로 해석된다. 즉, 엔터티 집합의 지시 함수이다.

\langle\langle e,t\rangle,t\rangle

유형의 표현식은 엔터티 집합에서 진리값으로의 함수, 즉 (집합의 지시 함수) 집합이다. 이 마지막 유형은 일반적으로 "모두" 또는 "아무도"와 같은 자연 언어 양화사의 유형으로 간주된다.^[10]

레코드 유형 이론은 레코드를 사용하여 형식 의미론을 표현하는 프레임워크이다.^[11]^[12]

3. 5. 사회 과학

그레고리 베이트슨은 사회 과학에 논리형식 이론을 도입했으며, 그의 이중 구속과 논리 수준에 대한 개념은 러셀의 형식 이론에 기초한다.^[13]

4. 유형 이론과 논리

버트런드 러셀은 소박한 집합론의 고틀로프 프레게 판이 러셀의 역설로 인해 문제가 있다는 것을 발견하고, 1902년부터 1908년 사이에 다양한 유형 이론을 제시했다.^[14] 유형 이론은 수학적 논리의 일종으로, 추론 규칙을 통해 판단을 유도한다.

Mendelson (1997, 289-293)의 체계 '''ST'''는 양화의 논의 영역을 유형의 계층으로 나누고, 개체 요소(individuals)에는 유형을 할당한다. 기반이 되는 논리는 일계 술어 논리이며, 양화 변수의 범위는 유형에 의해 한정된다. '''ST'''는 『수학 원리』의 유형 이론에 비해 단순하며, 임의 관계의 논의 영역은 모두 같은 유형이어야 한다.^[14]

계층 중 가장 낮은 유형에서는 개체 요소에 멤버가 없고, 그것들은 두 번째로 낮은 유형의 멤버가 된다. 각 유형에는 더 상위 유형이 있으며, 페아노 공리의 후자 함수 (successor function)의 표기법과 비슷하다. '''ST'''에서는 최고위 유형이 있는지 여부는 규정하지 않는다. 각 유형에 자연수를 할당하는 것이 용이하며, 최하층의 유형에 0을 할당한다. 단, 유형 이론 자체는 자연수의 정의를 전제로 하지 않는다.^[14]

'''ST'''에 고유한 기호로서 프라임이 붙은 변수와 접중사 ∈가 있다. 논리식에서 프라임이 없는 변수는 모두 같은 유형에 속하고, 프라임이 붙은 변수 (''x′'')는 그보다 한 단계 위의 유형에 속한다. '''ST'''의 원자 논리식은 (항등식) 또는 형식이다. 접중사 기호 ∈는 집합의 소속 관계를 나타낸다.^[14]

'''ST'''에서의 일계 술어 논리에서는 유형을 넘나드는 양화가 불가능하다. 따라서 외연성과 내포성의 공리를 유형을 넘어서 성립하는 공리 도식 (axiom schema)으로 정의한다.^[14]

동일성:
외연성:
자유 변항 ''x''를 포함하는 임의의 일계 술어 논리식이다.
내포성:
같은 유형의 요소를 모은 것은 다음 레벨의 유형의 오브젝트를 형성한다. ''내포성''은 유형에 관한 공리일 뿐만 아니라 의 공리이기도 하다.
무한성: 최하층의 유형의 개체 요소 간에 대한 비어 있지 않은 이항 관계 이 존재한다. (자세한 조건은 원문 참조)
''무한성''은 순수한 수학적인 '''ST''' 고유의 공리이다. ''R''이 전순서 관계임을 의미하며, ''R''의 논의 영역이 무한일 때만 성립한다. 결과적으로 무한 집합의 존재를 전제로 한다.

'''ST'''는 유형 이론이 공리적 집합론과 유사하다는 것을 보여준다. 유형 이론의 출발점은 집합론이지만, 그 공리, 존재론, 용어는 다르다.^[14]

4. 1. 용어

논리 용어는 귀납적 정의에 따라 논리 상수, 변수, 또는 다른 용어에 적용되는 함수 적용으로 재귀적으로 정의된다. 상수 기호에는 자연수

0

, 부울 값

\mathrm{true}

와 후속 함수

\mathrm{S}

및 조건 연산자

\mathrm{if}

와 같은 함수가 포함될 수 있다. 따라서 일부 용어는

0

,

(\mathrm{S}\,0)

,

(\mathrm{S}\,(\mathrm{S}\,0))

및

(\mathrm{if}\,\mathrm{true}\,0\,(\mathrm{S}\,0))

일 수 있다.^[14]

4. 2. 판단

대부분의 유형 이론은 4가지 판단을 갖는다. 판단은 가정으로부터 유도될 수 있다. 턴스타일 기호

\vdash

를 사용하여 판단을 형식적으로 작성한다.

판단에 대한 공식 표기	설명
$\Gamma \vdash T$ 타입	$T$ 는 (가정 $\Gamma$ 아래) 타입이다.
$\Gamma \vdash t : T$	$t$ 는 (가정 $\Gamma$ 아래) 타입 $T$ 의 항이다.
$\Gamma \vdash T_1 = T_2$	타입 $T_1$ 은 (가정 $\Gamma$ 아래) 타입 $T_2$ 와 같다.
$\Gamma \vdash t_1 = t_2 : T$	항 $t_1$ 과 $t_2$ 는 모두 타입 $T$ 이며 같다 (가정 $\Gamma$ 아래).

예를 들어, "만약 $x$ 가 타입 $\mathsf{bool}$ 의 항이고 $y$ 가 타입 $\mathsf{nat}$ 의 항이라면, $(\mathrm{if}\,x\,y\,y)$ 는 타입 $\mathsf{nat}$ 의 항이다"라고 말할 수 있다. 이러한 판단은 턴스타일 기호를 사용하여 형식적으로 다음과 같이 작성한다.

: $x:\mathsf{bool},y:\mathsf{nat}\vdash(\textrm{if}\,x\,y\,y): \mathsf{nat}$

만약 가정이 없다면, 턴스타일의 왼쪽에는 아무것도 없을 것이다.

: $\vdash \mathrm{S}:\mathsf{nat}\to\mathsf{nat}$

왼쪽에 있는 가정의 목록은 판단의 '컨텍스트'이다. $\Gamma$ 와 $\Delta$ 와 같은 대문자 그리스 문자는 가정의 일부 또는 전체를 나타내기 위해 흔히 사용된다.

4. 3. 추론 규칙

대부분의 유형 이론은 다음과 같은 4가지 판단을 가진다.

판단에 대한 공식 표기	설명
$\Gamma \vdash T$ 타입	$T$ 는 (가정 $\Gamma$ 아래) 타입이다.
$\Gamma \vdash t : T$	$t$ 는 (가정 $\Gamma$ 아래) 타입 $T$ 의 항이다.
$\Gamma \vdash T_1 = T_2$	타입 $T_1$ 은 (가정 $\Gamma$ 아래) 타입 $T_2$ 와 같다.
$\Gamma \vdash t_1 = t_2 : T$	항 $t_1$ 과 $t_2$ 는 모두 타입 $T$ 이며 같다 (가정 $\Gamma$ 아래).

유형 이론의 추론 규칙은 다른 판단의 존재를 기반으로 어떤 판단을 내릴 수 있는지 알려준다. 규칙은 수평선을 사용하여 겐첸 스타일의 연역으로 표현되며, 선 위에는 필요한 입력 판단이 있고 선 아래에는 결과 판단이 있다.^[15] 예를 들어, 다음 추론 규칙은 판단적 동일성에 대한 대체 규칙을 명시한다.

: $\begin{array}{c}\Gamma\vdash t:T_1 \qquad \Delta\vdash T_1 = T_2 \\\hline\Gamma,\Delta\vdash t:T_2\end{array}$

규칙은 구문적이며 재작성을 통해 작동한다. 메타변수 $\Gamma$ , $\Delta$ , $t$ , $T_1$ , 그리고 $T_2$ 는 단일 기호뿐만 아니라 많은 함수 적용을 포함하는 복잡한 항과 유형으로 구성될 수 있다.

입력이 필요하지 않은 규칙의 한 예는 상수 항의 유형을 명시하는 규칙이다. 예를 들어, $\mathsf{nat}$ 유형의 항 $0$ 이 있다고 주장하려면 다음과 같이 작성한다.

: $\begin{array}{c}\hline\vdash 0 : nat \\\end{array}$

일반적으로, 타입 이론에서 증명의 원하는 결론은 타입 거주 가능성 중 하나이다.^[16] 타입 거주 가능성 결정 문제(약어: $\exists t.\Gamma \vdash t : \tau?$ )는 다음과 같다.

: 문맥 $\Gamma$ 와 타입 $\tau$ 가 주어졌을 때, 타입 환경 $\Gamma$ 에서 타입 $\tau$ 를 할당받을 수 있는 항 $t$ 가 존재하는지 여부를 결정한다.

지라르의 역설은 타입 거주 가능성이 커리-하워드 대응을 갖는 타입 시스템의 일관성과 밀접하게 관련되어 있음을 보여준다. 사운드하기 위해서는, 그러한 시스템은 비거주 타입이 있어야 한다.

타입 이론은 일반적으로 다음과 같은 규칙들을 포함한다.

판단을 생성 (이 경우 ''문맥''이라고 함)
문맥에 가정을 추가 (문맥 ''약화'')
가정을 재배열
변수를 생성하기 위해 가정을 사용
판단적 등식에 대한 반사성, 대칭성 및 추이성 정의
람다 항 적용에 대한 대입 정의
대입과 같은 등식의 모든 상호 작용 나열
타입 유니버스의 계층 정의
새로운 타입의 존재를 주장

또한, 각 "규칙별" 타입에 대해 4가지 종류의 규칙이 있다.

"타입 형성" 규칙은 타입을 생성하는 방법을 설명한다.
"항 도입" 규칙은 "쌍"과 "S"와 같은 정식 항 및 생성자 함수를 정의한다.
"항 제거" 규칙은 "첫 번째", "두 번째" 및 "R"과 같은 다른 함수를 정의한다.
"계산" 규칙은 타입별 함수로 계산이 수행되는 방식을 지정한다.

5. 유형 이론과 기초론

1902년부터 1908년 사이 버트런드 러셀은 소박한 집합론의 고틀로프 프레게 판이 러셀의 역설로 어려움을 겪고 있다는 것을 발견하고, 다양한 유형 이론을 제시했다.^[1]

유형 이론은 직관주의 논리 또는 구성적 논리와 유사성을 가지며, 범주론 및 컴퓨터 프로그래밍과도 연결될 수 있다.

여기에서는 멘델슨(Mendelson, 1997, 289-293)의 체계 '''ST'''를 설명한다. '''ST'''는 『수학 원리』의 유형 이론에 비해 단순하며, 양화의 논의 영역은 유형의 계층으로 나뉜다. 개체 요소(individuals)에는 유형이 할당되며, 양화 변수의 범위는 유형에 의해 한정된다. 임의 관계의 논의 영역은 모두 같은 유형이어야 한다.

가장 낮은 유형에는 개체 요소가 없고, 그것들은 두 번째로 낮은 유형의 구성원이 된다. 최하층 유형의 개체 요소는 집합론의 원소에 대응한다. 각 유형에는 더 상위 유형이 있으며, 페아노 공리의 후자 함수(successor function) 표기법과 비슷하다. '''ST'''에서는 최고위 유형이 있는지 여부는 규정하지 않으며, 초한수 개의 유형이 있어도 문제가 되지 않는다. 각 유형에 자연수를 할당하는 것이 용이하며, 최하층 유형에 0을 할당한다. 단, 유형 이론 자체는 자연수의 정의를 전제로 하지 않는다.

'''ST'''에 고유한 기호로서 프라임이 붙은 변수와 접중사 ∈가 있다. 논리식에서 프라임이 없는 변수는 모두 같은 유형에 속하고, 프라임이 붙은 변수(''x′'')는 그보다 한 단계 위의 유형에 속한다. '''ST'''의 원자 논리식은 (항등식) 또는 라는 형식이다. 접중사 기호 ∈는 집합의 소속 관계를 나타낸다.

'''ST'''에서의 일계 술어 논리에서는 유형을 넘나드는 양화가 불가능하므로, 어떤 유형과 그에 인접한 유형마다 외연성과 내포성의 공리를 정의해야 한다. 하지만 아래의 외연성과 내포성의 공리를 유형을 넘어서 성립하는 공리 도식(axiom schema)으로 하면 된다.

동일성:
외연성:
여기서 자유 변항 ''x''를 포함하는 임의의 일계 술어 논리식을 로 나타낸다.
내포성:
주의: 같은 유형의 요소를 모은 것은 다음 레벨의 유형의 오브젝트를 형성한다. ''내포성''은 유형에 관한 공리일 뿐만 아니라 의 공리이기도 하다.
무한성: 최하층 유형의 개체 요소 간에 대한 비어 있지 않은 이항 관계 로 이하를 만족하는 것이 존재.
협의의 전순서(비반사적이고 추이적이며, 강결합)이며, 극소 원소 이외의 임의의 요소는 그것보다 큰 요소를 가짐(여정의역은 정의역의 부분 영역임).
주의: ''무한성''은 순수한 수학적인 '''ST''' 고유의 공리이다. 이것은 ''R''이 전순서 관계임을 의미한다. 최하층 유형에 0을 할당했을 때, ''R''의 유형은 3이 된다. ''무한성''이 성립하는 것은 ''R''의 논의 영역이 무한일 때뿐이며, 결과적으로 무한 집합의 존재를 전제로 하고 있다. 관계를 순서쌍으로 정의하는 경우, 이 공리 전에 순서쌍을 정의할 필요가 생긴다. 이것은 '''ST'''에 쿠라토프스키(Kuratowski)의 정의를 도입함으로써 실현된다. ZFC와 같은 다른 집합론의 무한 집합의 공리가 왜 '''ST'''에서 채택되지 않았는지는 책에도 쓰여 있지 않다.

'''ST'''는 유형 이론이 공리적 집합론과 유사하다는 것을 보여주었다. 더욱이 ZFC 등의 기존의 집합론보다 단순한 존재론에 기초한 "iterative conception of set"이라고 불리는 '''ST'''의 보다 정교한 존재론이 더 간단한 공리(공리 도식)를 구성하고 있다. 유형 이론의 출발점은 집합론이지만, 그 공리, 존재론, 용어는 다르다. 유형 이론에는 이 외에도 New Foundations와 Scott-Potter set theory가 있다.

5. 1. 직관주의 논리

유형 이론의 논리적 틀은 직관주의 논리 또는 구성적 논리와 유사하다. 형식적으로 유형 이론은 종종 직관주의 논리의 브라우어-헤이팅-콜모고로프 해석의 구현으로 인용된다.^[17] 유형을 기초로 사용할 때, 특정 유형은 명제(증명될 수 있는 진술)로 해석되고, 해당 유형에 속하는 항은 해당 명제의 증명으로 해석된다. 일부 유형이 명제로 해석될 때, 유형으로 부울 대수를 만들기 위해 이를 연결하는 데 사용할 수 있는 일반적인 유형 집합이 있다. 그러나 이 논리는 고전 논리가 아닌 직관 논리이다. 즉, 배중률이나 이중 부정은 없다.

이러한 직관적 해석 하에서 논리 연산자 역할을 하는 일반적인 유형은 다음과 같다.

논리 이름	논리 표기법	유형 표기법	유형 이름
참	$\top$	$\top$	단위 유형
거짓	$\bot$	$\bot$	빈 유형
함축	$A \to B$	$A \to B$	함수
부정	$\neg A$	$A \to \bot$	빈 유형으로의 함수
그리고	$A \land B$	$A \times B$	곱 유형
또는	$A \lor B$	$A + B$	합 유형
모든 것에 대해	$\forall a \in A, P(a)$	$\Pi a:A.P(a)$	종속 곱
존재	$\exists a \in A, P(a)$	$\Sigma a: A.P(a)$	종속 합

배중률이 성립하지 않으므로, 유형 $\Pi a.A+ (A\to\bot)$ 의 항은 없다. 마찬가지로, 이중 부정 역시 성립하지 않으므로, 유형 $\Pi A.((A\to\bot)\to\bot)\to A$ 의 항도 없다.

5. 2. 구성적 수학

페르 마틴-뢰프는 구성적 수학의 기초로서 자신의 직관주의적 유형 이론을 제안했다.^[13] 구성적 수학은 "

P(x)

속성을 가진

x

가 존재한다"는 것을 증명할 때, 특정

x

와 그것이 속성

P

를 가지고 있다는 증명을 구성해야 한다고 요구한다. 유형 이론에서 존재성은 종속 곱 유형을 사용하여 달성되며, 그 증명에는 해당 유형의 항이 필요하다.

비구성적 증명의 예는 귀류법이다. 첫 번째 단계는

x

가 존재하지 않는다고 가정하고 모순으로 반박하는 것이다. 그 단계의 결론은 "

x

가 존재하지 않는 경우는 아니다"이다. 마지막 단계는 이중 부정을 통해

x

가 존재한다고 결론 내리는 것이다. 구성적 수학은

x

가 존재한다는 결론을 내리기 위해 이중 부정을 제거하는 마지막 단계를 허용하지 않는다.^[18]

5. 3. 커리-하워드 대응

커리-하워드 대응은 논리학과 프로그래밍 언어 사이의 유사성이다. 논리에서 "A → B" 함축은 "A" 타입에서 "B" 타입으로의 함수와 유사하다. 다양한 논리 규칙들은 프로그래밍 언어의 타입에서 표현식과 유사하며, 규칙 적용은 프로그래밍 언어의 프로그램과 유사하다는 점으로 확장된다. 따라서 이 대응은 "증명은 프로그램이다"로 요약된다.^[19]

5. 4. 연구 분야

범주론 연구자들은 널리 받아들여지는 체르멜로-프렝켈 집합론의 기초를 다루는 데 어려움을 겪었다. 이는 Lawvere의 집합 범주의 기본 이론(ETCS)과 같은 제안으로 이어졌다.^[6] 호모토피 유형 이론은 유형 이론을 사용하여 이러한 맥락을 이어간다. 연구자들은 종속적 유형(특히 동일성 유형)과 대수적 위상수학(특히 호모토피) 간의 연결을 탐구하고 있다.

데카르트 닫힌 범주는 타입화된 λ-계산(람다 대수)에 해당하고, C-모노이드는 타입화되지 않은 λ-계산(람다 대수)에 해당하며, 국소 데카르트 닫힌 범주는 마르틴-뢰프 유형 이론에 해당한다. 이러한 범주론과의 연관성을 바탕으로 호모토피 유형 이론은 유형 이론과 범주론을 결합하려는 시도로, 동일성 유형에 중점을 두고 연구가 진행 중이며, 큐빅 유형 이론이 제안되었다.

6. 정의

유형 이론에서 '정의'는 프로그램이 계산하는 값의 종류(형)에 따라 구(phrase)를 분류하여 프로그램의 동작을 증명하는 방법이다. 벤자민 C. 피어스(Benjamin C. Pierce)는 형 시스템을 "프로그램이 계산하는 값의 종류에 따라 구(phrase)를 분류함으로써, 해당 프로그램이 어떤 동작을 하지 않음을 증명하는 다루기 쉬운 문법적 기법"으로 정의했다.^[20]

예를 들어, "hello"는 문자열형, 5는 정수형으로 분류하여 이 둘을 더하는 연산을 제한한다. 형 시스템 설계 및 구현은 프로그래밍 언어의 중요한 기반이며, 컴파일러의 의미론적 분석 부분에서 타입 체크 알고리즘 구축에 활용된다.

6. 1. 용어와 유형

범주론은 초기에는 기초론과 거리가 멀었지만, 점차 두 분야가 깊은 연관성을 갖는 것으로 밝혀졌다. 존 레인 벨은 "범주는 '그 자체로' 일종의 유형 이론으로 간주될 수 있다"고 언급하며, 유형 이론이 집합론보다 범주론과 더 밀접하게 관련되어 있음을 시사했다.^[20] 범주는 그 대상을 유형(또는 종류)으로 간주함으로써 유형 이론으로 볼 수 있으며, "구문이 제거된 유형 이론"으로 생각할 수 있다.^[20]

이러한 관점에서 다음과 같은 중요한 결과들이 도출되었다:^[20]

데카르트 닫힌 범주는 타입화된 람다 대수(요아킴 람벡, 1970)에 해당한다.
C-모노이드 (곱과 지수 및 하나의 비종단 객체를 가진 범주)는 타입화되지 않은 람다 대수(람벡과 데이나 스콧에 의해 1980년경 독립적으로 관찰됨)에 해당한다.
국소 데카르트 닫힌 범주는 마르틴-뢰프 유형 이론에 해당한다 (Seely, 1984).

이러한 범주론과 유형 이론의 상호 작용은 범주적 논리라는 활발한 연구 분야로 발전했으며, Jacobs (1999)의 연구가 대표적이다.

프로그래밍 언어 이론에서 형 시스템은 벤자민 C. 피어스(Benjamin C. Pierce)의 정의가 일반적이다. 그는 형 시스템을 "프로그램이 계산하는 값의 종류에 따라 구(phrase)를 분류함으로써, 해당 프로그램이 어떤 동작을 하지 않음을 증명하는 다루기 쉬운 문법적 기법"으로 정의했다.(Pierce 2002)

형 시스템은 프로그램의 값을 "형"이라고 불리는 집합으로 분류하고( "형 설정" 또는 "형 할당"), 특정 프로그램의 동작이 부적절함을 나타낸다. 예를 들어, "hello"라는 값을 문자열형, 5라는 값을 정수형으로 할 때, "hello"와 5를 더하는 것을 제한하는 것이다.

형 시스템의 설계와 구현은 프로그래밍 언어 자체만큼이나 폭넓은 주제이며, 프로그래밍 언어의 가장 큰 기반이라고도 할 수 있다. 형 이론은 프로그래밍 언어의 컴파일러에서 의미론적 분석 부분의 타입 체크 알고리즘 구축에 응용된다.

형 이론은 자연 언어의 의미론 이론 구축에도 사용된다. 몬터규 문법의 내포 논리에서 형은 가장 기본적인 형인

e

(사물)와

t

(진리값)를 기반으로, 귀납적 규칙을 통해 정의된다.

#

a

와

b

가 형일 때,

\langle a,b\rangle

도 형이다.

#

a

가 형일 때,

\langle s,a\rangle

도 형이다. 여기서

s

는 지표이다.

\langle a,b\rangle

는 형

a

의 요소에서

b

의 요소로의 함수형이다. 예를 들어

\langle e,t\rangle

는 '사물'에서 진리값으로의 함수, 즉 집합의 지시 함수이다.

\langle\langle e,t\rangle,t\rangle

는 지시 함수가 가리키는 집합에서 진리값으로의 함수, 즉 집합의 집합으로, ''every boy''나 ''nobody''와 같은 표현에 해당한다.

6. 1. 1. 원자적 용어

범주론에서 차용된 개념으로, 가장 기본적인 유형을 원자라고 하며, 원자를 유형으로 갖는 항을 원자 항이라고 한다. 예를 들어

\mathsf{nat}

(자연수),

\mathsf{bool}

(불린)과 변수 등이 이에 해당한다.

6. 1. 2. 함수 용어

요아킴 람벡은 데카르트 닫힌 범주가 타입화된 λ-계산에 해당한다고 보았다(1970).^[20] 데이나 스콧과 람벡은 C-모노이드(곱과 지수 및 하나의 비종단 객체를 가진 범주)가 타입화되지 않은 λ-계산에 해당함을 1980년경 독립적으로 관찰했다.^[20] Seely는 1984년에 국소 데카르트 닫힌 범주가 마르틴-뢰프 유형 이론에 해당한다는 것을 보였다.^[20]

6. 1. 3. 람다 용어

요아킴 람벡은 1970년에 데카르트 닫힌 범주가 타입화된 람다 대수에 해당한다는 것을 보였다.^[20] 1980년경에는 람벡과 데이나 스콧이 C-모노이드(곱과 지수 및 하나의 비종단 객체를 가진 범주)가 타입화되지 않은 람다 대수에 해당한다는 것을 독립적으로 관찰했다.^[20] 1984년에는 국소 데카르트 닫힌 범주가 마르틴-뢰프 유형 이론에 해당한다는 것이 밝혀졌다(Seely).^[20]

6. 2. 추론 규칙

타입 이론과 관련된 많은 프로그램(예: 대화형 정리 증명기)은 타입 추론도 수행한다. 이는 사용자가 의도한 규칙을 선택할 수 있게 해주며, 사용자의 액션을 줄여준다.^[16]

가장 기본적인 유형을 원자라고 하며, 원자를 유형으로 갖는 항을 원자 항이라고 한다. 유형 이론에 포함된 일반적인 원자 항에는 nat^영어 유형으로 표기되는 자연수, bool^영어 유형으로 표기되는 부울 논리 값(true^영어/false^영어), 그리고 유형이 다를 수 있는 형식적 변수가 있다.^[16]

예를 들어, 다음은 원자 항이 될 수 있다.

$42:\mathsf{nat}$
$\mathrm{true}:\mathsf{bool}$
$x:\mathsf{nat}$
$y:\mathsf{bool}$

6. 2. 1. 함수 적용

만약

t

가

\sigma\to\tau

유형이고,

s

가

\sigma

유형이면,

(t\,s)

는

\tau

유형이다.^[16]

6. 2. 2. 환원

\beta

-환원:

(\lambda v. t)\,s\rightarrow t[v \colon= s]

\eta

-환원:

(\lambda v. t\, v)\rightarrow t

(단,

v

는

t

에서 자유 변수가 아님)

6. 3. 일반적인 용어와 유형

페르 마틴뢰프는 구성적 수학의 기초로서 자신의 직관주의적 유형 이론을 제안했다.^[13] 구성적 수학은 "

P(x)

속성을 가진

x

가 존재한다"는 것을 증명할 때, 특정

x

와 그것이 속성

P

를 가지고 있다는 증명을 구성해야 한다고 요구한다. 유형 이론에서 존재성은 종속 곱 유형을 사용하여 달성되며, 그 증명에는 해당 유형의 항이 필요하다.

비구성적 증명의 예는 귀류법이다. 첫 번째 단계는

x

가 존재하지 않는다고 가정하고 모순으로 반박하는 것이다. 그 단계의 결론은 "

x

가 존재하지 않는 경우는 아니다"이다. 마지막 단계는 이중 부정을 통해

x

가 존재한다고 결론 내리는 것이다. 구성적 수학은

x

가 존재한다는 결론을 내리기 위해 이중 부정을 제거하는 마지막 단계를 허용하지 않는다.^[18]

6. 4. 종속 타이핑

복잡한 항의 유형은 인수의 유형에 따라 달라질 수 있다. 예를 들어

\mathsf{list}\,a

,

\mathsf{vector}\,n

과 같은 표현이 있다. 람다 큐브는 다양한 제한 사항과 종속 타이핑 수준을 연구하기 위한 프레임워크이다.^[4]

6. 4. 1. 곱 유형

곱 유형은 두 가지 유형에 의존하며, 용어는 순서쌍

(s,t)

또는 기호

\times

로 표현된다. 제거자 함수는 다음과 같다.^[4]

$\mathrm{first}:(\Pi\,\sigma\,\tau.\sigma\times\tau\to\sigma)$
$\mathrm{second}:(\Pi\,\sigma\,\tau.\sigma\times\tau\to\tau)$

6. 4. 2. 종속 곱과 합

추론 규칙을 통해 용어들을 결합하는 방식을 명시함으로써 유형 이론의 강력함을 확인할 수 있다.^[4] 함수를 갖는 유형 이론은 함수 적용의 추론 규칙 또한 가진다. 만약

t

가

\sigma\to\tau

유형의 용어이고,

s

가

\sigma

유형의 용어라면,

t

를

s

에 적용한 결과(보통

(t\,s)

로 표기)는

\tau

유형이 된다. 예를 들어,

0:\textsf{nat}

,

1:\textsf{nat}

,

2:\textsf{nat}

의 유형 표기를 알고 있다면, 함수 적용을 통해 다음 유형 표기를 추론할 수 있다.^[16]

$(\mathrm{add}\,1): \textsf{nat}\to\textsf{nat}$
$((\mathrm{add}\,2)\,0): \textsf{nat}$
$((\mathrm{add}\,1)((\mathrm{add}\,2)\,0)): \textsf{nat}$

괄호는 연산 순서를 나타낸다. 그러나 관례상 함수 적용은 좌측 결합성을 가지므로, 필요한 경우가 아니면 괄호를 생략할 수 있다.^[16] 위의 세 가지 예시에서 처음 두 예시는 모든 괄호를 생략할 수 있으며, 세 번째 예시는

\mathrm{add}\,1\, (\mathrm{add}\,2\,0): \textsf{nat}

로 간단하게 나타낼 수 있다.

공집합형은 항이 없다. 이 유형은 보통

\bot

또는

\mathbb 0

으로 표기된다. 공집합형의 한 가지 용도는 형식 거주 가능성 증명이다. 만약 형식

a

에 대해, 형식

a\to\bot

의 함수를 유도하는 것이 일관된다면,

a

는 ''비거주'' 상태이며, 이는 항이 없음을 의미한다.

6. 4. 3. 항등형

커리-하워드 대응에 따라, 항등형은 명제 논리의 명제적 동치를 반영하기 위해 도입된 형식으로, 형식 이론이 이미 제공하는 판단적 (구문론적) 동치와는 대조적이다.^[1]

항등형은 동일한 유형의 두 개의 항을 필요로 하며, 기호

=

으로 표기한다.^[1] 예를 들어,

x+1

과

1+x

가 항이라면,

x+1=1+x

는 가능한 유형이다.^[1] 표준 항은 반사 함수

\mathrm{refl}

로 생성된다.^[1] 항

t

에 대해,

\mathrm{refl}\,t

호출은 유형

t=t

를 채우는 표준 항을 반환한다.^[1]

형식 이론에서 등식의 복잡성은 활발한 연구 주제가 되고 있으며, 호모토피 형식 이론은 형식 이론에서의 등식을 주로 다루는 주목할 만한 연구 분야이다.^[1]

6. 4. 4. 귀납적 유형

귀납적 타입은 매우 다양한 타입을 생성하기 위한 일반적인 템플릿이다. 실제로 위에서 설명한 모든 타입과 그 이상을 귀납적 타입의 규칙을 사용하여 정의할 수 있다. 귀납적 타입을 생성하는 두 가지 방법은 귀납-재귀와 귀납-귀납이다. 람다 항만 사용하는 방법은 스콧 인코딩이다.

Coq와 Lean과 같은 일부 증명 보조자는 귀납적 타입을 가진 구성 계산법인 귀납적 구성 계산법을 기반으로 한다.

7. 집합론과의 차이점

집합론은 추론 규칙과 공리를 모두 갖지만, 유형 이론은 규칙만 갖는다는 점에서 차이가 있다.^[14] 대부분의 유형 이론은 공리를 가지지 않고 추론 규칙에 의해 정의된다.

고전 집합론과 논리는 배중률을 갖지만, 유형 이론은 직관주의 논리를 따르는 경향이 있다.^[17] 유형 이론에서 "그리고"와 "또는"의 개념을 유형으로 인코딩하면 배중률이 반드시 성립하지 않을 수 있다.

집합론에서 원소는 여러 집합에 나타날 수 있지만, 유형 이론에서 항은 일반적으로 하나의 유형에만 속한다.^[4] 집합론에서는 원소가 하나의 집합에 제한되지 않고 다른 집합의 부분 집합과 합집합에 나타날 수 있다. 유형 이론에서는 부분 집합을 나타낼 때 술어 함수를 사용하거나, 종속 유형 곱 유형을 사용할 수 있다. 합집합의 경우, 유형 이론은 새로운 표준 항을 포함하는 합 유형을 사용한다.

유형 이론은 내장된 계산 개념을 갖는다. 예를 들어, "1+1"과 "2"는 유형 이론에서 다른 항이지만 동일한 값으로 계산된다. 반면 집합론에서 "1+1=2"는 "1+1"이 "2"라는 값을 가리키는 또 다른 방법임을 의미한다.

집합론은 수를 집합으로 인코딩하지만, 유형 이론은 처치 인코딩이나 귀납적 유형으로 수를 인코딩할 수 있다.

유형 이론에서 증명은 유형이지만, 집합론에서 증명은 기본 일차 논리의 일부이다.^[14]

7. 1. 유형 이론의 속성

용어는 항상 하나의 타입에 속한다.^[4] 계산은 규칙을 반복적으로 적용하여 수행된다. 많은 종류의 이론은 강정규화되어 있는데, 이는 규칙을 적용하는 모든 순서가 항상 동일한 결과를 낸다는 것을 의미한다. 하지만 그렇지 않은 경우도 있다. 정규화 타입 이론에서 한 방향으로의 계산 규칙은 "환원 규칙"이라고 하며, 규칙을 적용하는 것은 용어를 "환원"시키는 것이다. 규칙이 한 방향이 아니라면 "변환 규칙"이라고 한다.

일부 타입 조합은 다른 타입 조합과 동등하다.^[25] 함수를 "지수"로 간주할 때, 타입의 조합은 대수적 항등식과 유사하게 작성될 수 있다. 따라서

{\mathbb 0} + A \cong A

,

{\mathbb 1} \times A \cong A

,

{\mathbb 1} + {\mathbb 1} \cong {\mathbb 2}

,

A^{B+C} \cong A^B \times A^C

,

A^{B\times C} \cong (A^B)^C

이다.

7. 2. 공리

대부분의 유형 이론은 공리를 갖지 않지만, 필요에 따라 추가될 수 있다. 이는 유형 이론이 추론 규칙에 의해 정의되기 때문이다. 때때로 유형 이론은 몇 가지 공리를 추가하기도 하는데, 이는 추론 규칙을 사용하여 유도 없이 받아들여지는 판단이다. 규칙을 통해 깔끔하게 추가할 수 없는 속성을 보장하기 위해 종종 추가된다.

일반적으로 사용되는 일부 공리는 다음과 같다.

"공리 K"는 "동일성 증명의 유일성"을 보장한다. 즉, 동일성 유형의 모든 용어가 반사성과 같다는 것이다.^[27]
"단일성 공리"는 유형의 동등성이 유형의 동일성과 같다는 것을 주장한다. 이 속성에 대한 연구는 공리 없이도 속성이 유지되는 큐비컬 유형 이론으로 이어졌다.^[28]
"배제된 중간의 법칙"은 직관주의 논리 대신 고전 논리를 원하는 사용자를 만족시키기 위해 종종 추가된다.

선택 공리는 대부분의 유형 이론에서 추론 규칙으로부터 파생될 수 있기 때문에 유형 이론에 추가될 필요가 없다. 이는 유형 이론의 구성적 수학적 특성 때문인데, 여기서 값이 존재함을 증명하려면 값을 계산하는 방법이 필요하다. 선택 공리는 대부분의 집합론보다 유형 이론에서 덜 강력한데, 유형 이론의 함수는 계산 가능해야 하고, 구문 기반이므로 유형의 용어 수는 셀 수 있어야 하기 때문이다.

8. 유형 이론 목록

태그된 유니온이라고도 불리는 합 타입은 두 개의 타입에 의존하며, 일반적으로 $+$ 또는 $\sqcup$ 기호를 사용하여 표기한다. 타입 $\sigma\sqcup\tau$ 는 생성자 $\mathrm{left}:\sigma\to(\sigma\sqcup\tau)$ 및 $\mathrm{right}:\tau\to(\sigma\sqcup\tau)$ 를 사용하여 정의되며, 이들은 단사 함수이다. 또한, 제거자 함수 $\mathrm{match}:(\Pi\,\rho.(\sigma\to\rho)\to(\tau\to\rho)\to(\sigma\sqcup\tau)\to\rho)$ 를 가지며, 다음과 같은 특징을 가진다.

$\mathrm{match}\,f\,g\,(\mathrm{left}\,x)$ 는 $f\,x$ 를 반환한다.
$\mathrm{match}\,f\,g\,(\mathrm{right}\,y)$ 는 $g\,y$ 를 반환한다.

합 타입은 논리적 분리 및 합집합의 개념에 사용된다.

기타 유형 이론은 다음과 같다.

오토매스
ST 형식 이론
UTT (Luo의 종속 유형의 통합 이론)
일부 형태의 조합 논리
람다 큐브 (일명 순수 형식 시스템)에서 정의된 다른 것들
형식화된 람다 계산이라는 이름으로 된 다른 것들

활발히 연구 중인 유형 이론은 다음과 같다.

호모토피 형식적 의미론은 형식적 의미론의 동등성을 탐구한다.
큐비컬 형식적 의미론은 호모토피 형식적 의미론의 구현체이다.

8. 1. 주요 유형 이론

종속 타입의 흔한 두 가지 유형인 종속 곱 타입과 종속 합 타입은 BHK 직관 논리를 전칭 및 존재 양화와 동일하게 동작하게 하여 부호화할 수 있으며, 이는 커리-하워드 대응에 의해 형식화된다.^[23] 이들은 또한 곱과 합집합을 집합론에서 연결하므로, 각각

\Pi

와

\Sigma

기호로 표기되는 경우가 많다.^[17] 종속 곱 타입과 종속 합 타입은 일반적으로 함수 타입에 나타나며 프로그래밍 언어에 자주 통합된다.^[25]

예를 들어,

\mathrm{append}

함수는

\mathsf{list}\,a

와

a

타입의 항을 입력으로 받아 마지막에 요소가 추가된 리스트를 반환한다. 이 함수의 타입 주석은

\mathrm{append}:(\Pi\,a.\mathsf{list}\,a\to a\to\mathsf{list}\,a)

가 될 수 있으며, 이는 "모든 타입

a

에 대해,

\mathsf{list}\,a

와

a

를 전달하면

\mathsf{list}\,a

를 반환한다"로 읽을 수 있다.

합 타입은 두 번째 타입이 첫 번째 항의 값에 의존하는 종속 쌍에서 볼 수 있다. 이는 함수가 입력에 따라 다른 유형의 출력을 반환할 수 있는 컴퓨터 과학에서 자연스럽게 발생한다. 예를 들어, 부울 타입은 일반적으로 다음과 같이 세 개의 인수를 받아 동작하는 제거자 함수

\mathrm{if}

로 정의된다.

$\mathrm{if}\,\mathrm{true}\,x\,y$ 는 $x$ 를 반환한다.
$\mathrm{if}\,\mathrm{false}\,x\,y$ 는 $y$ 를 반환한다.

이 함수의 반환 타입은

\mathsf{bool}

입력에 따라 달라진다. 타입 이론에서 종속 타입을 허용하는 경우, 다음과 같은 함수

\mathrm{TF}\colon\mathsf{bool}\to U\to U\to U

를 정의할 수 있다.

$\mathrm{TF}\,\mathrm{true}\,\sigma\,\tau$ 는 $\sigma$ 를 반환한다.
$\mathrm{TF}\,\mathrm{false}\,\sigma\,\tau$ 는 $\tau$ 를 반환한다.

이때

\mathrm{if}

의 타입은

(\Pi\,\sigma\,\tau.\mathsf{bool}\to\sigma\to\tau\to(\Sigma\,x:\textsf{bool}.\mathrm{TF}\,x\,\sigma\,\tau))

로 쓸 수 있다.

주요 유형 이론은 다음과 같다.

단순 타입 람다 계산법은 고차 논리이다.
직관적 타입 이론
시스템 F
LF는 종종 다른 타입 이론을 정의하는 데 사용된다.
구성의 계산과 그 파생물들

8. 2. 기타 유형 이론

오토매스
ST 형식 이론
UTT (Luo의 종속 유형의 통합 이론)
일부 형태의 조합 논리
람다 큐브 (일명 순수 형식 시스템)에서 정의된 다른 것들
형식화된 람다 계산이라는 이름으로 된 다른 것들

8. 3. 활발히 연구 중인 유형 이론

호모토피 형식적 의미론은 형식적 의미론의 동등성을 탐구한다.
큐비컬 형식적 의미론은 호모토피 형식적 의미론의 구현체이다.

참조

_[1] 서적 Getting Started With Julia Programming 2015
_[2] 웹사이트 v.1 Types https://docs.juliala[...] 2022-03-24
_[3] 웹사이트 Russell’s Paradox https://plato.stanfo[...] 2020-10-12
_[4] 논문 A formulation of the simple theory of types
_[5] 서적 Introduction To Mathematical Logic Vol 1 https://archive.org/[...] 1956
_[6] 문서 ETCS
_[7] 서적 Modern Perspectives in Type-Theoretical Semantics https://books.google[...] Springer 2017-02-07
_[8] 서적 Elements of Formal Semantics: An Introduction to the Mathematical Theory of Meaning in Natural Language https://books.google[...] Edinburgh University Press 2016-04-08
_[9] 간행물 Type theory and semantics in flux http://lecomte.al.fr[...] Handbook of the Philosophy of Science 2012
_[10] 논문 Generalized quantifiers and natural language https://philpapers.o[...] 1981
_[11] 논문 Records and Record Types in Semantic Theory
_[12] 서적 Type theory and semantics in flux Handbook of the Philosophy of Science. Volume 14: Philosophy of Linguistics. Elsevier. 2010
_[13] 논문 Truth of a proposition, evidence of a judgement, validity of a proof https://doi.org/10.1[...] 1987-12-01
_[14] 서적 Homotopy Type Theory: Univalent Foundations of Mathematics https://homotopytype[...] Homotopy Type Theory
_[15] 웹사이트 Types of proof system https://www.logicmat[...] 2021-12-29
_[16] 서적 Lambda Calculus with Types https://books.google[...] Cambridge University Press 2013-06-20
_[17] 웹사이트 Rules to Martin-Löf's Intuitionistic Type Theory https://hott.github.[...]
_[18] 웹사이트 Axioms and Computation https://ncatlab.org/[...]
_[19] 간행물 A long and winding road towards modular synthesis Springer
_[20] 서적 Sets and Extensions in the Twentieth Century Elsevier
_[21] 간행물 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) IEEE 2021-06-29
_[22] 서적 Getting Started with Julia https://www.oreilly.[...] 2015
_[23] 간행물 Dependent Types at Work https://doi.org/10.1[...] Springer 2009
_[24] 논문 Introduction to generalized type systems https://doi.org/10.1[...] 1991-04
_[25] Youtube Programming with Math (Exploring Type Theory) https://www.youtube.[...]
_[26] 웹사이트 Axioms and Computation https://leanprover.g[...]
_[27] 웹사이트 Axiom K http://nlab-pages.s3[...]
_[28] 논문 Cubical Type Theory: A constructive interpretation of the univalence axiom https://www.cse.chal[...] 2016
_[29] 문서 Letter to Frege 1902
_[30] 문서 Mathematical Logic as based on the theory of types 1908

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com