의존형

1. 개요

의존형은 타입의 형태가 값에 따라 달라지는 프로그래밍 언어의 특징을 의미한다. 1934년 하스켈 커리의 연구를 시작으로, 윌리엄 하워드와 니콜라스 데 브라위언의 확장을 거쳐 프로그래밍과 논리학의 연관성을 깊게 하는 데 기여했다. 의존형은 형식적 정의를 통해 색인된 집합족의 유형과 유사하게 설명되며, Π형(의존 곱형)과 Σ형(의존 쌍형)으로 구분된다. 람다 큐브는 의존형을 포함한 다양한 타입 시스템을 분류하는 데 사용되며, 프로그래밍 언어와 논리학의 동시성을 통해 복잡한 수학적 속성을 표현하고, 코드 생성 및 프로그램 검증에 활용될 수 있다. 여러 프로그래밍 언어들이 의존형을 지원하며, 언어별 특징을 비교 분석할 수 있다.

2. 역사

1934년, 하스켈 커리는 형식적 람다 계산과 그 조합 논리 대응물에서 사용된 타입이 명제 논리의 공리와 동일한 패턴을 따른다는 것을 발견했다. 더 나아가, 논리의 모든 증명에 대해 프로그래밍 언어에는 일치하는 함수(항)가 있었다. 커리의 예시 중 하나는 단순 타입 람다 계산과 직관 논리 사이의 대응 관계였다.

술어 논리는 명제 논리를 확장한 것으로, 양화사를 추가한다. 하워드와 데 브라위언은 "모든"에 해당하는 종속 함수와 "존재한다"에 해당하는 종속 쌍에 대한 타입을 생성하여 람다 계산을 이 더욱 강력한 논리에 맞게 확장했다.

이러한 점과 하워드의 다른 연구로 인해, 명제-타입은 커리-하워드 대응으로 알려지게 되었다. 의존형은 프로그래밍과 논리학의 연관성을 깊게 하기 위해 만들어졌다.

2.1. 초기 역사

1934년, 하스켈 커리는 형식적 람다 계산과 그 조합 논리 대응물에서 사용된 타입이 명제 논리의 공리와 동일한 패턴을 따른다는 것을 발견했다. 논리의 모든 증명에 대해 프로그래밍 언어에는 일치하는 함수(항)가 있었으며, 커리의 예시 중 하나는 단순 타입 람다 계산과 직관 논리 사이의 대응 관계였다.

술어 논리는 명제 논리를 확장한 것으로, 하워드와 데 브라위언은 "모든"에 해당하는 종속 함수와 "존재한다"에 해당하는 종속 쌍에 대한 타입을 생성하여 람다 계산을 이 더욱 강력한 논리에 맞게 확장했다. 이러한 점과 하워드의 다른 연구로 인해, 명제-타입은 커리-하워드 대응으로 알려지게 되었다. 의존형은 프로그래밍과 논리학의 연관성을 깊게 하기 위해 만들어졌다.

2.2. 술어 논리로의 확장

하스켈 커리는 1934년에 형식적 람다 계산과 그 조합 논리 대응물에서 사용된 타입이 명제 논리의 공리와 동일한 패턴을 따른다는 것을 발견했다. 논리의 모든 증명에 대해 프로그래밍 언어에는 일치하는 함수(항)가 있었으며, 단순 타입 람다 계산과 직관 논리 사이의 대응 관계가 그 예시 중 하나였다.

술어 논리는 명제 논리를 확장한 것으로, 양화사를 추가한다. 윌리엄 앨빈 하워드와 니콜라스 고베르트 데 브라위언은 "모든"에 해당하는 종속 함수와 "존재한다"에 해당하는 종속 쌍에 대한 타입을 생성하여 람다 계산을 이 더욱 강력한 논리에 맞게 확장했다. 이러한 점과 하워드의 다른 연구로 인해, 명제-타입은 커리-하워드 대응으로 알려지게 되었다.

2.3. 커리-하워드 대응

1934년, 하스켈 커리는 형식적 람다 계산과 그 조합 논리 대응물에서 사용된 타입이 명제 논리의 공리와 동일한 패턴을 따른다는 것을 발견했다. 더 나아가, 논리의 모든 증명에 대해 프로그래밍 언어에는 일치하는 함수(항)가 있었다. 커리의 예시 중 하나는 단순 타입 람다 계산과 직관 논리 사이의 대응 관계였다.

술어 논리는 명제 논리를 확장한 것으로, 양화사를 추가한다. 하워드와 데 브라위언은 "모든"에 해당하는 종속 함수와 "존재한다"에 해당하는 종속 쌍에 대한 타입을 생성하여 람다 계산을 이 더욱 강력한 논리에 맞게 확장했다.

이러한 점과 하워드의 다른 연구로 인해, 명제-타입은 커리-하워드 대응으로 알려지게 되었다.

3. 형식적 정의

대략적으로 말해서, 의존형은 색인된 집합족의 유형과 유사하다. 보다 형식적으로, 유형의 우주 $\backslash mathcal\{U\}$에서 $A:\backslash mathcal\{U\}$의 유형이 주어지면, 각 항 $a:A$에 유형 $B(a):\backslash mathcal\{U\}$를 할당하는 유형족 $B:A\backslash to\backslash mathcal\{U\}$을 가질 수 있다. 우리는 유형 $B(a)$가 $a$에 따라 달라진다고 말한다.

공역이 인수에 따라 변화하는 함수는 의존 함수라고 하며, 이러한 함수를 위한 형은 의존형 또는 의존곱형이라고 하며, Π형이라고도 불린다. 의존곱형은
:$\backslash Pi\_\{(x:A)\}B(x)$
혹은
:$\backslash Pi\; (x:A),B(x)$
로 표기된다.

만약 B가 상수 함수 $B(x)=C$라면, 의존곱형은 일반적인 함수형(화살표형) $A\backslash to\; C$가 된다. 즉, $\backslash Pi\_\{(x:A)\}B$는 형 판단에서 함수형 $A\backslash to\; C$와 같다.

Π형이라는 이름은, 의존곱형이 형의 곱으로 간주될 수 있다는 생각에서 유래되었다. 의존곱형은 전칭 양화의 모델로 이해할 수도 있다.

예를 들어, 실수의 $n$개의 쌍을 $\backslash mbox\{Vec\}(\{\backslash mathbb\; R\},n)$으로 표기할 때, $\backslash Pi\_\{(n:\{\backslash mathbb\; N\})\}\; \backslash mbox\{Vec\}(\{\backslash mathbb\; R\},n)$는, 자연수 n을 받아서 n개의 실수의 쌍을 반환하는 함수의 형이다. 일반적인 함수 공간은, 의존곱형에서 반환값의 형이 실제로는 인수에 의존하지 않는 특별한 경우로 나타난다. 예를 들어, $\backslash Pi\_\{(n:\{\backslash mathbb\; N\})\}\backslash ;\; \{\backslash mathbb\; R\}$는 자연수에서 실수로의 함수의 형이며, 단순형 지정 람다 계산에서는 $\{\backslash mathbb\; N\}\backslash to\{\backslash mathbb\; R\}$로 표기된다.

형 다형 함수는 의존 함수(즉, 의존곱형을 갖는 함수)의 중요한 예이다. 다형 함수는, 형이 주어지면, 그 형을 포함하는 형을 갖는 값으로 동작한다. 예를 들어, 항등 함수, 즉 임의의 형 A에 대해 $a:A$를 받아서 a를 그대로 반환하는 함수의 형은,
:$\backslash Pi\_\{(A:\backslash mathcal\{U\})\}\; A\backslash to\; A$
로 쓸 수 있다.

의존 쌍 형식의 쌍대는 의존 쌍 형식, 의존 합 형식, 시그마 형식 또는 의존 곱 형식이다. 시그마 형식은 또한 존재 양화사로 이해될 수 있다.

의존 쌍 형식은 두 번째 항의 형식이 첫 번째 항의 값에 의존하는 순서쌍의 아이디어를 포착한다. 만약 $(a,b):\backslash sum\_\{x:A\}\; B(x),$이면 $a:A$이고 $b:B(a)$이다. 만약 $B$가 상수 함수라면, 의존 쌍 형식은 곱 형식이 되며, 즉, 일반적인 데카르트 곱 $A\backslash times\; B$와 동일하다.

$\backslash Sigma\_\{(x:A)\}\; B(x)$로 표기된다.

커리-하워드 대응에 의해, B는 A의 항에 대한 논리적 술어로 해석될 수 있다. 주어진 a:A에 대해, 타입 B(a)가 채워져 있는지 여부는 a가 이 술어를 만족하는지 여부를 나타낸다.

예를 들어, $m:\backslash mathbb\{N\}$이 $n:\backslash mathbb\{N\}$보다 작거나 같다는 것은, $m\; +\; k\; =\; n$을 만족하는 다른 자연수 $k:\backslash mathbb\{N\}$이 존재할 경우에만 해당한다.

$$m\backslash le\; n\; \backslash iff\; \backslash exists\{k\}\{\backslash in\}\backslash mathbb\{N\}\backslash ,m+k=n.$$

이 명제는 종속 쌍 타입에 해당한다.

$$\backslash sum\_\{k:\backslash mathbb\{N\}\}\; m+k=n.$$

즉, $m$이 $n$보다 작거나 같다는 명제의 증명은, $m$과 $n$의 차이인 음수가 아닌 수 $k$와, 등식 $m\; +\; k\; =\; n$의 증명 둘 다를 포함하는 쌍이다.

의존곱형의 쌍대는 의존 쌍형, 의존 합형, 또는 Σ형이라고 불리는 형식이다. 이는 여곱, 직합, 비교환 합 등의 유추이다. 의존 합형은 존재량화의 모델로 이해할 수도 있다.

$\backslash Sigma\; A\; B\_a:\; \backslash mathcal\{U\}$를, 형식 $A:\; \backslash mathcal\{U\}$ 위에 술어 $B:\; A\; \backslash rarr\; \backslash mathcal\{U\}$를 양화한 의존 합 타입으로 한다. 이 때, $B\_a$가 성립하는 $a:A$가 존재한다는 것과, $\backslash Sigma\; A\; B\_a$가 공집합이 아니라는 것은 동치이다. 예를 들어, a가 b 이하라는 것과, 자연수 n과 a+n=b의 증명의 쌍이 존재한다는 것은 동치이다.
:$a\backslash le\; b\; \backslash iff\; \backslash Sigma\; \backslash mathbb\{N\}\; (\backslash lambda\; n\; \backslash rarr\; a+n=b)$

3.1. Π 타입 (의존 곱 타입)

반환 값의 유형이 인수에 따라 달라지는 함수 (즉, 고정된 공역이 없음)를 의존형 함수라고 하며, 이 함수의 유형을 의존 곱 유형, 파이-유형 (Π 유형) 또는 의존 함수 유형이라고 한다. 유형의 패밀리 $B:\; A\; \backslash to\; \backslash mathcal\{U\}$에서 의존 함수 유형 $\backslash prod\_\{x\; :\; A\}\; B(x)$를 구성할 수 있는데, 이 유형의 항은 항 $a\; :\; A$를 취해 $B(a)$의 항을 반환하는 함수이다. 이 예에서 의존 함수 유형은 일반적으로 $\backslash prod\_\{x:A\}\; B(x)$ 또는 $\backslash prod\; \{(x:A)\}\; B(x)$로 표기된다.

$B:A\backslash to\backslash mathcal\{U\}$가 상수 함수인 경우, 해당 의존 곱 유형은 일반적인 함수 유형과 동일하다. 즉, $B$가 $x$에 의존하지 않으면 $\backslash prod\_\{x:A\}B$는 $A\backslash to\; B$와 판단적으로 같다.

'Π-유형'이라는 이름은 이것이 유형의 데카르트 곱으로 간주될 수 있다는 아이디어에서 유래했다. Π-유형은 또한 모형 전칭 양화사로 이해될 수 있다.

예를 들어, 실수의 n-튜플에 대해 $\backslash operatorname\{Vec\}(\backslash mathbb\{R\},n)$이라고 쓰면, $\backslash prod\_\{n:\backslash mathbb\{N\}\}\; \backslash operatorname\{Vec\}(\backslash mathbb\{R\},n)$은 주어진 자연수 에 대해 크기가 인 실수 튜플을 반환하는 함수의 유형이 된다. 일반적인 함수 공간은 범위 유형이 실제로 입력에 의존하지 않는 특수한 경우에 발생한다. 예를 들어, $\backslash prod\_\{n:\backslash mathbb\{N\}\}\; \{\backslash mathbb\{R\}\}$은 자연수에서 실수로의 함수 유형이며, 이는 타입 람다 계산에서 $\backslash mathbb\{N\}\backslash to\backslash mathbb\{R\}$로 쓰여진다.

형 다형 함수는 의존 함수(즉, 의존곱형을 갖는 함수)의 중요한 예이다. 다형 함수는, 형이 주어지면, 그 형을 포함하는 형을 갖는 값으로 동작한다. 예를 들어, 항등 함수, 즉 임의의 형 A에 대해 $a:A$를 받아서 a를 그대로 반환하는 함수의 형은,
:$\backslash Pi\_\{(A:\backslash mathcal\{U\})\}\; A\backslash to\; A$
로 쓸 수 있다.

3.2. Σ 타입 (의존 합 타입)

의존 쌍 형식의 쌍대는 의존 쌍 형식, 의존 합 형식, 시그마 형식, 또는 (혼란스럽게도) 의존 곱 형식이다. 시그마 형식은 또한 존재 양화사로 이해될 수 있다.

의존 쌍 형식은 두 번째 항의 형식이 첫 번째 항의 값에 의존하는 순서쌍의 아이디어를 포착한다. 만약 $(a,b):\backslash sum\_\{x:A\}\; B(x),$이면 $a:A$이고 $b:B(a)$이다. 만약 $B$가 상수 함수라면, 의존 쌍 형식은 곱 형식이 되며, 즉, 일반적인 데카르트 곱 $A\backslash times\; B$와 동일하다.

$\backslash Sigma\_\{(x:A)\}\; B(x)$로 표기된다.

커리-하워드 대응에 의해, B는 A의 항에 대한 논리적 술어로 해석될 수 있다. 주어진 a:A에 대해, 타입 B(a)가 채워져 있는지 여부는 a가 이 술어를 만족하는지 여부를 나타낸다.

예를 들어, $m:\backslash mathbb\{N\}$이 $n:\backslash mathbb\{N\}$보다 작거나 같다는 것은, $m\; +\; k\; =\; n$을 만족하는 다른 자연수 $k:\backslash mathbb\{N\}$이 존재할 경우에만 해당한다.

$$m\backslash le\; n\; \backslash iff\; \backslash exists\{k\}\{\backslash in\}\backslash mathbb\{N\}\backslash ,m+k=n.$$

이 명제는 종속 쌍 타입에 해당한다.

$$\backslash sum\_\{k:\backslash mathbb\{N\}\}\; m+k=n.$$

즉, $m$이 $n$보다 작거나 같다는 명제의 증명은, $m$과 $n$의 차이인 음수가 아닌 수 $k$와, 등식 $m\; +\; k\; =\; n$의 증명 둘 다를 포함하는 쌍이다.

의존곱형의 쌍대는 의존 쌍형, 의존 합형, 또는 Σ형이라고 불리는 형식이다. 이는 여곱, 직합, 비교환 합 등의 유추이다. 의존 합형은 존재량화의 모델로 이해할 수도 있다.

$\backslash Sigma\; A\; B\_a:\; \backslash mathcal\{U\}$를, 형식 $A:\; \backslash mathcal\{U\}$ 위에 술어 $B:\; A\; \backslash rarr\; \backslash mathcal\{U\}$를 양화한 의존 합 타입으로 한다. 이 때, $B\_a$가 성립하는 $a:A$가 존재한다는 것과, $\backslash Sigma\; A\; B\_a$가 공집합이 아니라는 것은 동치이다. 예를 들어, a가 b 이하라는 것과, 자연수 n과 a+n=b의 증명의 쌍이 존재한다는 것은 동치이다.
:$a\backslash le\; b\; \backslash iff\; \backslash Sigma\; \backslash mathbb\{N\}\; (\backslash lambda\; n\; \backslash rarr\; a+n=b)$

3.2.1. 존재 양화로서의 예시

$A:\backslash mathcal\{U\}$를 어떤 타입이라고 하고, $B:A\backslash to\backslash mathcal\{U\}$라고 하자. 커리-하워드 대응에 의해, $B$는 $A$의 항에 대한 논리적 술어로 해석될 수 있다. 주어진 $a\; :\; A$에 대해, 타입 $B(a)$가 채워져 있는지 여부는 $a$가 이 술어를 만족하는지 여부를 나타낸다. 이 대응은 존재 정량화와 종속 쌍으로 확장될 수 있다: 명제 $\backslash exists\{a\}\{\backslash in\}A\backslash ,B(a)$는 타입 $\backslash sum\_\{a:A\}B(a)$가 채워져 있을 경우에만 참이다.

예를 들어, $m:\backslash mathbb\{N\}$이 $n:\backslash mathbb\{N\}$보다 작거나 같다는 것은, $m\; +\; k\; =\; n$을 만족하는 다른 자연수 $k:\backslash mathbb\{N\}$이 존재할 경우에만 해당한다. 논리에서, 이 명제는 존재 정량화로 표현된다:

$$m\backslash le\; n\; \backslash iff\; \backslash exists\{k\}\{\backslash in\}\backslash mathbb\{N\}\backslash ,m+k=n.$$

이 명제는 종속 쌍 타입에 해당한다:

$$\backslash sum\_\{k:\backslash mathbb\{N\}\}\; m+k=n.$$

즉, $m$이 $n$보다 작거나 같다는 명제의 증명은, $m$과 $n$의 차이인 음수가 아닌 수 $k$와, 등식 $m\; +\; k\; =\; n$의 증명 둘 다를 포함하는 쌍이다.

의존곱형의 쌍대는 의존 쌍형, 의존 합형, 또는 Σ형이라고 불리는 형식이다. 이는 여곱, 직합, 비교환 합 등의 유추이다. 의존 합형은 존재량화의 모델로 이해할 수도 있다. 의존 합형은
:$\backslash Sigma\_\{(x:A)\}\; B(x)$
로 표기된다.

$\backslash Sigma\; A\; B\_a:\; \backslash mathcal\{U\}$를, 형식 $A:\; \backslash mathcal\{U\}$ 위에 술어 $B:\; A\; \backslash rarr\; \backslash mathcal\{U\}$를 양화한 의존 합 타입으로 한다. 이 때, $B\_a$가 성립하는 $a:A$가 존재한다는 것과, $\backslash Sigma\; A\; B\_a$가 공집합이 아니라는 것은 동치이다. 예를 들어, a가 b 이하라는 것과, 자연수 n과 a+n=b의 증명의 쌍이 존재한다는 것은 동치이다.
:$a\backslash le\; b\; \backslash iff\; \backslash Sigma\; \backslash mathbb\{N\}\; (\backslash lambda\; n\; \backslash rarr\; a+n=b)$

4. 람다 큐브

헨크 바렌드레흐트는 세 축을 따라 유형 시스템을 분류하는 수단으로 람다 큐브를 개발했다. 결과적으로 큐브 모양의 다이어그램의 8개 모서리는 각각 유형 시스템에 해당하며, 가장 덜 표현적인 모서리에는 단순 유형 람다 계산법이, 가장 표현적인 모서리에는 구성 계산법이 위치한다. 큐브의 세 축은 단순 유형 람다 계산법의 세 가지 다른 증분에 해당한다. 종속 유형의 추가, 다형성의 추가, 그리고 더 높은 Kind 유형 생성자(예를 들어, 유형에서 유형으로의 함수)의 추가가 그것이다. 람다 큐브는 순수 유형 시스템에 의해 더 일반화된다.

헨크 바렌드렉트는 여러 타입 시스템을 3개의 축을 기준으로 분류하는 람다 큐브를 발명했다. 정육면체 형태의 그림에서 8개의 꼭짓점 각각은 타입 시스템에 대응한다. 단순 타입 람다 계산이 표현력이 가장 낮은 꼭짓점에 배치되고, 구성의 계산이 표현력이 가장 높은 꼭짓점에 배치되어 있다. 정육면체의 3개의 축은 각각 단순 타입 람다 계산에 대한 3가지 종류의 다른 확장을 의미한다. 각각, 의존 타입의 추가, 타입 다형성의 추가, 고차원의 카인드를 가진 타입 생성자(예를 들어 타입에서 타입으로의 함수)의 추가이다.

람다 큐브에서 (좁은 의미의) 의존 타입과 다형 타입은 모두 (넓은 의미의) 의존 곱 타입의 특별한 경우로 볼 수 있지만, 값에 대한 양자화를 하는 경우에는 (좁은 의미의) 의존 타입, 타입이나 타입 생성자에 대한 양자화를 하는 경우에는 다형 타입이라고 부르며 구별된다. 람다 큐브에서 카인드(일반적인 타입을 모은 특별한 타입)를 $*$, 초 카인드(카인드를 모은 특별한 타입)를 $\backslash square$로 표기한다. 이때, (좁은 의미의) 의존 타입은 $A:*$ 및 $B:A\backslash to\; *$를 사용하여 구성되는, $\backslash Pi\_\{(x:A)\}\; B(x)$라는 타입이다. 한편, 다형 타입은 $A:\backslash square$ 및 $B:A\backslash to\; *$를 사용하여 구성되는, $\backslash Pi\_\{(x:A)\}\; B(x)$라는 타입이다. 예를 들어, $*:\backslash square$임을 이용하여 $\backslash Pi\_\{(x:*)\}\; B(x)$로 쓴 것은 타입에 대한 양자화를 하는 다형 타입이 된다. 람다 큐브는 순수 타입 시스템에 의해 더욱 일반화된다.

4.1. 람다 큐브의 세 축

헨크 바렌드렉트는 여러 타입 시스템을 3개의 축을 기준으로 분류하는 람다 큐브를 발명했다. 정육면체 형태의 그림에서 8개의 꼭짓점 각각은 타입 시스템에 대응한다. 단순 유형 람다 계산이 표현력이 가장 낮은 꼭짓점에 배치되고, 구성의 계산이 표현력이 가장 높은 꼭짓점에 배치되어 있다. 정육면체의 3개의 축은 각각 단순 타입 람다 계산에 대한 3가지 종류의 다른 확장을 의미한다. 각각, 의존 타입의 추가, 타입 다형성의 추가, 고차원의 카인드를 가진 타입 생성자(예를 들어 타입에서 타입으로의 함수)의 추가이다.

람다 큐브에서 (좁은 의미의) 의존 타입과 다형 타입은 모두 (넓은 의미의) 의존 곱 타입의 특별한 경우로 볼 수 있지만, 값에 대한 양자화를 하는 경우에는 (좁은 의미의) 의존 타입, 타입이나 타입 생성자에 대한 양자화를 하는 경우에는 다형 타입이라고 부르며 구별된다. 람다 큐브에서 카인드(일반적인 타입을 모은 특별한 타입)를 $*$, 초 카인드(카인드를 모은 특별한 타입)를 $\backslash square$로 표기한다. 이때, (좁은 의미의) 의존 타입은 $A:*$ 및 $B:A\backslash to\; *$를 사용하여 구성되는, $\backslash Pi\_\{(x:A)\}\; B(x)$라는 타입이다. 한편, 다형 타입은 $A:\backslash square$ 및 $B:A\backslash to\; *$를 사용하여 구성되는, $\backslash Pi\_\{(x:A)\}\; B(x)$라는 타입이다. 예를 들어, $*:\backslash square$임을 이용하여 $\backslash Pi\_\{(x:*)\}\; B(x)$로 쓴 것은 타입에 대한 양자화를 하는 다형 타입이 된다. 람다 큐브는 순수 타입 시스템에 의해 더욱 일반화된다.

4.2. 일차 의존 타입 이론

순수 일차 종속 타입 시스템 $\backslash lambda\; \backslash Pi$는 LF에 해당하는 것으로, 단순 타입 람다 계산의 함수 공간 타입을 종속 곱 타입으로 일반화하여 얻을 수 있다. 일계 의존형을 가진 $\backslash lambda\; \backslash Pi$형 시스템은 단순 타입 람다 계산의 함수형(화살표형)을 의존 곱형으로 일반화하여 얻을 수 있다. 이는 논리학의 Logical Framework LF(:en:Logical framework#LF)에 해당한다.

4.3. 이차 의존 타입 이론

2차 의존형 시스템 $\backslash lambda\; \backslash Pi\; 2$는 타입 생성자에 대한 양자화를 허용하여 $\backslash lambda\; \backslash Pi$에서 파생된다. 이 이론에서 의존 곱 연산자는 단순 타입 람다 계산의 $\backslash to$ 연산자와 시스템 F의 $\backslash forall$ 바인더를 모두 포함한다.

4.4. 고차 의존형 다형 람다 계산

고차 시스템 $\backslash lambda\; \backslash Pi\; \backslash omega$는 람다 큐브의 네 가지 추상화 형태, 즉 항에서 항으로의 함수, 타입에서 타입으로의 함수, 항에서 타입으로의 함수, 타입에서 항으로의 함수로 $\backslash lambda\; \backslash Pi\; 2$를 확장한다. 이 시스템은 파생물인 귀납적 구성의 계산법이 Coq 증명 보조자의 기반 시스템인 구성의 계산법에 해당한다. 귀납적 구성의 계산법은 Coq가 사용하는 형식 시스템이다.

5. 프로그래밍 언어와 논리학의 동시성

커리-하워드 대응은 형식이 임의로 복잡한 수학적 속성을 표현할 수 있음을 의미한다. 사용자가 형식이 구현(즉, 해당 형식의 값이 존재함)한다는 구성적 증명을 제공할 수 있다면, 컴파일러는 증명을 확인하고 해당 구성을 수행하여 값을 계산하는 실행 가능한 컴퓨터 코드로 변환할 수 있다. 증명 확인 기능은 종속적으로 형식이 지정된 언어를 증명 보조자와 밀접하게 관련시킨다. 코드는 기계적으로 검증된 수학적 증명에서 직접 파생되므로, 코드 생성 측면은 형식적 프로그램 검증 및 증명 동반 코드에 대한 강력한 접근 방식을 제공한다.
커리-하워드 동형 대응에 의해, 아무리 복잡한 수학적 성질도 형을 통해 표현할 수 있다. 만약 사용자가 형이 비어있지 않다(즉, 그 형을 가진 값이 존재한다)는 구성적 증명을 제시할 수 있다면, 컴파일러는 증명의 타당성을 검사하고, 증명의 구성을 추적함으로써 실제로 그 값을 계산할 수 있는 실행 가능한 프로그램 코드를 출력할 수 있다. 이처럼 증명을 검사할 수 있다는 성질 때문에, 의존형을 가진 프로그래밍 언어는 정리 증명 보조 시스템과 밀접한 관계를 갖는다. 코드를 생성할 수 있다는 관점에서, 기계적으로 검증된 수학적 증명으로부터 프로그램 코드를 직접 도출할 수 있기 때문에, 형식적 기법에 의한 프로그램 검증이나 증명 동반 코드에 대한 접근법이 고려된다.

6. 종속 타입을 지원하는 언어 비교

wikitext

커리-하워드 동형 대응에 의해, 아무리 복잡한 수학적 성질도 형을 통해 표현할 수 있다. 만약 사용자가 형이 비어있지 않다 (즉, 그 형을 가진 값이 존재한다)는 구성적 증명을 제시할 수 있다면, 컴파일러는 증명의 타당성을 검사하고, 증명의 구성을 추적함으로써 실제로 그 값을 계산할 수 있는 실행 가능한 프로그램 코드를 출력할 수 있다. 이처럼 증명을 검사할 수 있다는 성질 때문에, 의존형을 가진 프로그래밍 언어는 정리 증명 보조 시스템과 밀접한 관계를 갖는다. 코드를 생성할 수 있다는 관점에서, 기계적으로 검증된 수학적 증명으로부터 프로그램 코드를 직접 도출할 수 있기 때문에, 형식적 기법에 의한 프로그램 검증이나 증명 동반 코드에 대한 접근법이 고려된다.

6.1. 언어별 특징 비교

커리-하워드 동형 대응에 의해, 아무리 복잡한 수학적 성질도 형을 통해 표현할 수 있다. 만약 사용자가 형이 비어있지 않다 (즉, 그 형을 가진 값이 존재한다)는 구성적 증명을 제시할 수 있다면, 컴파일러는 증명의 타당성을 검사하고, 증명의 구성을 추적함으로써 실제로 그 값을 계산할 수 있는 실행 가능한 프로그램 코드를 출력할 수 있다. 이처럼 증명을 검사할 수 있다는 성질 때문에, 의존형을 가진 프로그래밍 언어는 정리 증명 보조 시스템과 밀접한 관계를 갖는다. 코드를 생성할 수 있다는 관점에서, 기계적으로 검증된 수학적 증명으로부터 프로그램 코드를 직접 도출할 수 있기 때문에, 형식적 기법에 의한 프로그램 검증이나 에 대한 접근법이 고려된다.

7. 한국의 의존 타입 연구 및 활용