قاعدة الطباعة

في نظرية الأنواع ، قاعدة التصنيف هي قاعدة استدلال تصف كيفية إسناد نظام الأنواع نوعًا إلى بنية نحوية . ^{[ 1 ] : 94} يمكن لنظام الأنواع تطبيق هذه القواعد لتحديد ما إذا كان البرنامج مصنفًا بشكل صحيح وما هي تعابير الأنواع . ومن الأمثلة النموذجية على استخدام قواعد التصنيف تعريف استدلال الأنواع في حساب لامدا ذي التصنيف البسيط ، وهو اللغة الداخلية للفئات المغلقة الديكارتية . ^{[ 2 ]}

تحدد قواعد الكتابة بنية علاقة الكتابة التي تربط المصطلحات النحوية بأنواعها. ^{[ 1 ] : 92} نحويًا، يُشار عادةً إلى علاقة الكتابة بنقطتين رأسيتين، على سبيل المثال${\displaystyle e:\tau }$يشير إلى أن التعبير${\displaystyle e}$له نوع${\displaystyle \tau }$تُحدد القواعد نفسها عادةً باستخدام تدوين الاستدلال الطبيعي . ^{[ 1 ] : 26} على سبيل المثال، تحدد قواعد الكتابة التالية علاقة الكتابة للغة بسيطة من القيم المنطقية : ^{[ 1 ] : 93}

${\displaystyle {\frac {}{{\mathsf {true}}:{\mathsf {Bool}}}}\qquad {\frac {}{{\mathsf {false}}:{\mathsf {Bool}}}}\qquad {\frac {e_{1}:{\mathsf {Bool}}\quad \;e_{2}:\tau \quad \;e_{3}:\tau {\mathbf {if} \ e_{1}\ \mathbf {ثم} \ e_{2}\ \mathbf {else} \ e_{3}:\tau }}}$

تنص كل قاعدة على أنه يمكن استنتاج النتيجة أسفل الخط من المقدمات أعلاه. القاعدتان الأوليان لا تحتويان على مقدمات أعلاه، لذا فهما بديهيتان . أما القاعدة الثالثة فتحتوي على مقدمات أعلاه (ثلاث مقدمات تحديدًا)، لذا فهي قاعدة استدلال .

في لغات البرمجة، يعتمد نوع المتغير على مكان ربطه ، مما يستلزم قواعد كتابة حساسة للسياق. تُحدد هذه القواعد من خلال حكم كتابة ، يُكتب عادةً${\displaystyle \Gamma \vdash e:\tau }$، وهو ما ينص على أن التعبير${\displaystyle e}$له نوع${\displaystyle \tau }$في سياق الكتابة${\displaystyle \Gamma }$يربط ذلك المتغيرات بأنواعها. وتُستكمل سياقات الكتابة أحيانًا بأنواع المتغيرات الفردية؛ على سبيل المثال،${\displaystyle \Gamma ,x{:}\tau _{1}\vdash e:\tau _{2}}$يمكن قراءتها على أنها "السياق"${\displaystyle \Gamma }$بالإضافة إلى المعلومات التي تفيد بأن التعبير${\displaystyle x}$له نوع${\displaystyle \tau _{1}}$وينتج عن الحكم أن التعبير${\displaystyle e}$له نوع${\displaystyle \tau _{2}}$يمكن استخدام هذه الصيغة لإعطاء قواعد كتابة لمراجع المتغيرات وتجريد لامدا في حساب لامدا ذي الكتابة البسيطة : ^{[ 1 ] : 101-102}

${\displaystyle {\frac {x{:}\tau \in \Gamma }{\Gamma \vdash x:\tau }}\qquad {\frac {\Gamma ,x{:}\tau _{1}\vdash e:\tau _{2}}{\Gamma \vdash (\lambda x{:}\tau _{1}.\,e):\tau _{1}\rightarrow \تاو _{2}}}}$

وبالمثل، تصف قاعدة الكتابة التالية ما يلي:${\displaystyle \mathbf {let} }$بنية لغة التعلم الآلي القياسية :

${\displaystyle {\frac {\Gamma \vdash e_{1}:\tau _{1}\qquad \Gamma ,x{:}\tau _{1}\vdash e_{2}:\tau _{2}}{\Gamma \vdash \mathbf {let} \ x=e_{1}\ \mathbf {in} \ e_{2}\ \mathbf {end}$ :\tau _{2}}}}

لا تُحدد جميع أنظمة قواعد الكتابة خوارزمية فحص النوع بشكل مباشر . على سبيل المثال، تتطلب قاعدة الكتابة لتطبيق دالة متعددة الأشكال ذات المعاملات في نظام هيندلي-ميلنر "تخمين" النوع المناسب الذي يجب إنشاء الدالة فيه. ^{[ 3 ]} يتطلب تكييف نظام قواعد تصريحي مع خوارزمية قابلة للتقرير إنتاج نظام خوارزمي منفصل يمكن إثبات أنه يُحدد علاقة الكتابة نفسها. ^{[ 4 ]}

• الحكم (المنطق الرياضي)
• نظام الكتابة
• نظرية الأنواع
• مراسلات كاري-هوارد
• حساب المتتابعات

• كارديلي، لوكا (مارس 1996). "أنظمة الأنواع" . مجلة ACM Computing Surveys . 28 (1): 263-264 . doi : 10.1145/234313.234418 . S2CID 227408784 . 
• كارديلي، لوكا (يونيو 2004). أنظمة الأنواع ، 41 صفحة. دليل علوم الحاسوب، الطبعة الثانية، الفصل 97. تحرير ألين ب. تاكر. ISBN 9780429209390. تاريخ الاطلاع: 5 يناير 2025.