시스템 F

시스템 F(다형 람다 미적분 또는 2차 람다 미적분)는 형식에 대한 보편적 정량화 메커니즘인 단순 형식 람다 미적분학을 도입하는 형식 람다 미적분이다.시스템 F는 프로그래밍 언어에서 파라메트릭 다형성을 공식화하여 하스켈, ML 등의 언어에 대한 이론적 기초를 형성하고 있으며, 논리학자 장 이브 지라드(1972)와 컴퓨터 과학자 존 C에 의해 독자적으로 발견되었다. 레이놀즈(1974년).

단순히 입력된 람다 미적분학에는 항에 걸친 변수와 이들을 위한 바인더가 있는 반면, 시스템 F에는 유형에 대한 변수와 이들을 위한 바인더가 추가로 존재한다.일례로 신분함수가 어떤 형태든 A → A 형태를 가질 수 있다는 사실은 시스템 F에서 판단으로 공식화된다.

${\displaystyle \vdash \lambda \alpha .\lambda x^{\alpha }x:\all \alpha .\alpha \to \alpha }}$

여기서 $\alpha {\displaystyle }$ ${\displaystyle \alpha }$은(는) 유형 변수다.대문자 $\lambda {\displaystyle \mathrm{}}$ ${\displaystyle \Lambda }$은(는) 값 수준 함수에 사용되는$$ 소문자 $\lambda {\displaystyle }$ ${\displaystyle \lambda }$과는 반대로 형식 수준 함수를 나타내는 데 전통적으로 사용된다$$.(위첨자 $\alpha {\displaystyle }$ ${\displaystyle \alpha}$은 바운드 x가 $\alpha {\displaystyle }$ ${\displaystyle \alpha }$ 형식임을 의미하며$,$ 콜론 뒤의 표현은 앞의 람다 식의 유형이다.)

용어 재쓰기 시스템으로서 시스템 F는 강하게 정상화되고 있다.그러나 시스템 F의 형식 추론(명시 형식 주석 없음)은 해석할 수 없다.Curry-Howard 이소모르피즘에서 System F는 보편적 정량화만을 사용하는 2차 직관논리의 파편에 해당한다.시스템 F는 람다 큐브의 일부로 볼 수 있으며, 종속 유형을 포함한 훨씬 더 표현력이 뛰어난 타입의 람다 캘커리와 함께 볼 수 있다.

지라드에 따르면, 시스템 F의 "F"는 우연히 선택되었다.^[1]

타이핑 규칙

시스템 F의 타이핑 규칙은 다음을 추가하여 간단히 타이핑된 람다 미적분의 타이핑 규칙이다.

${\displaystyle {\frac {\Gamma \vdash M{\mathbin {:}}\forall \alpha .\sigma }{\Gamma \vdash M\tau {\mathbin {:}}\sigma [\tau /\alpha ]}}}$ (1)

${$$M{\mathbin{:}}\모두 \알파 .\sigma }}}($2)

여기서 $where{\displaystyle }$ ,${\displaystyle \tau }$ ${\displaystyle \sigma ,\tau$ $}$이(가) 유형이고$$, $\alpha {\displaystyle }$ ${\$$displaystyle \alpha ~{\text{type}}$은(는) 문맥상$$ $\alpha {\displaystyle }$ ${\displaystyle \text{타입}}$ ${\displaystystyle \alpha}$이(가) 바인딩되어 있음을$$ 나타낸다.첫 번째 규칙은 적용의 법칙이고, 두 번째 규칙은 추상화의 법칙이다.^{[2] [3]}

논리 및 술어

${\displaystyle \mathsf{B}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ e n ${\$ 타입은$$ 다음과 같이 정의된다.$$α${\displaystyle \mathrm{}\alpha }$ ${\displaystyle \to \alpha }$ → α →${\displaystyle \alpha }$ → α → $\displaystyle \all \alpha \to \alpha$ \alpha $}}.$ 여기서 $\alpha {\displaystyle }$ ${\displaypha }$은 유형 변수다.즉: ${\displaystyle \mathsf{B}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ e n ${\$은(는) 유형 α와 유형 α의 두 식을 입력하여 출력하는 모든 함수의 유형이며$$, 유형 α의 식을 생성한다(참고${\displaystyle }$→ ${\displaystyle \to }$을 오른쪽 연관성으로 간주한다$$).

부울 값 $T{\displaystyle \mathbf{}}$ ${\$과($)$ F {\$displaystyle$ \$mathbf${F}에 대한 다음 두 가지 정의가$$ 사용되어 Church 부울런의 정의가 확장된다.

${\displaystyle \mathbf {T} =\Lambda \alpha {.}}\boda x^{\buffer }\bufferda y^{\buffer }{{}}{.}}x}$

${\displaystyle \mathbf {F} =\Lambda \alpha {.}}\boda x^{\buffer }\bufferda y^{\buffer }{{}}{.}y}$

(위의 두 함수는 두 개의 인수가 아닌 세 개의 인수를 필요로 한다는 점에 유의하십시오.후자는 람다 표현이어야 하지만, 첫 번째 표현은 유형이어야 한다.이 사실은 이러한 식의 유형이 α${\displaystyle \mathrm{}\alpha \alpha }$ →${\displaystyle \alpha }$ → α → ${\displaystyle \alpha }$ →${\displaystyle }$α →$$α {\$displaystyle$\$forall$\$알파 .\alpha \to$ \$alpha \};$α를 결합하는 범용 정량자는 람다식 자체에서 알파 를 결합하는 alpha에 해당한다.또한 $B{\displaystyle \mathsf{}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ e$$n {\$displaystyle$ {\$mathsf$ {$Boolean}}$은(는$)$ ${\displaystyle \alpha \alpha }$ → α → ${\displaystyle \alpha }$ →${\displaystyle \alpha }$ → α $\\\$display $style$\ for \$alpha \to \alpha \}$에 대한 편리한 속기법이지만$,$ 시스템 F 자체의 상징은 아니다.Likewise, ${\displaystyle \mathbf {T} }$ and ${\displaystyle \mathbf {F} }$ are also "meta-symbols", convenient shorthands, of System F "assemblies" (in the Bourbaki sense); otherwise, if such functions could be named (within System F), then there would be no need for the lambda-expressive apparatus capable of defining functions 익명으로, 그리고 그러한 제약에 따라 작동하는 고정 포인트 결합기에 대해.

Then, with these two ${\displaystyle \lambda }$-terms, we can define some logic operators (which are of type ${\displaystyle {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}}$):

${\displaystyle {\begin{aigned}\mathrm {AND} &=\lambda x^{Boolean}\mathsf {Boolean}\lambda y^{\mathsf {Boolean}{{Boolean}}}}}{{}}}}}}}}}}}x\,{\mathsf {Boolean}\,y\,\mathbf {F} \\\mathrm {OR} &=\lambda x^{Boolean}\lambda y^{\mathsf {Boolean}}{\mathsf {Boolean}}}{{{{{{boolean}}}}}}}}}}}}{{{{{{{{{boolean}}}}}}x\,{\mathsf {Boolean}\,\mathbf {T} \,y\\\\mathrm {NOT} &=\lambda x^{\mathsf {Boolean}}{{\mathsf}{Boolean}}}}}{{{}}}}}}}}}}}}}}}}}x\,{\mathsf {Boolean}\,\mathbf {F}\,\mathbf {T} \end{igned}}}}}$

Note that in the definitions above, ${\displaystyle {\mathsf {Boolean}}}$ is a type argument to ${\displaystyle x}$, specifying that the other two parameters that are given to ${\displaystyle x}$ are of type ${\displaystyle {\mathsf {Boolean}}}$. As in Church encodings, there is no neea를 위해 d를 구하다IFTHELLSE 함수는 결정 함수로 ${\displaystyle \mathsf{원시}}$ $B{\displaystyle \mathsf{}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ e n ${\${\$mathsf$ {$Boolean}}-$유형$$ 용어를 사용할 수 있다.단, 요청된 경우:

${\displaystyle \mathrm {IFTHENE} =\lambda \alpha .\lambda x^{\lambda y^{\lambda z^{\lambda }{\alpha }.x\alpha yz}$

할 거다.술어는 ${\displaystyle \mathsf{B}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ ${\displaystyle \mathsf{o}}$ e n ${\$ -typed$$ 값을 반환하는 함수다.가장 기본적인 술어는 ISZERO로, 만약 그 주장이 교회 숫자 0인 경우에만$$ $T{\displaystyle \mathbf{}}$ ${\$를) 반환한다.

$\displaystyle \mathrm {ISZERO} =\lambda n^{\all \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha }{{.}n\,{\mathsf {Boolean}\,(\lambda x^{\mathsf {Boolean}){{\mathsf {Boolean}}}{{{.}\mathbf {F}\,\mathbf {T}}$

시스템 F 구조물

시스템 F는 마틴 뢰프의 유형 이론에서 그것과 관련된 재귀적 구조를 자연적으로 내장할 수 있게 한다.추상 구조(S)는 시굴자를 사용하여 생성된다.다음은 다음과 같이 입력된 기능이다.

${\displaystyle K_{}}$ ${\displaystyle {1\mathrm{}}_{}}$→ ${\displaystyle {}_{}}$ ${\displaystyle {2\mathrm{}}_{}}$→ ${\displaystyle \cdots }$→ ${\displaystyle S}$ ${\displaystyle K_{1}\오른쪽$ 화살표 $K_{2}\오른쪽$ 화살표 $\dots \오른쪽$ 화살표 $S}$.

재귀성은 S자체가 ${\$유형 중 하나 내에서 나타날 때 나타나며$,$ 이러한 생성자의 m을 가지고 있으면 다음과 같이 S유형을 정의할 수 있다.

$\dots \rightarrow \rightarrow \lapha .(K_{1}^{m}[\alpha/S]\rightarrow \lapa }}}\rightarrow \rightarrow \rapa }}}}}$

예를 들어, 자연수는 생성자가 있는 유도 데이터 유형 N으로 정의될 수 있다.

${\displaystyle {\begin{aigned}{\mathit {0}&:\mathrm {N} \\mathit {such}&:\mathrm {N} \rightarrow \mathrmatrm {N} \ended}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}$

이 구조에 해당하는 System F 타입은${\displaystyle \mathrm{}\alpha .}$ ${\displaystyle \alpha }$ ${\displaystyle \to }$ (${\displaystyle \alpha }$→${\displaystyle \alpha }$) → ${\displaystyle \alpha }$. → α. α. α$.$ \$displaystyle$\ $forall \alpha \to \alpha \to \alpha$ 이 타입의 조건은 교회 숫자의 타입으로 구성되는데, 이 중 몇 가지는 다음과 같다.

${\displaystyle {\begin{aigned}0&:=\lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha \.x\1\:=\Lambda \lambda x^{\alpha }.\lambda f^{\alpha \to \alpha \fx\\2&:=\lambda \lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)\\3&:=\Lambda \lambda x^{\alpha }.\lambda f^{\required \to \to \f(f(f))\end{aigned}}}$

If we reverse the order of the curried arguments (i.e., ${\displaystyle \forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }$), then the Church numeral for n is a function that takes a function f as argument and returns the n^th power of f.즉, Church numeral은 고차적 함수로서, 단일 인수 함수 f를 취하고, 또 다른 단일 인수 함수를 반환한다.

프로그래밍 언어에 사용

이 글에서 사용된 시스템 F의 버전은 명시적으로 타이핑된 것, 즉 교회 스타일의 미적분학이다.λ 문자에 포함된 타이핑 정보는 타이핑 확인을 쉽게 한다.조 웰스(1994)는 시스템 F의 커리식 변종, 즉 명시적인 타이핑 주석이 없는 것에 대해 유형 확인이 불분명하다는 것을 증명함으로써 "부끄러울 정도로 개방적인 문제"를 해결했다.^[4][5]

웰스의 결과는 시스템 F에 대한 유형 추론이 불가능하다는 것을 암시한다."Hindley-Milner" 또는 단순히 "HM"으로 알려진 시스템 F의 제한은 쉬운 유형의 추론 알고리즘을 가지고 있으며 Haskell 98 및 ML 제품군과 같은 많은 정적으로 타이핑된 기능 프로그래밍 언어에 사용된다.시간이 지남에 따라 HM형 시스템의 제약이 명백해짐에 따라 언어는 그들의 타입 시스템에 대해 보다 표현적인 로직으로 꾸준히 이동해왔다.GHC a Haskell 컴파일러는 HM(2008년 기준)을 넘어 비합성형 균등으로 확장된 시스템 F를 사용한다.^[6] OCaml 유형 시스템의 비 HM 기능에는 GADT가 포함된다.^[7][8]

지라드 레이놀즈 이소모르피즘

2차 직감 논리학에서는 2차 다형 람다 미적분(F2)이 지라드(1972년)에 의해 발견되고 레이놀즈(1974년)에 의해 독자적으로 발견되었다.^[9]지라드는 표현 정리를 증명했다: 2차 직감론적 술어 논리(P2)에서는 자연수에서 총체적으로 증명될 수 있는 자연수까지의 함수들이 P2에서 F2로 투영되는 것을 형성한다.^[9]레이놀즈는 F2의 모든 용어가 논리적 관계 P2에 내장될 수 있는 논리적 관계를 만족한다는 추상화 정리를 증명했다.^[9]레이놀즈는 지라드 투영에 이어 레이놀즈 임베딩이 정체성, 즉 지라드 레이놀즈 이소모르피즘을 형성한다는 것을 증명했다.^[9]

시스템_ω F

시스템 F는 바렌트레트의 람다 입방체의 첫 번째 축에 해당하는 반면, 시스템_ω F 또는 고차 다형 람다 미적분은 첫 번째 축(폴리모르퍼시즘)과 두 번째 축(유형 연산자)을 결합하여 다른, 보다 복잡한 시스템이다.

시스템 F는_ω 시스템 제품군에 따라 귀납적으로 정의될 수 있으며, 여기서 유도는 각 시스템에서 허용되는 종류에 기초한다.

• ${\displaystyle F_{}}$ ${\displaystyle n_{}}$ ${\$는 다음과 같은 종류를 허용한다.
  • ${\displaystyle \star }$ ${\displaystyle \star }($유형) 및
  • ${\displaystyle J}$ ${\displaystyle \Rightarrow }$ ${\displaystyle K}$ ${\displaystyle J\Rightarrow K}$ 여기서$$ $J{\displaystyle }$ ${\displaystyle \in }$ F ${\displaystyle {\mathrm{n}}_{}}$- 1 ${\$ 및$$ $K{\displaystyle }$ ${\displaystyle \in }$ F ${\displaystyle n_{}}${\$displaysty K\in$F_{$$$n}}}($유형별로 함수 종류, 인수 유형이 낮은 순서)

한계에서 시스템 $F{\displaystyle {}_{}}$ ${\displaystyle {\Omega }_{}}$ ${\$을(를) 정의하면 된다.

• ${\displaystyle F_{\omega}={\underset {1\leq i}{\\bigcup }F_{i}}}}$

즉, F는_ω 인수(및 결과)가 임의의 순서로 될 수 있는 유형에서 유형까지 기능을 허용하는 시스템이다.

F는_ω 이러한 매핑에서 인수의 순서에 제한을 두지 않지만, 이러한 매핑에 대한 인수의 우주를 제한한다는 점에 유의하십시오. F는 값이 아닌 유형이어야 한다.${\displaystyle }$ F는_ω 값에서 값까지의 매핑([\$displaystyle \lambda }$ 추상화$$], 유형에서 $$으로 매핑$([\displaystyle \Lambda }$ 추상화$$) 및 $$에서 유형으로 매핑$([\displaystyle \lambda }$ } } 추상화$$)을 허용하지만 값에서 매핑을 허용하지 않는다.l 유형)

참고 항목

• 실존적 유형 - 보편적 유형의 실존적 수량화 상대적 유형
• 시스템 F_<: — 하위 타이핑으로 시스템 F를 확장
• 시스템 U

메모들

참조

추가 읽기

• Pierce, Benjamin (2002). "V Polymorphism Ch. 23. Universal Types, Ch. 25. An ML Implementation of System F". Types and Programming Languages. MIT Press. pp. 339–362, 381–388. ISBN 0-262-16209-1.

외부 링크

Wikibooks에는 다음과 같은 주제의 책이 있다.하스켈

• Franck Binard의 시스템 F 요약.
• System_ω F: Greg Morrisett의 현대 컴파일러의 일꾼