카파 미적분학

수학 논리학, 범주 이론, 컴퓨터 과학에서 카파 미적분은 1차 함수를 정의하는 공식적인 시스템이다.

람다 미적분과 달리 카파 미적분은 고차 함수가 없으며, 그 함수는 1등급 객체가 아니다.카파-미적분은 "타입 람다 미적분학의 1차적인 파편을 개조한 것"^[1]으로 볼 수 있다.

기능이 1등급 객체가 아니기 때문에 카파 미적분 표현 평가에는 폐쇄가 필요하지 않다.

정의

아래의 정의는 하세가와 205쪽과 207쪽에 있는 도표에서 개작한 것이다.^[1]

문법

카파 미적분은 아래 문법에 의해 주어지는 유형과 표현으로 구성된다.

$\displaystyle \tau =1\mid \tau \tau \tots }$

${\displaystyle e=x\mid id_{\tau id_}\mid !_{\tau }}\mid \mid \tau }(e)\mid e\mid \cappa x:1{\to}\to.e}$

바꾸어 말하면, 환언하면

• 1은 유형이다.
• $\tau {\displaystyle {}_{}}$ 1${\$} 및$$ ${\displaystyle {2\mathrm{}}_{}}$ 2$${\$displaystyle$\$tau$$$$_{1}\times \tau _{2$}}:$$if$$$$ ${\displaystyle {1\mathrm{}}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle {2\mathrm{}}_{}}$ ${\$\tau _{1}\2}}: 유형이다.
• 모든 변수는 표현식이다.
• τ가 유형인 경우 i ${\displaystyle {}_{}}$ ${\displaystyle {\tau }_{}}$ ${\$은(는) 표현이다$$.
• 만약 τ이 타입이라면${\displaystyle {}_{}}$!${\displaystyle {\tau }_{}}$ ${\$은 표현이다$$.
• τ가 유형이고 e가 표현인 경우, ${\displaystyle {\tau }_{}}$(${\displaystyle e}$ ) ${\displaystyle \operatorname {relipt} _{\tau }(e)}$은 표현이다$$.
• $e{\displaystyle {}_{}}$$$ ${\displaystyle {1\mathrm{}}_{}}$ ${\$및 e$$ ${\displaystyle {2\mathrm{}}_{}}$ ${\$ 식인 경우 $e{\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}{}_{}}$ e ${\displaystyle {2\mathrm{}}_{}}$ ${\$}\$circle e_{2}}:$ 식인$$ 경우
• x가 변수인 경우 τ은 유형이고 e는 표현식인 경우 ${\displaystyle \kappa }$ x${\displaystyle }$: ${\displaystyle 1\mathrm{}}$→ ${\displaystyle \tau .}$ ${\displaystyle e}$ ${\displaystyle \cappa x{:}1{\to }\tau \;;$$\;e}$은(는) 표현식이다.

:${\displaystyle 1}$→ ▼ ${\displaystyle :1$$\to }\tau }$ 및 ${\displaystyle \mathrm{id}}$, ! 및 리프트 ${\displaystyle \operatorname {lift}}$의 첨자는 컨텍스트에서 명확하게 결정할 수 있을 때 생략되기도$$ 한다.

대등사치는 흔히 ${\displaystyle \mathrm{리프트}}$ ${\displaystyle \operatorname {lift}$과$($와) 구성의 조합으로 사용된다.

${\displaystyle e_{1}e_{2}\\\overset {\covername {def}{}}{=}}\{1}\reftname \reft}(e_{2})}$

타이핑 규칙

여기서는 단순 타이핑된 람다 ${\displaystyle \mathrm{미적분학}}$과의 비교를 용이하게 하기 위해 가상의 판단보다는 시퀀스( ${\displaystyle \gamma }$ ${\displaystyle \{}$ {${\displaystyle }${ \$$\$displaystyle \Gamma \vdash$e:\$tau$ $\})$를 사용한다.이를 위해서는 하세가와에 나타나지 않는 추가 Var 규칙이 필요하다.^[1]

카파 미적분학에서 표현식은 출처의 유형과 대상의 유형이라는 두 가지 유형을 가진다.표기법 $e{\displaystyle }$ :${\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$→ ${\displaystyle \tau {}_{}}$ ${\displaystyle {2\mathrm{}}_{}}$ ${\$$$${2}}:$ 식 e가 소스 유형 $\tau {\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}${\$displaystyle${\$tau _{$1$}}$ 및 대상 ${\displaystyle {유형\mathrm{}}_{}}$ $\tau {\displaystyle {}_{}}$ 2$${\$displaystystyle {\{\{\}$을 $나타내는$ 데 사용된다$.$

카파 미적분학의 식은 다음 규칙에 따라 유형이 할당된다.

${\displaystyle {x{:}}{{\to }\tau \\\\\Gamma } \over {\Gamma \\dash x:1{\to }\tau }}}}}}$	(Var)
${\dash id_{\tash id_}\;:\;\\tau \to \to \tau }}}} 이상 \displaystyle {}}}}$	(Id)
${\displaystyle {}\\vdash !_{\tau }\;:\;\tau \to:1}} 이상$	(뱅)
${\displaystyle {\Gamma \vdash e_{1}{:}\tau _{1}{\to }\tau _{2}\;\;\\\\\\\\\\Gamma \vdash e_{2}{:}\tau _{2}{\to }\tau _{3}}{3}} \\\Gamma \vdash e_{2}\circ e_{1}:\tau _{1}{1}\to }}}}}}}}}}}}$	(Comp)
${\displaystyle {\gamma \vdash e{:}{{}\to }\\tau_{liff}_{\tau_{2}}(e)\\\\to(\tau _{1}\times \tau_{{}}}}}}}}}}}이상 \}$	(리프트)
${\displaystyle {\Gamma ,\;x{:}1{\to }\tau _{1}\;\vdash \;e:\tau _{2}{\to }\tau _{3}} \over {\Gamma \vdash \kappa x{:}1{\to }\tau _{1}\,.\,e\;:\;\tau _{1}\times \tau _{2}\to \tau _{3}}}$	(카파)

바꾸어 말하면, 환언하면

• Var: $x{\displaystyle }$: ${\displaystyle 1}$→ ${\displaystyle x:1\to }\tau }$을(를) $가정$하면 ${\displaystyle \mathrm{x}}$: 1${\displaystyle }$→ → ${\displaystyle$x:1${\to }\tau }$로 결론을 내릴 수 있다$$.
• ID: 모든 유형 τ에 대해 $i{\displaystyle }$ ${\displaystyle {}_{}}$ ${\displaystyle \tau }$ :${\displaystyle }$: → → ${\displaystyle id_{\tau }:\tau {\to}\tau }$
• Bang: 모든 유형 τ, !${\displaystyle {}_{\tau }}$ :${\displaystyle {}_{}\tau }$→ ${\displaystyle 1\mathrm{}}$ ${\displaystyle !_{\tau }:\tau {\to }1$}
• Comp: ${\displaystyle {e\mathrm{}}_{}}$ $1{\displaystyle {}_{}}$ ${\$}의 대상 유형이 $e{\displaystyle {}_{}}$ 2 ${\$$1$}의 소스 유형과$$ 일치하는$$ 경우$$, e ${\displaystyle {1\mathrm{}}_{}}${\$displaystyle e_{$2$}\circircle e_{1$}의 소스 유형 및 $e{\displaystyle {}_{}}$ 2 ${\$}의 대상 유형을 사용하여$$ e ${\displaystyle {2\mathrm{}}_{}}$${\displaystyle {}_{}}$emption $e{\displaystyle {}_{}}$ 2 emption e ${\displaystyle 1_{}}$을 구성할 수 있다.$$
• Lift: if ${\displaystyle e:1{\to }\tau _{1}}$, then ${\displaystyle \operatorname {lift} _{\tau _{2}}(e):\tau _{2}{\to }(\tau _{1}\times \tau _{2})}$
• Kappa: if we can conclude that ${\displaystyle e:\tau _{2}\to \tau _{3}}$ under the assumption that ${\displaystyle x:1{\to }\tau _{1}}$, then we may conclude without that assumption that ${\displaystyle \kappa x{:}1{\to }\tau _{1}\,$$.\,e\;:\;\tau _{1}\reason \tau _{2}\to \tau _{3}}}$

이퀄리티스

카파 미적분은 다음과 같은 동일성을 준수한다.

• 중립성:If ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$ then ${\displaystyle f{\circ }id_{\tau _{1}}=f}$ and ${\displaystyle f=id_{\tau _{2}}{\circ }f}$
• 연관성:If ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$, ${\displaystyle g:\tau _{2}{\to }\tau _{3}}$, and ${\displaystyle h:\tau _{3}{\to }\tau _{4}}$, then ${\displaystyle (h{\circ }g){\circ }f=h{\circ }(g{\circ }f)}$.
• 종단성:${\displaystyle f\mathrm{}}$: ${\displaystyle \tau }$→ 1 ${\displaystyle$ f${:$$}\tau {\to }1}$ 및$$ $g{\displaystyle }$: ${\displaystyle \tau \mathrm{}}$→ 1 ${\displaystyle g{:$$}\tau {\to }1}$ $다음$ f${\displaystyle }$= ${\displaystyle g}$ ${\displaystyle f=g}$
• 리프트 감소: ${\displaystyle (\kappa x.f)\rettname {lift} _{\tau }(c)=f[c/x]}}$
• 카파-축소: ${\displaystyle \kappa }$ x${\displaystyle }$.${\displaystyle }$( ${\displaystyle h}$ ${\displaystyle \circ }$ ${\displaystyle {\mathrm{리프트}}_{}}$ ${\displaystyle {\tau }_{}{}_{}}$ ( ${\displaystyle x}$)${\displaystyle }$= ${\displaystyle h}$ ${\displaystyle \kappa$ x$.(h\circle \operatorname {lift} _{\tau$}($x)$$=h}$ x가 h에서 자유롭지 않은 경우$$

마지막 두 개의 동일성은 미적분학의 축소 규칙으로, 왼쪽에서 오른쪽으로 다시 쓴다.

특성.

유형 1은 단위 유형으로 간주할 수 있다.따라서, 인수 유형이 같고 결과 유형이 1인 두 함수는 모두 같아야 한다. 유형 1의 값이 하나뿐이므로 두 함수는 모든 인수(터미널성)에 대해 해당 값을 반환해야 한다.

유형 $1{\displaystyle \mathrm{}}$→ ${\displaystyle \tau }$ ${\displaystyle 1{\to }\tau }$을(를) 가진 표현은 "정수" 또는 "접지 유형"의 값으로 볼 수 있다$$. 이는 1이 단위 유형이기 때문에 이 유형으로부터의 함수는 반드시 일정한 함수이기 때문이다.카파 규칙은 추상화하는 변수가 일부 τ에 대해$$ $유형{\displaystyle \mathrm{}}$ 1${\displaystyle }$→ $→[\displaystyle$ 1${\to }\tau }}$을(를) 갖는 경우에만 추상화를 허용한다는 점에 유의하십시오.이것은 모든 기능이 일차적으로 이루어지도록 하는 기본적인 메커니즘이다.

범주형 의미론

카파 미적분은 문맥적으로 완전한 범주의 내부 언어로서 의도되었다.

예

다중 인수가 있는 식에는 "우측 불균형" 이진 트리가 있는 소스 유형이 있다.예를 들어, 유형 A, B, C의 세 개의 인수를 갖는 함수 f와 결과 유형 D는 유형을 갖는다.

${\displaystyle f:A\time (B\time (C\time 1)\to D}$

If we define left-associative juxtaposition ${\displaystyle f\;c}$ as an abbreviation for ${\displaystyle (f\circ \operatorname {lift} (c))}$, then – assuming that ${\displaystyle a:1{\to }A}$, ${\displaystyle b:1{\to }B}$, and ${\displaystyle c:1{\to }C}$ –다음 기능을 적용할 수 있다.

${\displaystyle f\;a\;b\;c\;:\;1\to D}$

${\displaystyle b}$ ${\displaystyle c}$ ${\displaystyle f\;a\;b\;c}$이라는 표현식은 소스 유형 1을 가지기$$ 때문에 "접지 값"이며 다른 함수에 대한 인수로 전달될 수 있다.${\displaystyle g}$: (${\displaystyle D}$ ${\displaystyle \times }$ E${\displaystyle }$)${\displaystyle }$→ F ${\displaystyle$ g$:(D\times$ E$){\to }F$

$(\displaystyle g\;(f\;a\;b\;c)\;:\;E\to F}$

람다 미적분학의$$ $A{\displaystyle }$→${\displaystyle }$(${\displaystyle B}$→${\displaystyle }$( ${\displaystyle C}$ → D )$daystyle A{\to }(B{\to })(C{\to }D)}}$의 커스터드 함수처럼 부분 적용이 가능하다.

$디스플레이 스타일 f\;a\;:\;B\time (C\time 1)\to D}$

그러나 상위 유형(예: (${\displaystyle \tau }$ →${\displaystyle \tau }$)${\displaystyle }$→ ${\displaystyle \tau }$ ${\displaystyle (\tau {\to }\tau ){\to }\tau$ $\})$은 관련되지 않는다.f a의 source type이 1이 아니기 때문에 지금까지 언급된 가정에서는 다음 식을 제대로 형식화할 수 없다는 점에 유의한다.

$([\displaystyle h\;(f\;a)}$

연속적인 애플리케이션은 복수의 인수에 사용되기 때문에, 그 타이핑을 결정하기 위해 함수의 정확성을 알 필요는 없다. 예를 들어, 만약${\displaystyle \mathrm{우리}}$가 c${\displaystyle }$: ${\displaystyle 1}$ → C$${\$displaystyle c:$1{\$to }C}$라고 알고 있다면, 그 표현은 다음과 같다.

j c

j가 타입을 가지고 있는 한 잘 정돈되어 있다.

${\displaystyle (C}$ ${\displaystyle \times }$ ${\displaystyle \alpha }$)${\displaystyle }$→ ${\displaystyle \beta }$ ${\displaystyle (C\times \alpha ){\to }\beta }$일부 α에 대해$$

그리고 β. 이 속성은 표현의 주성형을 계산할 때 중요한데, 형식의 문법을 제한하여 활자 람다 캘커리에서 고차 함수를 제외하려고 할 때 어려울 수 있다.

역사

바렌트레트는 원래 결합 대수라는 맥락에서 "기능적 완전성"이라는 용어를 도입했다^[2].카파 미적분은 임의의 범주에 대해 기능적 완전성의 적절한 아날로그를 공식화하려는 람베크의^[3] 노력에서 생겨났다(헤르미다와 제이콥스,^[4] 섹션 1 참조).하세가와는 후에 카파 미적분을 자연수에 대한 산술과 원시 재귀 등을 포함한 사용 가능한 프로그래밍 언어로 개발했다.^[1]화살에 대한 연결은 나중에 파워, 티에일레케 등에 의해 조사되었다^[5].

변형

선형, 아핀, 순서형 등 하위구조 유형을 가진 카파 미적분학 버전을 탐구할 수 있다.이러한 확장자는${\displaystyle {}_{}}$!${\displaystyle {\tau }_{}}$ ${\$ 식을$$ 제거하거나 제한해야 한다.이러한 상황에서 × 타입 오퍼레이터는 진정한 데카르트 제품이 아니며, 이를 명확히 하기 위해 일반적으로 ⊗라고 쓰여 있다.

참조