- Linuxとかプログラミングの覚え書き

systemdにバグ．/home以下のファイルが全削除される可能性あり

systemdのバージョン256に /homeディレクトリ以下のファイルを削除してしまうバグがあったそうで，修正版の 256.1 がリリースされています．

systemdのissuesによると，一時ファイルを一括削除する systemd-tmpfiles --purge コマンドが /home以下を不要ファイルと誤判定して削除するそうです

 

C++で変数を使わずに1+1=2を証明する（ペアノ算術による証明）

プログラミングは得意だけど数学は苦手．
プログラミングはわかるけど数学はわからない．

そういうときは数学の話をプログラミングの話に置換して考えてみましょう．

お題：1+1=2の証明

例として 1+1=2 の証明を取り上げます

ここにある「ペアノ算術による証明」をc++で実装してみます．

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 とします




    
	
  1. // step1.cpp 
    2. 
	
  2. // 整数の定義
    3. 
	
  3.  
    4. 
	
  4. #include <iostream>
    5. 
	
  5.  
    6. 
	
  6. struct Zero {};
    7. 
	
  7. template <typename X> struct next { typedef X value_type; };
    8. 
	
  8. typedef next<Zero> One;
    9. 
	
  9. typedef next<One> Two;
    10. 
	
  10. typedef next<Two> Three;
    11. 
	
  11. typedef next<Three> Four;
    12. 
	
  12. typedef next<Four> Five;
    13. 
	
  13. typedef next<Five> Six;
    14. 
	
  14.  
    15. 
	
  15. int
    16. 
	
  16. main()
    17. 
	
  17. {
    18. 
	
  18. // typeid(X).name() で「型」Xの名前を表示する
    19. 
	
  19. //
    20. 
	
  20. // 出力は c++filt -t で demangle する必要がある
    21. 
	
  21.  
    22. 
	
  22. std::cout << " Zero: " << typeid(Zero).name() << std::endl;
    23. 
	
  23. std::cout << " One: " << typeid(One).name() << std::endl;
    24. 
	
  24. std::cout << " Two: " << typeid(Two).name() << std::endl;
    25. 
	
  25. std::cout << "Three: " << typeid(Three).name() << std::endl;
    26. 
	
  26. std::cout << " Four: " << typeid(Four).name() << std::endl;
    27. 
	
  27. std::cout << " Five: " << typeid(Five).name() << std::endl;
    28. 
	
  28. std::cout << " Six: " << typeid(Six).name() << std::endl;
    29. 
	
  29.  
    30. 
	
  30. return 0;
    31. 
	
  31. }
    32. 




コンパイルして実行すると次のような出力が得られます






    
	
  1. $ g++ step1.cpp
    2. 
	
  2. $ ./a.out | c++filt -t
    3. 
	
  3. Zero: Zero
    4. 
	
  4. One: next<Zero>
    5. 
	
  5. Two: next<next<Zero> >
    6. 
	
  6. Three: next<next<next<Zero> > >
    7. 
	
  7. Four: next<next<next<next<Zero> > > >
    8. 
	
  8. Five: next<next<next<next<next<Zero> > > > >
    9. 
	
  9. Six: next<next<next<next<next<next<Zero> > > > > >
    10. 




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 が足し算の結果となるように定義します






    
	
  1. // Defintion of addition
    2. 
	
  2. template <typename X, typename Y> struct Add;
    3. 
	
  3.  
    4. 
	
  4. // X + 0 becomes X
    5. 
	
  5. template <typename X> struct Add<X, Zero> {
    6. 
	
  6. typedef X value_type;
    7. 
	
  7. };
    8. 
	
  8.  
    9. 
	
  9. // X + next<Y> becomes next<X+Y>
    10. 
	
  10. template <typename X, typename Y> struct Add<X, next<Y> > {
    11. 
	
  11. typedef typename Add<X, Y>::value_type Tmp;
    12. 
	
  12. typedef next<Tmp> value_type;
    13. 
	
  13. };
    14. 




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 とします






    
	
  1. //
    2. 
	
  2. // Proving that 1+1 = 2 by using c++ template
    3. 
	
  3. //
    4. 
	
  4. // by pyopyopyo
    5. 
	
  5. //
    6. 
	
  6. // Usage:
    7. 
	
  7. // $ g++ -std=c++11 prove.cpp -o prove
    8. 
	
  8. // $ ./prove | c++filt -t
    9. 
	
  9. //
    10. 
	
  10.  
    11. 
	
  11. #include <iostream>
    12. 
	
  12.  
    13. 
	
  13. // Define of zero
    14. 
	
  14. struct Zero {};
    15. 
	
  15.  
    16. 
	
  16. // Defines of integers
    17. 
	
  17. template <typename X> struct next { typedef X value_type; };
    18. 
	
  18. typedef next<Zero> One;
    19. 
	
  19. typedef next<One> Two;
    20. 
	
  20. typedef next<Two> Three;
    21. 
	
  21. typedef next<Three> Four;
    22. 
	
  22. typedef next<Four> Five;
    23. 
	
  23. typedef next<Five> Six;
    24. 
	
  24.  
    25. 
	
  25. // Defintion of addition
    26. 
	
  26. template <typename X, typename Y> struct Add;
    27. 
	
  27.  
    28. 
	
  28. // X + 0 becomes X
    29. 
	
  29. template <typename X> struct Add<X, Zero> {
    30. 
	
  30. typedef X value_type;
    31. 
	
  31. };
    32. 
	
  32.  
    33. 
	
  33. // X + next<Y> becomes next<X+Y>
    34. 
	
  34. template <typename X, typename Y> struct Add<X, next<Y> > {
    35. 
	
  35. typedef typename Add<X, Y>::value_type Tmp;
    36. 
	
  36. typedef next<Tmp> value_type;
    37. 
	
  37. };
    38. 
	
  38.  
    39. 
	
  39. int
    40. 
	
  40. main()
    41. 
	
  41. {
    42. 
	
  42. // Prints name of types.
    43. 
	
  43. std::cout << " Zero: " << typeid(Zero).name() << std::endl;
    44. 
	
  44. std::cout << " One: " << typeid(One).name() << std::endl;
    45. 
	
  45. std::cout << " Two: " << typeid(Two).name() << std::endl;
    46. 
	
  46. std::cout << "Three: " << typeid(Three).name() << std::endl;
    47. 
	
  47. std::cout << " Four: " << typeid(Four).name() << std::endl;
    48. 
	
  48. std::cout << " Five: " << typeid(Five).name() << std::endl;
    49. 
	
  49. std::cout << " Six: " << typeid(Six).name() << std::endl;
    50. 
	
  50.  
    51. 
	
  51. // Prove
    52. 
	
  52. typedef Add<One, One>::value_type Ans;
    53. 
	
  53. std::cout << "One + One = " << typeid(Ans).name() << std::endl;
    54. 
	
  54. // static_assert(std::is_same<Two, Ans>::value == true, "proved that 1+1 is 2");
    55. 
	
  55.  
    56. 
	
  56.  
    57. 
	
  57. std::cout << "One + Two = " << typeid( Add<One,Two>::value_type ).name() << std::endl;
    58. 
	
  58. std::cout << "Two + One = " << typeid( Add<One,Two>::value_type ).name() << std::endl;
    59. 
	
  59.  
    60. 
	
  60. return 0;
    61. 
	
  61. }
    62. 




コンパイルして実行します



$ 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++であり，記述方法が違うだけなのです．



ですから，プログラミングは得意だけど数学は苦手，プログラムはわかるけど数学はわからないという人は，数学の話をプログラミングの話に置換して考えてみると，ロジックをあっさり理解できる可能性があります．





まとめ



    
	
  • 数学は難しい！そう感じたときはC++のコードに置換して考えてみましょう．
    • 
	
  • 数学と言ってもtemplateを定義してそれを展開しているだけ，c++のプログラミングと一緒じゃん，と思えるようになるかも知れません
    •