دستورالعمل‌ها
یک عدد گویا به‌عنوان خارج‌قسمت دو عدد صحیح a و b تعریف می‌شود که به آن‌ها به‌ترتیب صورت و مخرج می‌گویند و b != 0 است.
توجه داشته باشید که از نظر ریاضی، مخرج نمی‌تواند صفر باشد.
اما در بسیاری از پیاده‌سازی‌های اعداد گویا خواهید دید که مخرج مجاز است صفر باشد، با رفتاری مشابه بی‌نهایت مثبت یا منفی در اعداد ممیز شناور.
در چنین مواردی، معمولاً هنوز هم مخرج و صورت نمی‌توانند هم‌زمان صفر باشند.
قدر مطلق |r| عدد گویای r = a/b برابر |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₂).
تقسیم عدد گویای r₁ = a₁/b₁ بر عدد گویای دیگری r₂ = a₂/b₂ برابر است با r₁ / r₂ = (a₁ * b₂) / (a₂ * b₁)، به شرط اینکه a₂ صفر نباشد.
به توان رساندن عدد گویای 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) ریشه‌ی qاُم p است.
عملیات زیر را پیاده‌سازی کنید:
- جمع، تفریق، ضرب و تقسیم دو عدد گویا،
- قدر مطلق، به توان رساندن یک عدد گویای داده‌شده به توان عدد صحیح، به توان رساندن یک عدد گویای داده‌شده به توان عدد حقیقی (ممیز شناور) و به توان رساندن یک عدد حقیقی به عدد گویا.
پیاده‌سازی شما از اعداد گویا باید همیشه به ساده‌ترین صورت کاهش یابد.
برای مثال، 4/4 باید به 1/1 کاهش یابد، 30/60 باید به 1/2 کاهش یابد، 12/8 باید به 3/2 کاهش یابد و غیره.
برای کاهش یک عدد گویای r = a/b، a و b را بر بزرگ‌ترین مقسوم‌علیه مشترک (gcd) a و b تقسیم کنید.
بنابراین برای مثال، gcd(12, 8) = 4، پس r = 12/8 را می‌توان به (12/4)/(8/4) = 3/2 کاهش داد.
صورت کاهش‌یافته‌ی یک عدد گویا باید در «شکل استاندارد» باشد (مخرج باید همیشه یک عدد صحیح مثبت باشد).
اگر مخرجی با عدد صحیح منفی وجود داشت، هم صورت و هم مخرج را در -1 ضرب کنید تا شکل استاندارد به دست آید.
برای مثال، 3/-4 باید به -3/4 کاهش یابد.
فرض کنید زبان برنامه‌نویسی‌ای که استفاده می‌کنید پیاده‌سازی‌ای از اعداد گویا ندارد.
اثبات ویژگی‌ها
در این تمرین باید نوعی به اسم RationalNumber تعریف کنید که یک عدد گویای معتبر و کاملاً ساده‌شده را نمایش می‌دهد.
این موضوع مستقیماً به واسطه‌ی ویژگی‌ای تضمین می‌شود که بخشی از خودِ نوع است.
کدگذاری مشخصات و محدودیت‌ها به‌طور مستقیم در سطح نوع، باعث می‌شود حالت‌های نامعتبر عملاً غیرقابل‌نمایش باشند.
اما این کار بار اضافی نیز بر دوش برنامه‌نویس می‌گذارد، چون باید ثابت کند که آن ویژگی همیشه برقرار است.
این فصل مقدمه‌ی خوبی برای اثبات قضیه در Lean ارائه می‌دهد.
برای مطالعه‌ای عمیق‌تر، این کتاب به‌عنوان یک منبع رسمی در وب‌سایت Lean معرفی شده است.
همچنین ممکن است بخواهید یک مرجع برای این زبان را هم بررسی کنید.
