完全数

説明

ニコマコス（西暦60〜120年）による正の整数の分類法に基づいて、ある数値が完全数、過剰数、不足数のどれにあたるかを判定してください。

ギリシャの数学者ニコマコスは、正の整数の分類法を考案しました。それぞれの数値は、そのアリコット和に基づいて、完全数・過剰数・不足数のいずれか1つにだけ分類されます。 _アリコット和_とは、ある数値の約数のうち、その数値自身を除いたものの和と定義されます。 例えば、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は、0より大きいNatの要素を表します。

部分型の要素はどれも、元になっている型の値と、その値が対応する述語を満たすという数学的な意味での証明との、2つの組になっていると考えることができます。

部分型は型のレベルで不変条件を強制するため、不正な形の値を作ることはできません。

---

出典

Neal Ford著『Functional Thinking』の第2章より