निर्देश
परिमेय संख्या को दो पूर्णांकों a और b के भागफल के रूप में परिभाषित किया जाता है, जिन्हें क्रमशः अंश और हर कहा जाता है, और जहाँ b != 0 होता है।
ध्यान दीजिए कि गणित की दृष्टि से हर शून्य नहीं हो सकता।
लेकिन परिमेय संख्याओं के कई कार्यान्वयनों में आप पाएँगे कि हर को शून्य होने दिया जाता है, और उसका व्यवहार फ्लोटिंग पॉइंट संख्याओं में धन या ऋण अनंत जैसा होता है।
ऐसे मामलों में भी अंश और हर सामान्यतः एक साथ शून्य नहीं हो सकते।
परिमेय संख्या r = a/b का निरपेक्ष मान |r|, |a|/|b| के बराबर होता है।
दो परिमेय संख्याओं r₁ = a₁/b₁ और r₂ = a₂/b₂ का योग r₁ + r₂ = a₁/b₁ + a₂/b₂ = (a₁ * b₂ + a₂ * b₁) / (b₁ * b₂) होता है।
दो परिमेय संख्याओं r₁ = a₁/b₁ और r₂ = a₂/b₂ का अंतर r₁ - r₂ = a₁/b₁ - a₂/b₂ = (a₁ * b₂ - a₂ * b₁) / (b₁ * b₂) होता है।
दो परिमेय संख्याओं r₁ = a₁/b₁ और r₂ = a₂/b₂ का गुणनफल (गुणा) r₁ * r₂ = (a₁ * a₂) / (b₁ * b₂) होता है।
यदि a₂ शून्य न हो, तो परिमेय संख्या r₁ = a₁/b₁ को दूसरी परिमेय संख्या r₂ = a₂/b₂ से भाग देने पर r₁ / r₂ = (a₁ * b₂) / (a₂ * b₁) मिलता है।
परिमेय संख्या r = a/b को ऋणेतर पूर्णांक घात n तक बढ़ाने पर r^n = (a^n)/(b^n) प्राप्त होता है।
परिमेय संख्या r = a/b को ऋणात्मक पूर्णांक घात n तक बढ़ाने पर r^n = (b^m)/(a^m) प्राप्त होता है, जहाँ m = |n| है।
परिमेय संख्या r = a/b को वास्तविक (फ्लोटिंग पॉइंट) संख्या x तक बढ़ाने पर भागफल (a^x)/(b^x) प्राप्त होता है, जो एक वास्तविक संख्या है।
वास्तविक संख्या x को परिमेय संख्या r = a/b तक बढ़ाने पर x^(a/b) = root(x^a, b) प्राप्त होता है, जहाँ root(p, q) का अर्थ p का qवाँ मूल है।
निम्नलिखित ऑपरेशन कार्यान्वित कीजिए:
- दो परिमेय संख्याओं का जोड़, घटाव, गुणा और भाग,
- निरपेक्ष मान, किसी दी गई परिमेय संख्या को पूर्णांक घात तक बढ़ाना, किसी दी गई परिमेय संख्या को वास्तविक (फ्लोटिंग पॉइंट) घात तक बढ़ाना, और किसी वास्तविक संख्या को परिमेय संख्या तक बढ़ाना।
आपके कार्यान्वयन में परिमेय संख्याएँ हमेशा न्यूनतम रूप में ही रहनी चाहिए।
उदाहरण के लिए, 4/4 को न्यूनतम रूप में लाने पर 1/1 मिलना चाहिए, 30/60 को 1/2 मिलना चाहिए, 12/8 को 3/2 मिलना चाहिए, इत्यादि।
परिमेय संख्या r = a/b को न्यूनतम रूप में लाने के लिए a और b को उनके महत्तम समापवर्तक (gcd) से भाग दीजिए।
तो, उदाहरण के लिए, gcd(12, 8) = 4, इसलिए r = 12/8 को न्यूनतम रूप में लाकर (12/4)/(8/4) = 3/2 किया जा सकता है।
परिमेय संख्या का न्यूनतम रूप "मानक रूप" में होना चाहिए (हर हमेशा एक धनात्मक पूर्णांक होना चाहिए)।
यदि हर ऋणात्मक पूर्णांक हो, तो अंश और हर दोनों को -1 से गुणा कीजिए, ताकि मानक रूप प्राप्त हो जाए।
उदाहरण के लिए, 3/-4 को न्यूनतम रूप में लाकर -3/4 किया जाना चाहिए।
मान लीजिए कि जिस प्रोग्रामिंग भाषा का आप उपयोग कर रहे हैं, उसमें परिमेय संख्याओं का कोई कार्यान्वयन नहीं है।
प्रॉपर्टी सिद्ध करना
इस अभ्यास में, आपको एक RationalNumber टाइप परिभाषित करना है जो एक पूर्णतः न्यूनतम रूप में मान्य परिमेय संख्या को दर्शाता है।
यह सीधे एक ऐसी प्रॉपर्टी से लागू किया जाता है जो स्वयं टाइप का हिस्सा है।
विनिर्देशों और बाधाओं को सीधे टाइप लेवल पर एनकोड करने से अमान्य अवस्थाएँ व्यावहारिक रूप से निरूपित नहीं की जा सकतीं।
हालाँकि, इससे प्रोग्रामर पर एक अतिरिक्त बोझ भी पड़ता है, जिसे यह सिद्ध करना होता है कि यह प्रॉपर्टी हमेशा सत्य रहती है।
यह अध्याय Lean में प्रमेय सिद्ध करने का एक अच्छा परिचय देता है।
गहराई से जानने के लिए, यह किताब Lean की वेबसाइट पर एक आधिकारिक संसाधन के रूप में सूचीबद्ध है।
आप भाषा के लिए एक संदर्भ भी देख सकते हैं।
