유형 규칙

형식 이론에서 형식 규칙은 형식 시스템이 형식을 통사적 구조에 할당하는 방법을 설명하는 추론 규칙이다.이러한 규칙은 프로그램이 잘 타이핑되었는지와 어떤 유형 식이 있는지 확인하기 위해 유형 시스템에 의해 적용될 수 있다.형식 규칙의 사용에 대한 프로토타입적인 예는 단순 타이핑된 람다 미적분학에서 형식 추론을 정의하는 데 있는데, 이것은 데카르트 폐쇄 범주의 내부 언어다.

표기법

▼ $유형{\displaystyle }${\$displaystyle \tau$}의 e$${\$displaystyle e}$ 식이 $e{\displaystyle :}$ ${\displaystyle \tau }$ ${\displaystyle e\$로 기록됨$$!$:\!\tau$ $\}.$ 타이핑 환경은 $\gamma {\displaystyle \mathrm{}}$ ${\displaystyle \Gamma }$로 쓰여 있다$.$ 추론 표기법은 속편과 추론 규칙의 일반적인 것으로 다음과 같은 일반 형식을 가지고 있다.

${\displaystyle {\frac {\Gamma _{1}\vdash e_{1}\!:\!\tau _{1}\quad \cdots \quad \Quad \Quad \Gamma _{n}\vdash e_{n}\!:\!\tau _{n}{\감마 \vdash e\!:\!\tau }}$

라인 위의 순서는 규칙이 적용되기 위해 충족되어야 하는 전제로서, 결론은 라인 아래의 순서가 된다.${\displaystyle {이}_{}}$는 e i {\$displaystyle e_{i}$가 환경 $environment$ ${\displaystyle i_{}}$ ${\$에 모두$$$i{\displaystyle }$ ${\displaystyle i_{}}$${\displaystyle }$= ${\displaystyle 1}$인 경우 다음과 같이 읽을 수 있다${\displaystyle \mathrm{.}}$$[\displaystyle i=1..$$n$ 그러면 $e{\displaystyle }$ ${\displaystyle$ e$}$이라는 표현식은 $environment{\displaystyle \mathrm{}}$ ${\displaystyle \Gamma }$ 환경을 가지며 $type$ ${\displaystyle \tau }$을(를) 입력하십시오$.$

예를 들어, 실제 숫자에 대한 산술 계산을 수행하는 간단한 언어는 다음과 같은 규칙을 가질 수 있다.

${\displaystyle {\frac {\Gamma \vdash e_{1}\!:\!real\quad \감마 \vdash e_{2}\!:\!real}{\Gamma \vdash e_{1}+e_{2}\\!real}\qquad {\frac {\\Gamma \vdash e_{1}\!:\!integer\quad \Gamma \vdash e_{2}:integer}{\Gamma \vdash e_{1}+e_{2}}}\!:\!}\qquad \cdots }$

형식 규칙에는 전제가 없을 수 있으며, 일반적으로 이러한 경우 행이 생략된다.형식 규칙은 이전 환경에 새 변수를 추가하여 환경을 변경할 수도 있다. 예를 들어 선언에는 ${\$ 유형의 새 변수 $i{\displaystyle }$ ${\displaystyle d}$ ${\displaystyle id}$이$($가) $\gamma {\displaystyle \mathrm{}}$ ${\displaystyle \Tau '}$에 추가되는 다음과 같은 형식 규칙이 있을 수 있다$.$

$\displaystyle {\frac {\Gamma \vdash e'\!:\!\tau '\quad \감마,id\!:\!\tau '\vdash e\!:\\\tau }{{\Gamma \vdash {\text ID = }}e'{\text{{{}e}{\text{end}}:\!\tau }}$

여기서 let 표현식의 구문은 Standard ML의 구문이다. 따라서 형식 규칙은 자연적 추론에서와 같이 합성 표현식의 유형을 도출하는 데 사용될 수 있다.

참고 항목

• 판단(수학적 논리)
• 유형 시스템
• 유형론
• 커리-하워드 통신

추가 읽기

• Cardelli, Luca (March 1996). "Type Systems" (PDF). ACM Computing Surveys. 28 (1): 263–264. doi:10.1145/234313.234418.