交差型規律

言語という用語${\displaystyle (\vdash _{\text{CD}})}$λ項（またはラムダ式）によって与えられる。

${\displaystyle {\begin{aligned}M,N&::=x\mid (\lambda x.\!M)\mid (M\;N)&&{\text{ ただし }}x{\text{ は項変数の範囲をとる }}\\\end{aligned}}}$

型言語${\displaystyle (\vdash _{\text{CD}})}$は、以下の文法によって帰納的に定義される。

${\displaystyle {\begin{aligned}\varphi &::=\alpha \mid \sigma \to \varphi &&{\text{ ただし }}\alpha {\text{ は型変数の範囲}}\\\sigma &::=\varphi _{1}\cap \cdots \cap \varphi _{n}&&{\text{ ただし }}n\geq 1\end{aligned}}}$

交差型コンストラクタ（${\displaystyle \cap }$) は結合法則、交換法則、冪等法則を法として取られます。

タイピングのルール${\displaystyle (\to \!\!{\text{I}})}$、${\displaystyle (\to \!\!{\text{E}})}$、${\displaystyle (\cap {\text{I}})}$、 そして${\displaystyle (\cap {\text{E}})}$の${\displaystyle (\vdash _{\text{CD}})}$は：

${\displaystyle {\begin{array}{cc}{\dfrac {\Gamma ,x:\sigma \vdash _{\text{CD}}M:\varphi }{\Gamma \vdash _{\text{CD}}\lambda x.\!M:\sigma \to \varphi }}(\to \!\!{\text{I}})&{\dfrac {\Gamma \vdash _{\text{CD}}M:\sigma \to \varphi \quad \Gamma \vdash _{\text{CD}}N:\sigma }{\Gamma \vdash _{\text{CD}}M\;N:\varphi }}(\to \!\!{\text{E}})\\\\{\dfrac {\Gamma \vdash _{\text{CD}}M:\varphi _{1}\quad \ldots \quad \Gamma \vdash _{\text{CD}}M:\varphi _{n}}{\Gamma \vdash _{\text{CD}}M:\varphi _{1}\cap \cdots \cap \varphi _{n}}}(\cap {\text{I}})&{\dfrac {(1\leq i\leq n)}{\Gamma ,x:\varphi _{1}\cap \cdots \cap \varphi _{n}\vdash _{\text{CD}}x:\varphi _{i}}}(\cap {\text{E}})\end{array}}}$

型付け可能性と正規化は密接に関連しています${\displaystyle (\vdash _{\text{CD}})}$以下の特性により: ^{[ 2 ]}

• 対象者削減: もし${\displaystyle \Gamma \vdash _{\text{CD}}M:\sigma }$そして${\displaystyle M\to _{\beta }N}$、 それから${\displaystyle \Gamma \vdash _{\text{CD}}N:\sigma }$。
• 正規化: もし${\displaystyle \Gamma \vdash _{\text{CD}}M:\sigma }$、 それから${\displaystyle M}$β正規形を持つ。
• 強く正規化するλ項の型付け可能性：もし${\displaystyle M}$強く正規化する場合、${\displaystyle \Gamma \vdash _{\text{CD}}M:\sigma }$一部の人にとって${\displaystyle \Gamma }$そして${\displaystyle \sigma }$。
• λ I正規化の特性評価：${\displaystyle M}$λ I 計算において正規形を持つのは、以下の条件を満たす場合のみである。${\displaystyle \Gamma \vdash _{\text{CD}}M:\sigma }$一部の人にとって${\displaystyle \Gamma }$そして${\displaystyle \sigma }$。

型言語が空の交差部分を含むように拡張されている場合、つまり${\displaystyle \sigma =\varphi _{1}\cap \cdots \cap \varphi _{n}{\text{ ただし }}n=0}$、 それから${\displaystyle (\vdash _{\text{CD}})}$β等式に関して閉じており、推論意味論に関して健全かつ完全である。^{[ 17 ]}

言語という用語${\displaystyle (\vdash _{\text{BCD}})}$λ項（またはラムダ式）によって与えられる。

${\displaystyle {\begin{aligned}M,N&::=x\mid (\lambda x.\!M)\mid (M\;N)&&{\text{ ただし }}x{\text{ は項変数の範囲をとる }}\\\end{aligned}}}$

型言語${\displaystyle (\vdash _{\text{BCD}})}$は、以下の文法によって帰納的に定義される。

${\displaystyle {\begin{aligned}\sigma ,\tau &::=\alpha \mid \omega \mid \sigma \to \tau \mid \sigma \cap \tau &&{\text{ ただし }}\alpha {\text{ は型変数の範囲をとる }}\end{aligned}}}$

交差型サブタイピング${\displaystyle (\leq )}$は、以下の性質を満たす交差型上の最小の前順序関係（反射的かつ推移的な関係）として定義されます。

${\displaystyle {\begin{aligned}&\sigma \leq \omega ,\quad \omega \leq \omega \to \omega ,\quad \sigma \cap \tau \leq \sigma ,\quad \sigma \cap \tau \leq \tau ,\\&(\sigma \to \tau _{1})\cap (\sigma \to \tau _{2})\leq \sigma \to \tau _{1}\cap \tau _{2},\\&{\text{if }}\sigma \leq \tau _{1}{\text{ and }}\sigma \leq \tau _{2}{\text{, then }}\sigma \leq \tau _{1}\cap \tau _{2},\\&{\text{if }}\sigma _{2}\leq \sigma _{1}{\text{ and }}\tau _{1}\leq \tau _{2}{\text{, then }}\sigma _{1}\to \tau _{1}\leq \sigma _{2}\to \tau _{2}\end{aligned}}}$

交差型サブタイピングは二次時間で決定可能である。^{[ 18 ]}

タイピングのルール${\displaystyle (\to \!\!{\text{I}})}$、${\displaystyle (\to \!\!{\text{E}})}$、${\displaystyle (\cap {\text{I}})}$、${\displaystyle (\leq )}$、${\displaystyle ({\text{A}})}$、 そして${\displaystyle (\omega )}$の${\displaystyle (\vdash _{\text{BCD}})}$は：

${\displaystyle {\begin{array}{cc}{\dfrac {\Gamma ,x:\sigma \vdash _{\text{BCD}}M:\tau }{\Gamma \vdash _{\text{BCD}}\lambda x.\!M:\sigma \to \tau }}(\to \!\!{\text{I}})&{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \to \tau \quad \Gamma \vdash _{\text{BCD}}N:\sigma }{\Gamma \vdash _{\text{BCD}}M\;N:\tau }}(\to \!\!{\text{E}})\\\\{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \quad \Gamma \vdash _{\text{BCD}}M:\tau }{\Gamma \vdash _{\text{BCD}}M:\sigma \cap \tau }}(\cap {\text{I}})&{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \quad (\sigma \leq \tau )}{\Gamma \vdash _{\text{BCD}}M:\tau }}(\leq )\\\\{\dfrac {}{\Gamma ,x:\sigma \vdash _{\text{BCD}}x:\sigma }}({\text{A}})&{\dfrac {}{\Gamma \vdash _{\text{BCD}}M:\omega }}(\omega )\end{array}}}$

• 意味論：${\displaystyle (\vdash _{\text{BCD}})}$これは、 λ項の解釈がそれに割り当てることができる型の集合と一致するフィルタλモデルに関して健全かつ完全である。 ^{[ 3 ]}
• 対象者削減: もし${\displaystyle \Gamma \vdash _{\text{BCD}}M:\sigma }$そして${\displaystyle M\to _{\beta }N}$、 それから${\displaystyle \Gamma \vdash _{\text{BCD}}N:\sigma }$[ ^{3 ]​}
• 主題の拡張：もし${\displaystyle \Gamma \vdash _{\text{BCD}}N:\sigma }$そして${\displaystyle M\to _{\beta }N}$、 それから${\displaystyle \Gamma \vdash _{\text{BCD}}M:\sigma }$[ ^{3 ]​}
• 強い正規化の特性：${\displaystyle M}$β減少に関して強く正規化するのは、${\displaystyle \Gamma \vdash _{\text{BCD}}M:\sigma }$ルールなしで導出可能${\displaystyle (\omega )}$一部の人にとって${\displaystyle \Gamma }$そして${\displaystyle \sigma }$[ ^{19 ]​}
• 主ペア（「主型」とも呼ばれる^{[ 20 ]}）：${\displaystyle M}$が強く正規化される場合、主対が存在する${\displaystyle (\Gamma ,\sigma )}$任意の型に対して${\displaystyle \Gamma '\vdash _{\text{BCD}}M:\sigma '}$そのペア${\displaystyle (\Gamma ',\sigma ')}$主対から取得できる${\displaystyle (\Gamma ,\sigma )}$型の拡張、持ち上げ、置換によって。^{[ 21 ]}