নির্দেশনা
নিকোমাকাসের (৬০ - ১২০ খ্রিস্টাব্দ) ধনাত্মক পূর্ণসংখ্যার শ্রেণিবিভাগ অনুসারে একটি সংখ্যা perfect, abundant, না deficient তা নির্ধারণ করুন।
গ্রিক গণিতবিদ নিকোমাকাস ধনাত্মক পূর্ণসংখ্যার জন্য একটি শ্রেণিবিভাগ তৈরি করেছিলেন, যেখানে প্রতিটি সংখ্যাকেই তার প্রকৃত গুণনীয়কের সমষ্টির ভিত্তিতে perfect, abundant বা deficient, এই তিনটি শ্রেণির ঠিক একটিতে ফেলা হয়।
প্রকৃত গুণনীয়কের সমষ্টি বলতে সংখ্যাটির নিজেকে বাদ দিয়ে তার গুণনীয়কগুলোর যোগফলকে বোঝায়।
যেমন, 15 সংখ্যাটির প্রকৃত গুণনীয়কের সমষ্টি 1 + 3 + 5 = 9।
Perfect
কোনো সংখ্যা তার প্রকৃত গুণনীয়কের সমষ্টির সমান হলে সেই সংখ্যাকে perfect বলা হয়।
যেমন:
-
6 একটি perfect সংখ্যা, কারণ 1 + 2 + 3 = 6
-
28 একটি perfect সংখ্যা, কারণ 1 + 2 + 4 + 7 + 14 = 28
Abundant
কোনো সংখ্যা তার প্রকৃত গুণনীয়কের সমষ্টির চেয়ে ছোট হলে সেই সংখ্যাকে abundant বলা হয়।
যেমন:
-
12 একটি abundant সংখ্যা, কারণ 1 + 2 + 3 + 4 + 6 = 16
-
24 একটি abundant সংখ্যা, কারণ 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Deficient
কোনো সংখ্যা তার প্রকৃত গুণনীয়কের সমষ্টির চেয়ে বড় হলে সেই সংখ্যাকে deficient বলা হয়।
যেমন:
-
8 একটি deficient সংখ্যা, কারণ 1 + 2 + 4 = 7
- মৌলিক সংখ্যা deficient
কাজ
কোনো সংখ্যা perfect কি না তা নির্ধারণ করার একটি উপায় তৈরি করুন।
আপনার ভাষার ট্র্যাকের ওপর নির্ভর করে আপনাকে হয়তো কোনো সংখ্যা abundant বা deficient কি না তা নির্ধারণের উপায়ও তৈরি করতে হতে পারে।
একটি ইন্ডাক্টিভ টাইপ ডিফাইন করা
এই অনুশীলনীতে আশা করা হয় যে রিটার্ন ভ্যালু হবে একটি ইন্ডাক্টিভ টাইপ Classification, যা আপনাকে ডিফাইন করতে হবে।
এই টাইপের একটি BEq ইনস্ট্যান্স থাকতে হবে, অর্থাৎ এটি একটি বুলিয়ান সমতা পরীক্ষা সমর্থন করে, এবং একটি Repr ইনস্ট্যান্স থাকতে হবে, অর্থাৎ টাইপের মানগুলো প্রদর্শনের জন্য ফরম্যাট করা যাবে।
ইনস্ট্যান্স ডিক্লারেশন সম্পর্কে এই পৃষ্ঠাটি দেখতে পারেন।
Lean অনেক ক্লাসের জন্য স্বয়ংক্রিয়ভাবে ইনস্ট্যান্স জেনারেট করতে পারে।
সাবটাইপ
classify ফাংশনের আর্গুমেন্ট হলো Positive নামের একটি সাবটাইপ:
def Positive := { x : Nat // x > 0 }
সাবটাইপ কোনো নির্দিষ্ট টাইপের সেই এলিমেন্টগুলোকে বোঝায়, যেগুলো একটি প্রেডিকেট সন্তুষ্ট করে।
Positive হলো Nat-এর সেই এলিমেন্টগুলো, যেগুলো 0-এর চেয়ে বড়।
সাবটাইপের যেকোনো এলিমেন্টকে একটি জোড় হিসেবে ভাবা যায়, যার একটি অংশ হলো আন্ডারলাইং টাইপের একটি মান আর অন্যটি হলো গাণিতিক অর্থে একটি প্রমাণ যে এই মানটি সংশ্লিষ্ট প্রেডিকেট সন্তুষ্ট করে।
সাবটাইপ টাইপ লেভেলে ইনভ্যারিয়েন্ট নিশ্চিত করে, ফলে ত্রুটিপূর্ণ মান তৈরি করা যায় না।
