نوع القسمة

في مجال نظرية الأنواع في علوم الحاسوب ، يُعرف نوع القسمة بأنه نوع بيانات يحترم علاقة مساواة يُحددها المستخدم . يُعرّف نوع القسمة علاقة تكافؤ.${\displaystyle \equiv }$على عناصر النوع - على سبيل المثال، يمكننا القول إن قيمتين من النوع Pointمتكافئتان إذا كانت لهما نفس الإحداثيات س و ص؛ رسميًا p1 == p2إذا كان p1.x == p2.x && p1.y == p2.y. في نظريات الأنواع التي تسمح بأنواع القسمة، يُشترط شرط إضافي وهو أن تحترم جميع العمليات التكافؤ بين العناصر. على سبيل المثال، إذا fكانت دالة على قيم من النوع Point، فيجب أن يكون صحيحًا أنه بالنسبة لقيمتين من Pointالنوع p1، p2إذا كان ، p1 == p2فإن f(p1) == f(p2).

تُعدّ أنواع القسمة جزءًا من فئة عامة من الأنواع تُعرف بأنواع البيانات الجبرية . في أوائل ثمانينيات القرن العشرين، تم تعريف أنواع القسمة وتطبيقها كجزء من مساعد البرهان Nuprl ، في عملٍ قاده روبرت ل. كونستابل وآخرون. ^{[ 1 ] [ 2 ]} دُرست أنواع القسمة في سياق نظرية مارتن-لوف للأنواع ، ^{[ 3 ]} ونظرية الأنواع التابعة ، ^{[ 4 ]} ومنطق الرتبة العليا ، ^{[ 5 ]} ونظرية أنواع التماثل . ^{[ 6 ]}

لتعريف نوع خارج القسمة، يُقدَّم عادةً نوع بيانات مع علاقة تكافؤ على هذا النوع، على سبيل المثال، Point // ==حيث ==تمثل علاقة مساواة معرفة من قِبل المستخدم. عناصر نوع خارج القسمة هي فئات تكافؤ لعناصر النوع الأصلي. ^{[ 3 ]}

يمكن استخدام أنواع القسمة لتعريف الحساب النمطي . على سبيل المثال، إذا Integerكان نوع البيانات هو الأعداد الصحيحة،${\displaystyle \equiv _{2}}$يمكن تعريفها بالقول إن${\displaystyle x\equiv _{2}y}$إذا كان الفرق${\displaystyle xy}$هو عدد زوجي. ثم نشكل نوع الأعداد الصحيحة modulo 2: ^{[ 1 ]}

Integer //${\displaystyle \equiv _{2}}$

يمكن إثبات أن العمليات على الأعداد الصحيحة، +، -معرفة جيدًا على نوع القسمة الجديد.

في نظريات الأنواع التي تفتقر إلى أنواع القسمة، تُستخدم المجموعات الجزئية (المجموعات المزودة صراحةً بعلاقة تكافؤ) غالبًا بدلًا من أنواع القسمة. ومع ذلك، على عكس المجموعات الجزئية، قد تتطلب العديد من نظريات الأنواع برهانًا رسميًا على أن أي دوال معرفة على أنواع القسمة تكون معرفة جيدًا . ^{[ 7 ]}

تُعدّ أنواع القسمة جزءًا من فئة عامة من الأنواع تُعرف بأنواع البيانات الجبرية . وكما تُشابه أنواع الضرب وأنواع الجمع الضرب الديكارتي والاتحاد المنفصل للبنى الجبرية المجردة، فإن أنواع القسمة تعكس مفهوم القسمة في نظرية المجموعات ، وهي مجموعات تُقسّم عناصرها إلى فئات تكافؤ بواسطة علاقة تكافؤ مُعطاة على المجموعة. وتُسمى البنى الجبرية التي تكون مجموعتها الأساسية قسمة أيضًا بالقسمة. ومن أمثلة هذه البنى القسمة: مجموعات القسمة ، والمجموعات ، والحلقات ، والفئات ، وفي علم الطوبولوجيا، فضاءات القسمة . ^{[ 3 ]}

• نوع البيانات الجبرية
• نوع المنتج
• سيتويد
• نوع المجموع