निर्देश
निकोमैकस (60 - 120 ईस्वी) ने धनात्मक पूर्णांकों के लिए जो वर्गीकरण प्रणाली बनाई थी, उसके आधार पर निर्धारित कीजिए कि कोई संख्या पूर्ण है, अधिक है या न्यून।
यूनानी गणितज्ञ निकोमैकस ने धनात्मक पूर्णांकों के लिए एक वर्गीकरण प्रणाली बनाई, जिसमें हर संख्या अपने एलिक्वॉट योग के आधार पर पूर्ण, अधिक या न्यून इन तीन श्रेणियों में से ठीक एक में आती है।
एलिक्वॉट योग किसी संख्या के सभी गुणनखंडों का जोड़ है, लेकिन इसमें वह संख्या खुद शामिल नहीं होती।
उदाहरण के लिए, 15 का एलिक्वॉट योग 1 + 3 + 5 = 9 है।
पूर्ण
कोई संख्या तब पूर्ण होती है जब वह अपने एलिक्वॉट योग के बराबर होती है।
उदाहरण के लिए:
-
6 एक पूर्ण संख्या है क्योंकि 1 + 2 + 3 = 6
-
28 एक पूर्ण संख्या है क्योंकि 1 + 2 + 4 + 7 + 14 = 28
अधिक
कोई संख्या तब अधिक होती है जब वह अपने एलिक्वॉट योग से कम होती है।
उदाहरण के लिए:
-
12 एक अधिक संख्या है क्योंकि 1 + 2 + 3 + 4 + 6 = 16
-
24 एक अधिक संख्या है क्योंकि 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
न्यून
कोई संख्या तब न्यून होती है जब वह अपने एलिक्वॉट योग से अधिक होती है।
उदाहरण के लिए:
-
8 एक न्यून संख्या है क्योंकि 1 + 2 + 4 = 7
- अभाज्य संख्याएँ न्यून होती हैं
कार्य
ऐसा तरीका बनाइए जिससे पता चले कि दी गई संख्या पूर्ण है या नहीं।
आपके भाषा ट्रैक के अनुसार आपको यह तय करने का तरीका भी बनाना पड़ सकता है कि दी गई संख्या अधिक है या न्यून।
इंडक्टिव टाइप को परिभाषित करना
इस अभ्यास में अपेक्षा है कि रिटर्न वैल्यू एक इंडक्टिव टाइप Classification हो, जिसे आपको खुद परिभाषित करना है।
इस टाइप में एक BEq इंस्टेंस होना चाहिए, यानी यह बूलियन समानता की जाँच की अनुमति देता है। साथ ही एक Repr इंस्टेंस भी होना चाहिए, यानी इस टाइप की वैल्यू को प्रदर्शित करने के लिए फॉर्मेट किया जा सकता है।
इंस्टेंस घोषणाओं के बारे में इस पेज को देख सकते हैं। Lean कई क्लासों के लिए इंस्टेंस अपने आप बना सकता है।
सबटाइप
classify फंक्शन का आर्गुमेंट एक सबटाइप है, जिसका नाम Positive है:
def Positive := { x : Nat // x > 0 }
सबटाइप किसी खास टाइप के उन एलिमेंट को दर्शाते हैं जो किसी प्रेडिकेट को पूरा करते हैं।
Positive Nat के उन एलिमेंट को दर्शाता है जो 0 से बड़े हैं।
किसी भी सबटाइप के एलिमेंट को एक जोड़े के रूप में सोचा जा सकता है, जिसमें एक वैल्यू उस मूल टाइप की होती है और एक प्रमाण, गणितीय अर्थ में, कि यह वैल्यू संबंधित प्रेडिकेट को पूरा करती है।
सबटाइप टाइप के स्तर पर ही इनवेरिएंट लागू करते हैं, जिससे यह पक्का हो जाता है कि गलत ढंग से बनी वैल्यू बनाई ही नहीं जा सकती।
