小ネタ. (0 = zero, 1 = succ<zero>, 2 = succ<succ<zero>>, ...)という風にネストしたクラステンプレートの実体を自然数に対応させて1+1=2を確認する. 数学に疎いので厳密な証明になっているかはわかりません.
#include <type_traits>
namespace nat {
struct nat {};
template <class T>
concept bool Nat = std::is_base_of_v<nat, T>;
/* 自然数0が存在する */
struct zero : nat {};
/* 全ての自然数にはその次の自然数が存在する */
template <Nat>
struct succ : nat {};
template <Nat, Nat>
struct plus;
template <Nat N, Nat M>
using plus_t = typename plus<N, M>::type;
/* 加法の定義 */
/* N + 0 = N */
template <Nat N>
struct plus<N, zero> {
using type = N;
};
/* 加法の定義 */
/* N + succ(M) = succ(N + M) */
template <Nat N, Nat M>
struct plus<N, succ<M>> {
using type = succ<plus_t<N, M>>;
};
} // namespace nat
auto main() -> int {
using namespace nat;
/* 1 := succ(0) */
using one = succ<zero>;
/* 2 := succ(succ(0)) */
using two = succ<succ<zero>>;
static_assert(std::is_same_v<plus_t<one, one>, two>, "1 + 1 == 2");
}
検証(コンパイル)
自然数の制約にC++2aのconceptを使ったので適宜対応するオプションを与える. アサーションが失敗せずにコンパイルが通るはず.
$ g++-8 -std=c++2a -fconcepts peano.cpp
おまけ
偶数を定義してみる
namespace nat {
template <Nat>
struct is_even;
template <Nat N>
constexpr bool is_even_v = is_even<N>::value;
template <Nat N>
concept bool Even = is_even_v<N>;
/* 0は偶数 */
template <>
struct is_even<zero> : public std::bool_constant<true> {};
/* 偶数の次の次は偶数 */
template <Even E>
struct is_even<succ<succ<E>>> : public std::bool_constant<true> {};
/* それ以外は偶数ではない */
template <Nat>
struct is_even : public std::bool_constant<false> {};
} // namespace nat
auto main() -> int {
using namespace nat;
using one = succ<zero>;
using two = succ<one>;
using three = succ<two>;
using four = succ<three>;
using five = succ<four>;
static_assert(Even<zero>, "0 is even");
static_assert(!Even<one>, "1 is not even");
static_assert(Even<two>, "2 is even");
static_assert(!Even<three>, "3 is not even");
static_assert(Even<four>, "4 is even");
static_assert(!Even<five>, "5 is not even");
}