プログラミングは得意だけど数学は苦手．
プログラミングはわかるけど数学はわからない．
そういうときは数学の話をプログラミングの話に置換して考えてみましょう．
c++を使った 1+1=2の証明（ペアノ算術による証明）
c++を使って 1+1=2を証明します．
ただし，定数や変数，加算の演算子"+"は使用しません．
変数や演算子は使わずに「型」を使って 1+1が2になることを示します．
第１ステップ：c++で整数を定義する
変数や定数を使わず，整数自体を「型」で定義します．
整数 Zero の定義
整数のゼロ（"0"）をZero型と定義します．
struct Zero {};
整数 One の定義
整数の1に対応する型をOne型とします
Oneは「Zeroの隣の型」と定義します
定義にはC++のテンプレートを使います．まずテンプレートをつかって，「型Xの隣の型」をnext<X>型と定義します
template <typename X> struct next { typedef X value_type; };
テンプレート next を使うと，Zero型の隣は next<Zero> 型と記述できます．
毎回 next<Zero> と記述するのは面倒なので，typedefを使って next<Zero>型の別名をOne型と定義します
typedef next<Zero> One;
同様に Twoを定義します．TwoはOneの隣なのでnext<One> となります
typedef next<One> Two;
ここまでの定義を整理すると
| Two は next<One> の別名 | TwoはOneの隣 |
| One は next<Zero> の別名 | OneのZeroの隣 |
となります．Two を展開すると next< next< Zero > > となります．つまり「Twoは（（Zeroの隣）の隣）」です．これでZero，One，Twoまで，３つの整数が定義できました．
同じ方法でZeroからSixまで定義すると次のようなソースコードが出来上がります
ファイル名をstep1.cpp とします
// step1.cpp // 整数の定義 #include <iostream> struct Zero {}; template <typename X> struct next { typedef X value_type; }; typedef next<Zero> One; typedef next<One> Two; typedef next<Two> Three; typedef next<Three> Four; typedef next<Four> Five; typedef next<Five> Six; int main() { // typeid(X).name() で「型」Xの名前を表示する // // 出力は c++filt -t で demangle する必要がある std::cout << " Zero: " << typeid(Zero).name() << std::endl; std::cout << " One: " << typeid(One).name() << std::endl; std::cout << " Two: " << typeid(Two).name() << std::endl; std::cout << "Three: " << typeid(Three).name() << std::endl; std::cout << " Four: " << typeid(Four).name() << std::endl; std::cout << " Five: " << typeid(Five).name() << std::endl; std::cout << " Six: " << typeid(Six).name() << std::endl; return 0; }
コンパイルして実行すると次のような出力が得られます
$ g++ step1.cpp $ ./a.out | c++filt -t Zero: Zero One: next<Zero> Two: next<next<Zero> > Three: next<next<next<Zero> > > Four: next<next<next<next<Zero> > > > Five: next<next<next<next<next<Zero> > > > > Six: next<next<next<next<next<next<Zero> > > > > >
c++-filt は demangleといって，c++が内部で使っている型名を，人間が解読できる形式に変換するコマンドです
出力をみると
One: next<Zero> Two: next<next<Zero> >
と テンプレート next
たとえばSixの行をみると， Zeroのnextのnextの〜とnextが６回登場しています．つまりSixはZeroの６個隣の値として定義されています．
私達が普段 0，1，2と表記している数字はこれら Zero，One, Twoをtypedefした記号にすぎない，と考えると数学が少しわかった気になるはずです！
第２ステップ：足し算を定義する
足し算も template を使って定義します．
「X+Y」を Add<X,Y>型として定義し，Add<X,Y>::value_type が足し算の結果となるように定義します
// Defintion of addition template <typename X, typename Y> struct Add; // X + 0 becomes X template <typename X> struct Add<X, Zero> { typedef X value_type; }; // X + next<Y> becomes next<X+Y> template <typename X, typename Y> struct Add<X, next<Y> > { typedef typename Add<X, Y>::value_type Tmp; typedef next<Tmp> value_type; };
Add型の定義は２つあります
- 定義A： Add<X, Zero> 型は，X型に展開
- 定義B： Add<X, next<Y>> 型は next< Add<X,Y>> に展開
の２つです
定義Aは
template <typename X> struct Add<X, Zero> { typedef X value_type; };
です．これは，例をあげると，たとえば1+0は
Add<One, Zero>
となり，計算結果は
Add<One, Zero>::value_type
です．これは One に展開されます
第３ステップ： 1+1の計算
定義Bは
template <typename X, typename Y> struct Add<X, next<Y> > { typedef typename Add<X, Y>::value_type Tmp; typedef next<Tmp> value_type; };
です．
1+1の場合を考えてみます
今までに定義した型を使うと，1+1は
Add<One, One>
と記述できます．
計算結果は
Add<One, One>::value_next
です．このテンプレートを展開します．まず
Add<One, One>
は
Add<One, next<Zero>>::value_next
と展開できます．つまりtypename X=One, typename Y=Zero となるので，定義Bの
typedef typename Add<X, Y>::value_type Tmp; typedef next<Tmp> value_type;
この部分はX，Yが置換されて
typedef typename Add<One, Zero>::value_type Tmp; typedef next<Tmp> value_type;
となります
さらに定義Aより
typedef typename Add<One, Zero>::value_type Tmp; typedef next<Tmp> value_type;
の Add<One, Zero>::value_type は Oneに置換され
typedef One Tmp; typedef next<Tmp> value_type;
よって
typedef next<One> value_type;
となります
ここまでをまとめると
Add<One, One>::value_next
は next<One>となります．
next<One>とは何でしょうか？そうTwoのことです．つまりOne+OneはTwoに展開されました．
以上まとめると，Zero, next<X>, add<X,Y> という３つの定義だけで 1+1 を2 に展開できることが示せました．
最終的なソースコード
このようにテンプレートの展開をくりかえすことで，整数が表現でき，整数の足し算が実行できます．実際のソースコードを示します
ファイル名は prove.cpp とします
// // Proving that 1+1 = 2 by using c++ template // // by pyopyopyo // // Usage: // $ g++ -std=c++11 prove.cpp -o prove // $ ./prove | c++filt -t // #include <iostream> // Define of zero struct Zero {}; // Defines of integers template <typename X> struct next { typedef X value_type; }; typedef next<Zero> One; typedef next<One> Two; typedef next<Two> Three; typedef next<Three> Four; typedef next<Four> Five; typedef next<Five> Six; // Defintion of addition template <typename X, typename Y> struct Add; // X + 0 becomes X template <typename X> struct Add<X, Zero> { typedef X value_type; }; // X + next<Y> becomes next<X+Y> template <typename X, typename Y> struct Add<X, next<Y> > { typedef typename Add<X, Y>::value_type Tmp; typedef next<Tmp> value_type; }; int main() { // Prints name of types. std::cout << " Zero: " << typeid(Zero).name() << std::endl; std::cout << " One: " << typeid(One).name() << std::endl; std::cout << " Two: " << typeid(Two).name() << std::endl; std::cout << "Three: " << typeid(Three).name() << std::endl; std::cout << " Four: " << typeid(Four).name() << std::endl; std::cout << " Five: " << typeid(Five).name() << std::endl; std::cout << " Six: " << typeid(Six).name() << std::endl; // Prove typedef Add<One, One>::value_type Ans; std::cout << "One + One = " << typeid(Ans).name() << std::endl; // static_assert(std::is_same<Two, Ans>::value == true, "proved that 1+1 is 2"); std::cout << "One + Two = " << typeid( Add<One,Two>::value_type ).name() << std::endl; std::cout << "Two + One = " << typeid( Add<One,Two>::value_type ).name() << std::endl; return 0; }
コンパイルして実行します
$ g++ prove.cpp -o prove ./prove | c++filt -t
Zero: Zero One: next<Zero> Two: next<next<Zero> > Three: next<next<next<Zero> > > Four: next<next<next<next<Zero> > > > Five: next<next<next<next<next<Zero> > > > > Six: next<next<next<next<next<next<Zero> > > > > > One + One = next<next<Zero> > One + Two = next<next<next<Zero> > > Two + One = next<next<next<Zero> > >
末尾の３行が，それぞれ
- 1+1は2
- 1+2は3
- 2+1も3
となることを示しています
prove.cppのソースコードは「ペアノ算術」や「ペアノの公理」が言ってることをそのままtemplateを実装しただけです．それをc++のコンパイラで展開すると，One+OneがTwoになるなるという結果が得られています．
数学の本に書いてある小難しい話は，実は，大半が同じ構造になっています．数学の本は，冒頭で templateを定義して，後半はひたすらそのtemplateを展開しています．つまりロジックは同じです．違いは，ロジックを数式で記述するのが数学，templateで記述するのがc++であり，記述方法が違うだけなのです．
ですから，プログラミングは得意だけど数学は苦手，プログラムはわかるけど数学はわからないという人は，数学の話をプログラミングの話に置換して考えてみると，ロジックをあっさり理解できる可能性があります．
