نظام الكتابة النقية

في فرعي المنطق الرياضي المعروفين بنظرية البرهان ونظرية الأنواع ، يُعد نظام الأنواع الخالص ( PTS )، المعروف سابقًا بنظام الأنواع المعمم ( GTS )، شكلًا من أشكال حساب لامدا المكتوب ، يسمح بعدد غير محدود من الأصناف والتبعيات بينها. يمكن اعتبار هذا الإطار تعميمًا لمكعب لامدا لباريندريخت ، بمعنى أن جميع زوايا المكعب يمكن تمثيلها كحالات لنظام أنواع خالص بصنفين فقط. ^{[ 1 ] [ 2 ]} في الواقع، صاغ باريندريخت (1991) مكعبه ضمن هذا السياق. ^{[ 3 ]} قد تُخفي أنظمة الأنواع الخالصة التمييز بين الأنواع والمصطلحات ، وتُؤدي إلى انهيار التسلسل الهرمي للأنواع ، كما هو الحال في حساب الإنشاءات ، ولكن هذا ليس هو الحال عمومًا، فعلى سبيل المثال، يسمح حساب لامدا المكتوب ببساطة للمصطلحات فقط بالاعتماد على المصطلحات.

طُرحت أنظمة الأنواع النقية بشكل مستقل من قِبل ستيفانو بيراردي (1988) ويان تيرلو (1989). ^{[ 1 ] [ 2 ]} ناقشها باريندريخت باستفاضة في أبحاثه اللاحقة. ^{[ 4 ]} في أطروحته للدكتوراه، ^{[ 5 ]} عرّف بيراردي مكعبًا من المنطق البنائي يُشبه مكعب لامدا (هذه المواصفات غير مترابطة). أُطلق على تعديل هذا المكعب لاحقًا اسم مكعب L من قِبل هيرمان جوفرز، الذي وسّع في أطروحته للدكتوراه تطابق كاري-هوارد ليشمل هذا السياق. ^{[ 6 ]} بناءً على هذه الأفكار، عرّف جي.  بارث وآخرون أنظمة الأنواع النقية الكلاسيكية (CPTS) بإضافة عامل نفي مزدوج . ^{[ 7 ]} وبالمثل، في عام 1998، قدّم تين بورغويس أنظمة الأنواع النقية المشروطة (MPTS). ^{[ 8 ]} ناقش رودا تطبيق أنظمة الأنواع النقية على البرمجة الوظيفية ؛ واقترح رودا وجورينغ لغة برمجة قائمة على أنظمة الأنواع النقية. ^{[ 9 ]}

من المعروف أن جميع الأنظمة المشتقة من مكعب لامدا تتميز بخاصية التطبيع القوي . أما أنظمة الأنواع النقية، فليست بالضرورة كذلك، فمثلاً، النظام U من مفارقة جيرارد ليس كذلك. (باختصار، وجد جيرارد أنظمة نقية يمكن فيها التعبير عن عبارة "الأنواع تُشكل نوعًا"). علاوة على ذلك، فإن جميع الأمثلة المعروفة لأنظمة الأنواع النقية غير المُطَبَّعة بقوة ليست مُطَبَّعة (بشكل ضعيف) : فهي تحتوي على تعابير لا تمتلك صيغًا طبيعية ، تمامًا مثل حساب لامدا غير المُنمَّط . يُعدّ هذا الأمر مشكلة مفتوحة رئيسية في هذا المجال، وهي ما إذا كان هذا هو الحال دائمًا، أي ما إذا كان نظام الأنواع النقية المُطَبَّع (بشكل ضعيف) يمتلك دائمًا خاصية التطبيع القوي. يُعرف هذا باسم حدسية باريندريخت-جوفرز-كلوب (نسبةً إلى هينك باريندريخت ، وهيرمان جوفرز ، ويان ويليم كلوب ). ^{[ 10 ]}

يُعرَّف نظام النوع النقي بثلاثية${\textstyle ({\mathcal {S}},{\mathcal {A}},{\mathcal {R}})}$أين${\textstyle {\mathcal {S}}}$هي مجموعة من الأنواع،${\textstyle {\mathcal {A}}\subseteq {\mathcal {S}}^{2}}$هي مجموعة البديهيات، و${\textstyle {\mathcal {R}}\subseteq {\mathcal {S}}^{3}}$هي مجموعة القواعد. يتم تحديد الكتابة في أنظمة الكتابة النقية بواسطة القواعد التالية، حيث${\textstyle s}$أي نوع: ^{[ 4 ]}

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

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

${\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{(weakening)}}}$

${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}\quad (s_{1},s_{2},s_{3})\in {\mathcal {R}}}{\Gamma \vdash \Pi x:AB:s_{3}}}\quad {\text{(product)}}}$

${\displaystyle {\frac {\Gamma \vdash C:\Pi x:AB\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:AB:s}{\Gamma \vdash \lambda x:Ab:\Pi x:AB}}\quad {\text{(abstraction)}}}$

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

لغات البرمجة التالية تحتوي على أنظمة أنواع نقية:

• SAGE ^{[ 11 ]}
• اليارو ^{[ 12 ]}
• هينك 2000 ^{[ 13 ]}
• لغة هاسكل منذ الإصدار الثامن من GHC. ^{[ 14 ] [ 15 ]}

• النظام U – مثال على نظام PTS غير متسق
• يستخدم حساب λμ نهجًا مختلفًا للتحكم عن CPTS

• شميدت، ديفيد أ. (1994). "القسم 8.3 أنظمة الأنواع المعممة" . بنية لغات البرمجة المكتوبة . مطبعة معهد ماساتشوستس للتكنولوجيا. ص 255-258 . ISBN  0-262-19349-3.

• نظام النوع النقي في مختبر n
• جونز، روجر بيشوب (1999). "نظرة عامة على أنظمة النوع النقي" .