有理數

說明

有理數定義為兩個整數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₂)。

將有理數r₁ = a₁/b₁除以另一個有理數r₂ = a₂/b₂，在a₂不為零時，結果是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同除以a和b的最大公因數（gcd）。 因此，舉例來說，gcd(12, 8) = 4，所以r = 12/8可以約分成(12/4)/(8/4) = 3/2。 有理數約分後的形式應該符合「標準形式」（分母一律為正整數）。 如果分母是負整數，就將分子與分母同乘以-1，以確保符合標準形式。 例如，3/-4應該約分成-3/4

假設你使用的程式語言沒有有理數的實作。

證明屬性

在這個練習中，你必須定義一個 RationalNumber 型別，用來表示一個完全約分且有效的有理數。這是由型別本身的屬性直接強制保證的。

直接在型別層級編碼規格與限制，能讓無效的狀態實質上無法表示。不過，這也為程式設計師帶來了額外的負擔：他們必須證明這個屬性永遠成立。

這一章對 Lean 中的定理證明做了很好的入門介紹。如果想更深入鑽研，Lean 網站將這本書列為官方資源。

你也可以查閱這門語言的參考資料喔。

---

出處

Wikipedia