تخصص نوع التقاطع

مصطلح لغة${\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 ]}