구조연산

수학 논리와 컴퓨터 과학에서, 구성 미적분(CoC)은 티에리 코캉에 의해 만들어진 유형 이론이다.이것은 입력된 프로그래밍 언어이자 수학의 건설적인 기초가 될 수 있습니다.이 두 번째 이유로 CoC와 그 변형은 Coq와 다른 입증 보조자들의 기초가 되었다.

그것의 변형들 중 일부는 귀납적^[1] 구성의 미적분, 귀납적 구성의 미적분, 그리고 귀납적 구성의 서술적 미적분을 포함한다.

일반적인 특징

CoC는 티에리 코캉이 최초로 개발한 고차형 람다 미적분이다.그것은 바렌드레그트의 람다 큐브의 꼭대기에 있는 것으로 잘 알려져 있다.CoC 내에서 항간, 항간, 항간, 유형간 및 항간 함수를 정의할 수 있습니다.

CoC는 매우 정규화되어 ^[2]있기 때문에 일관성이 있습니다.괴델의 불완전성 정리에 따르면 CoC ^{[citation needed]}자체에서 일관성을 증명하는 것은 불가능하다.

사용.

CoC는 Coq 인증 보조와 함께 개발되었습니다.이론에 특징이 추가됨에 따라(또는 가능한 부채가 제거됨) Coq에서 사용할 수 있게 되었습니다.

CoC의 변형은 Matita와 같은 다른 입증 보조에 사용됩니다.

구성 미적분의 기초

구성 미적분은 카레-하워드 동형사상의 확장으로 간주될 수 있다.Curry-Howard 동형사상은 단순 유형화된 람다 미적분의 용어를 직관적 명제 논리학의 각 자연 추론 증거와 연관시킨다.구성 미적분은 이 동형성을 수량화된 진술의 증명을 포함하는 완전한 직관적 술어 미적분의 증명으로 확장합니다.

조건.

구성 미적분에서의 용어는 다음 규칙을 사용하여 구성됩니다.

• ${\displaystyle \mathbf{T}}${\$displaystyle \mathbf {T}}$는 용어(타입이라고도 함)입니다.
• ${\displaystyle \mathbf{P}}${\$displaystyle \mathbf {P}}$는 용어(프롭이라고도 하며 모든 명제의 유형)이다.
• 변수(${\displaystyle ,}$ ${\displaystyle y,}$ $…(\style$ x,$y,\ldots$는 용어입니다.
• A$(\displaystyle$ A$)$와 B$(\displaystyle$ B$)$가 용어인 $경우{\displaystyle }$ (${\displaystyle A}$B$)(\displaystyle(AB$도${\displaystyle }$용어입니다.
• A$(\displaystyle$ A$)$와 B$(\displaystyle$ B$)$가 $항이고{\displaystyle }$ x$(\displaystyle$ x$)$가 변수인 $경우{\displaystyle }$ 다음 항도 있습니다.
  • $displaystyle$$A$$B$
  • $displaystyle (\forall$$B$

즉, BNF에서 구문은 다음과 같습니다.

$\displaystyle e:=\mathbf {T} \mid \mathbf {P} \mid x\mid e,e\mid \mid \mad da x scmathbin {:} e:\mid \forall xcathbin {:} e.$

구성 미적분에는 5종류의 객체가 있습니다.

1. 증명, 즉 명제 유형의 용어이다.
2. 명제(소형이라고도 함
3. 명제를 반환하는 함수인 술어
4. 술어 유형인 ${\displaystyle \mathbf{}}$ 유형$($\mathbf ${P}$은 대형 유형의 예임)
5. ${\displaystyle \mathbf{T}}$\$displaystyle \mathbf {T}$ 자체$$, 대형 활자의 유형입니다.

판단

구성 미적분을 통해 타이핑 판단을 증명할 수 있습니다.

${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}$

그 말은 그 암시로 해석될 수 있죠

$변수{\displaystyle {}_{}}$ ${\displaystyle {x\mathrm{}}_{}}$1, $…({displaystyle x_{1$},$x_{2$},\ldots$})$가 각각 ${\displaystyle {유형\mathrm{}}_{}}$ ${\displaystyle {}_{}{}_{}{A2}_{}}$인$경우$$t{\displaystyle }$$(\displaystyle$ t)는 유형$$B$(\displaystyle$$$B$)$입니다.

구성 미적분에 대한 유효한 판단은 일련의 추론 규칙에서 도출할 수 있다.다음에서는 유형 할당의 시퀀스를 의미하기 위해 $(\displaystyle \Gamma)$을 사용합니다.${\displaystyle {}_{}{}_{}}$1 : ${\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$,${\displaystyle {}_{}{x\mathrm{}}_{}}$2 : ${\displaystyle {A\mathrm{}}_{}}$ 2, ${\displaystyle {}_{}}$(\$displaystyle x_{1$} $:$$A_{1},x_{2}:$$A_{2},\ldots$ $\}$ ;${\displaystyle A,}$ B${\displaystyle ,}$ $,$ ${\displaystyle D}$(\$displaystyle$ A$, B, C$,$$D), $K$(\displaystyle K$,$ L$)는$P$$$(\$ \$mathbf$$${$P$$})$ $T(\$displaystyle \$mathbf$${\displaystyle }${${\displaystyle T}$$\})$ 중 $하나$를 $의미$합니다$.$자유 $변수{\displaystyle }$x(\$displaystyle$ x$)$에 대해 B$(\displaystyle$ B$)$라는 용어를 사용합니다.

추론 규칙은 다음 형식으로 작성됩니다.

$(Displaystyle)B}{\Gamma'\vdash C:D}}}$

즉,

${\displaystyle \gamma }$A${\displaystyle }$:$$ \ $displaystyle$\ $Gamma$\$vdash$A :$B}$는 유효한 판단이며, ${\displaystyle \mathrm{so}}$ $C{\displaystyle {\mathrm{}}^{}}$: ${\displaystyle D}$\ $displaystyle$\ $Gamma$' \ $vdash$C :$D}$

구성 계산의 추론 규칙

1. ${\displaystyle \frac{\gamma \mathbf{}}{}}$P${\displaystyle \frac{}{}}$: ${\displaystyle \frac{T\mathbf{}}{}}$\ $displaystyle {{ }$ \$over$ \ $Gamma$\ $vdash$\$mathbf${$P }$ : \ $mathbf${$T }$ }

2. ${\displaystyle \frac{\gamma 、}{}}$ x${\displaystyle \frac{}{}}$: A 、 ${\displaystyle \frac{\gamma 、}{}}$ : x :$$ \ $display$ style ${{ } over$ \ $Gamma , x$ : $A$, \ $Gamma$' \ $vdash$x :$A}}}$

3. ${\displaystyle \frac{\mathrm{gam}A}{}}$: K ${\displaystyle \frac{、x}{}}$ : ${\displaystyle \frac{A}{}}$ ${\displaystyle \frac{、B}{}}$ : ${\displaystyle \frac{L}{}}$ (${\displaystyle \frac{\mathrm{}x}{}}$x :${\displaystyle \frac{A}{}}$ .${\displaystyle \frac{}{}}$B${\displaystyle \frac{}{}}$) :$$ \ $display$ \ $style$\$Gamma \ vdash$A :$K$ \ $qad$\ $Gamma$ , x :$A$ \ $vdash$ B $:$ L :$Over$ \$Gamma$ :$B) : L}}}$

4.${\displaystyle \frac{\gamma }{}}$ ${\displaystyle \frac{A}{}}$ : K ${\displaystyle \frac{、}{}}$x : ${\displaystyle \frac{A、}{}}$ ${\displaystyle \frac{N}{}}$ : B ${\displaystyle \frac{\mathrm{}}{}}$ (${\displaystyle \frac{x}{}}$ x ${\displaystyle \frac{:A}{}}$ .${\displaystyle \frac{N}{}}$)${\displaystyle \frac{}{}}$: (${\displaystyle \frac{\mathrm{}x}{}}$x : ${\displaystyle \frac{A}{}}$. ${\displaystyle \frac{B}{}}$ ) \$display$ style \ $Gamma$\ $K$\ $q quad$ \$Gamma$ ,$B :$ \ $Dash$ :$(N):(모두 x:$$A).$$B)}}}}$

5. $\gamma {\displaystyle \frac{\mathrm{}M}{}}$: (${\displaystyle \frac{\mathrm{}x}{}}$x :${\displaystyle \frac{A}{}}$ .${\displaystyle \frac{B}{}}$ )${\displaystyle \frac{n}{}}$ N${\displaystyle \frac{}{}}$: ${\displaystyle \frac{A}{m}}$ M${\displaystyle \frac{N}{}}$ :${\displaystyle \frac{B}{}}$ [ ${\displaystyle \frac{x}{}}$ : ${\displaystyle \frac{=N}{}}$](\ $display$style \ $Gamma$\ $vdash$ M : (\$for all x:$$A$)$B) \qquad \qquad \Gamma \vdash N:A \over {Gamma \vdash MN:B [x:=N]}}$

6. ${\displaystyle \frac{\gamma }{}}$M${\displaystyle \frac{}{}}$: ${\displaystyle \frac{A}{}}$ ${\displaystyle \frac{{}_{}}{}}$ ${\displaystyle \frac{{}_{}}{}}$ B ${\displaystyle \frac{\mathrm{}}{}}$B${\displaystyle \frac{}{}}$: ${\displaystyle \frac{K}{}}$ ${\displaystyle \frac{⊢M}{}}$ :$$ \ $display$style \ $Gamma$\$vdash$M :$A\qquad \qquad A=_{\beta }B\qquad \qquad \Gamma \vdash B:K \over \Gamma \vdash M:$$B}}}$

논리 연산자의 정의

구성 계산에는 기본 연산자가 거의 없습니다. 제안을 형성하는 유일한 논리 연산자는 $"\displaystyle\forall$입니다. 단, 이 연산자는 다른 모든 논리 연산자를 정의하기에 충분합니다.

${\displaystyle\array\cclllA 오른쪽 화살표 B&\equiv &\forall x:A.B&(x\notin B)\\A\wedge B&\equiv&\forall C:\mathbf {P}. (A\오른쪽 화살표 B\오른쪽 화살표 C\\\)A\veee B&\equiv &\forall C:\mathbf {P} . ( A \ Rightarrow C ) \ Rightarrow ( B \ Rightarrow C ) \ Rightarrow C & \ neg A & \ equiv & \ \ \ \ \ \ \ \ mathbf { P （ \ A \ Rightrow C ） 。B&\equiv &\forall C:\mathbf {P} . (forall x:A).(B\오른쪽 화살표 C)\오른쪽 화살표 C&\end {array}}$

데이터 유형의 정의

컴퓨터 공학에서 사용되는 기본 데이터 유형은 구성 미적분 내에서 정의할 수 있습니다.

부란스

$\displaystyle \forall A:\mathbf {P}.A\오른쪽 화살표 A\오른쪽 화살표 A}$

내추럴

$\displaystyle \forall A:\mathbf {P}.(A\오른쪽 화살표 A)\오른쪽 화살표(A\오른쪽 화살표 A)}$

$제품{\displaystyle }$A × $(표시 스타일$ A$\times$ B$)$

${\displaystyle A\wedge B}$

분리 $유니언{\displaystyle }$A +$$ {$style$A + $B}$

$(\displaystyle A\veee B)$

Boulans 및 Naturals는 Church 인코딩과 동일한 방법으로 정의됩니다.그러나 명제의 확장성과 무관성의 ^[3]증명에서 추가적인 문제가 발생한다.

「 」를 참조해 주세요.

• 순수형 시스템
• 람다 입방체
• 시스템 F
• 종속형
• 직관적 유형 이론
• 호모토피형 이론

레퍼런스