순수형제

증명 이론과 유형 이론으로 알려진 수학 논리의 가지에서, 이전에 일반화된 유형 시스템(GTS)으로 알려진 순수 유형 시스템(PTS)은 이들 중 어느 것에도 임의의 수의 종류와 의존성을 허용하는 타입 람다 미적분학의 한 형태다.이 프레임워크는 두 가지 종류만 있으면 큐브의 모든 모서리가 PTS의 인스턴스로 표현될 수 있다는 점에서 바렌트레트의 람다 큐브를 일반화한 것으로 볼 수 있다.^[1][2]사실, 바렌트레트(1991)는 이 환경에서 자신의 큐브를 틀에 넣었다.^[3]순수형 시스템은 구성의 미적분처럼 형식과 용어의 구분을 모호하게 하고 형식 계층을 붕괴시킬 수 있지만, 일반적으로는 그렇지 않다. 예를 들어 단순하게 타이핑된 람다 미적분학은 용어에 의존하는 용어만을 허용한다.

순수형 시스템은 스테파노 베라르디(1988년)와 얀 테루(1989년)가 독자적으로 도입했다.^[1][2]바렌트레트는 후속 논문에서 그것들을 상세히 논했다.^[4]베라르디는 박사학위 논문에서 람다 큐브와 유사한 건설적 로직의 큐브를 정의했다(^[5]이 사양들은 의존성이 없다).후에 이 큐브의 수정은 Geuvers에 의해 L-큐브라고 불리게 되었는데, 그는 박사 논문에서 Curry-Howard의 서신을 이 설정으로 확장시켰다.^[6]이러한 사상을 바탕으로 바르테 등은 이중 부정 연산자를 추가하여 고전적인 순수형 시스템(CPTS)을 정의했다.^[7]마찬가지로, 1998년에 Tijn Borghuis는 모달 순수형 시스템(MPTS)을 도입했다.^[8]Roorda는 기능 프로그래밍에 순수형 시스템의 적용을 논의했고, Roorda와 Jeuring은 순수형 시스템에 기반한 프로그래밍 언어를 제안했다.^[9]

람다 큐브의 시스템은 모두 강하게 정상화되고 있는 것으로 알려져 있다.일반적으로 순수한 타입 시스템은 필요하지 않다. 예를 들어 Girard의 역설에서 나온 System U는 그렇지 않다. (확실히, Girard는 "유형이 형태를 이루고 있다"라는 문장을 표현할 수 있는 순수한 시스템을 발견했다.)더욱이 강하게 정상화되지 않고 있는 순수형 시스템의 알려진 모든 예는 심지어 (약하게) 정상화가 되지 않는다: 그것들은 정형화되지 않은 람다 미적분처럼^{[citation needed]} 정상적인 형태를 가지고 있지 않은 표현들을 포함하고 있다.PTS의 정상화가 항상 유효한지 여부, 즉 PTS의 정상화가 항상 강력한 정상화 속성을 가지는지는 현장에서 중요한 개방적인 문제다.이것은 바렌트레트-지우버스-클롭 추측^[10](Henk Barendregt, Herman Geuvers, Jan Willem Klop의 이름을 따서 명명)으로 알려져 있다.

정의

A pure type system is defined by a triple ${\textstyle ({\mathcal {S}},{\mathcal {A}},{\mathcal {R}})}$ where ${\textstyle {\mathcal {S}}}$ is the set of sorts, ${\textstyle {\mathcal {A}}\subseteq {\mathcal {S}}^{2}}$ is the set of axioms, and ${\textsty$$le {\mathcal{R}\subseteq {\mathcal{S}^{3}}}$은(는) 규칙 집합이다.pure type 시스템에 입력하는 것은 다음 규칙에 의해 결정되며, $여기$서$$s {\$textstyle$ s$}$은(는) 모든 종류의 것이다$$.^[4]

${\displaystyle {\frac {(s_{1},s_{2})\in {\mathcal {A}{\\dash s_{1}:s_{2}}\quad {\text{(axiom)}}}$

${\displaystyle {\frac {\\Gamma \vdash A:s\quad x\notin {\text{dom}(\Gamma )}{\Gamma ,x:A\vdash x::}{\text{dom}}}{\Gamma}}}}{\Gamma:A}\quad {\text{(시작)}}}$

${\displaystyle {\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s\quad x\notin {\text{dom}(\Gamma )}{\Gamma ,x:C\vdash A:B}}\quad{\text{(취약)}}}$

${\displaystyle {\frac {\gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}\quad(s_{1},s_{3})\quad(s_{1},s_{3})\mathcal {R}{\\\\mathmathma \vdash \vdash \pi x:A}}}}}}B:s_{3}}\quad {\text{(제품)}}}$

${\displaystyle {\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash a:A}{\Gamma \vdash Ca:B[x:=a]}\quad {\text{(응용프로그램)}}}$

${\displaystyle {\frac {\Gamma ,x:A\vdash b:B\quad \Gamma \vdash \Pi x:A.B:s}{\Gamma \vdash \lambda x:A.b:\Pi x:A.B}}\quad {\text{(추정)}}}$

${\displaystyle {\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(변환)}}}$

구현

다음 프로그래밍 언어는 순수형 시스템을 가지고 있다.^{[citation needed]}

• SAGE ^[11]
• 야로
• 헨크 2000

참고 항목

• 시스템 U – 일관되지 않은 PTS의 예
• λ μ-미적분은 CPTS와는 다른 제어 접근법을 사용한다.

메모들

참조

추가 읽기

• Schmidt, David A. (1994). "§ 8.3 Generalized Type Systems". The structure of typed programming languages. MIT Press. pp. 255–8. ISBN 0-262-19349-3.

외부 링크

• 순수형 시스템(nLab)
• Jones, Roger Bishop (1999). "Pure Type Systems overview".