सेटॉइड

"ई-समुच्चय" redirects here. For प्रजनन चिकित्सा में तकनीक, see ई-समुच्चय.

गणित में, समुच्चय (X, ~) एक समुच्चय (गणित) (या प्रकार (गणित)) X है जो एक तुल्यता संबंध ~ से सुसज्जित है। एक सेटॉइड को ई-समुच्चय, बिशप समुच्चय या विस्तारक समुच्चय भी कहा जा सकता है।

सेटॉयड्स का अध्ययन विशेष रूप से प्रमाण सिद्धांत और गणित के प्रकार-सैद्धांतिक आधारों में किया जाता है। प्रायः गणित में, जब कोई समुच्चय पर तुल्यता संबंध को परिभाषित करता है, तो तुरंत भागफल समुच्चय (समानता को समानता (गणित) में बदलना) बनाता है। इसके विपरीत, सेटोइड का उपयोग तब किया जा सकता है जब सर्वसमता और समानता के बीच अंतर को प्रायः गहन समानता (मूल समुच्चय पर समानता) और विस्तारित (शब्दार्थ) समानता (तुल्यता संबंध, या भागफल पर समानता) की व्याख्या के साथ बनाए रखा जाना चाहिए।

प्रमाण सिद्धांत

प्रमाण सिद्धांत में, विशेष रूप से करी-हावर्ड समतुल्यता के आधार पर रचनात्मक गणित का प्रमाण सिद्धांत, प्रायः एक गणितीय प्रस्ताव (गणित) को इसके प्रमाण (गणित) के समुच्चय (यदि कोई हो) के साथ पहचानता है। निश्चित रूप से दिए गए प्रस्ताव के कई प्रमाण हो सकते हैं; प्रमाण अप्रासंगिकता के सिद्धांत के अनुसार, सामान्यतः मात्र प्रस्ताव की सत्यता काअभिप्राय रखती है, न कि किस प्रमाण का उपयोग किया गया था। यद्यपि, करी-हावर्ड समतुल्यता प्रमाण को कलन विधि में बदल सकता है, और कलन विधि के बीच अंतर प्रायः महत्वपूर्ण होते हैं। इसलिए प्रमाण सिद्धांतकार प्रमाणों के एक समूह के साथ एक प्रस्ताव की पहचान करना पसंद कर सकते हैं, यदि वे बीटा रूपांतरण या इसी प्रकार के माध्यम से एक दूसरे में परिवर्तित हो सकते हैं, तो समकक्ष प्रमाणों पर विचार करें।

प्रकार सिद्धांत

गणित के प्रकार-सैद्धांतिक नींव में, सेटोइड का उपयोग एक प्रकार के सिद्धांत में किया जा सकता है जिसमें सामान्य गणितीय समुच्चयों को मॉडल करने के लिए भागफल प्रकार का अभाव होता है। उदाहरण के लिए, प्रति मार्टिन-लोफ के अंतर्ज्ञानवादी प्रकार के सिद्धांत में, वास्तविक संख्याओं का कोई प्रकार नहीं है, मात्र परिमेय संख्याओं के नियमित कॉची अनुक्रमों का एक प्रकार है। इसलिए, मार्टिन-लोफ़ के प्राधार में वास्तविक विश्लेषण करने के लिए, किसी को वास्तविक संख्याओं के समूह के साथ काम करना चाहिए, नियमित कॉची अनुक्रमों का प्रकार जो तुल्यता की सामान्य धारणा से सुसज्जित है। वास्तविक संख्याओं के विधेय और फलनों को नियमित कॉची अनुक्रमों के लिए परिभाषित करने और तुल्यता संबंध के साथ संगत सिद्ध करने की आवश्यकता है। सामान्यतः (यद्यपि यह उपयोग किए गए प्रकार के सिद्धांत पर निर्भर करते है), वरण का स्वयंसिद्ध प्रकार (अंतर्निहित फलनों) के बीच फलनों के लिए होगा, परन्तु सेटोइड (विस्तारित फलनों) के बीच फलनों के लिए नहीं। पद समुच्चय का विभिन्न प्रकार से या तो प्रकार के पर्याय के रूप में या समुच्चय के पर्याय के रूप में प्रयोग किया जाता है।

रचनात्मक गणित

रचनावाद (गणित) में, प्रायः समतुल्य संबंध के अतिरिक्त अलग संबंध के साथ एक सेटॉइड लिया जाता है, जिसे रचनात्मक सेटॉइड कहा जाता है। कभी-कभी आंशिक तुल्यता संबंध या आंशिक पृथकता का उपयोग करके आंशिक सेटॉइड भी माना जाता है। (देखें बारथे एट अल., खंड 1)

यह भी देखें

• ग्रुपॉयड

संदर्भ

• Hofmann, Martin (1995), "A simple model for quotient types", Typed lambda calculi and applications (Edinburgh, 1995), Lecture Notes in Comput. Sci., vol. 902, Berlin: Springer, pp. 216–234, CiteSeerX 10.1.1.55.4629, doi:10.1007/BFb0014055, ISBN 978-3-540-59048-4, MR 1477985.
• Barthe, Gilles; Capretta, Venanzio; Pons, Olivier (2003), "Setoids in type theory" (PDF), Journal of Functional Programming, 13 (2): 261–293, doi:10.1017/S0956796802004501, MR 1985376, S2CID 10069160.

बाहरी संबंध

• Implementation of setoids in Coq
• Setoid in nLab
• Bishop set in nLab