완전수

지침

니코마코스(서기 60~120년)가 양의 정수를 분류한 체계에 따라, 어떤 수가 완전수, 과잉수, 부족수인지 판별해요.

그리스 수학자 니코마코스는 양의 정수를 분류하는 체계를 고안했어요. 각 수를 진약수의 합에 따라 완전수, 과잉수, 부족수 중 하나로 구분하는 방식이었죠. _진약수의 합_은 어떤 수의 약수 중에서 자기 자신을 제외한 것들의 합으로 정의해요. 예를 들어, 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의 원소를 나타내죠.

서브타입의 원소는 기반 타입의 값과, 그 값이 해당 술어를 만족한다는 수학적 의미의 증명이 짝을 이룬 것으로 생각할 수 있어요.

서브타입은 타입 수준에서 불변식을 강제해서, 잘못된 형태의 값이 만들어질 수 없도록 해요.

---

출처

Neal Ford의 Functional Thinking 2장에서 가져왔어요.