今回はたし算に関する証明をいくつか行っていきます。以下のファイルを用意しました(https://polymony.net/wp-content/uploads/2019/06/agda2ndSource.zip)。(1)から開始してください。証明を行うためのいくつかのおまじないの行が追記されています。(2)は前回説明しました、SpacemacsとAgdaLayerについての最低限のコマンドを用意したチートシートです。
(1) 今回開始時のソースコード(AgdaSecondBegin.agda)
(2) Spacemacsの最低限コマンド集(SpacemacsCheatSheet.txt)
動画では最初に説明しただけで表示してませんでしたが、皆さんがご自身でプログラミングを進める際には、下の画像のようにSpacemacsのウィンドウを左に寄せておいて、右側にメモ帳でコマンド集を開いておくと便利かも知れません。
今回も動画を用意しました。証明の対象となる公式は以下の4つです。小学生の子は、nとmを例えば3と4で置き換えてみてください。
n + 0 = n
0 + n = n
(succ m) + n = succ (m + n)
（上は(1 + m) + n = 1 + (m + n) をsuccで表したもの）
(n + m) = (m + n)
どれも、一見すると当然成り立つ公式と思われますが、前回定義した自然数と足し算の定義から出発して証明することができます。下の動画でひとつずつ説明しています。
次回は、かけ算を定義していくつかの公式を証明する予定です。よろしくお願いします（※１）
（※１）動画の最後の方で、今回の証明で用いた手法は数学的帰納法と関係すると述べておいて、説明をしていませんでした。これは結構深い原理(自然数に関するinduction principle)に関連していて、今は混乱する可能性があるので、とりあえずAgdaの操作に慣れてください。
いずれ説明する予定ですが、興味がある人はHoTT（Homotopy Type Theory）の本（https://homotopytypetheory.org/book/）の1.9 The natural numbersを読んでみてください。実は足し算とか、こういう数学的帰納法的な証明がひとつの原理で説明がつきます。逆に言うと、この原理を理解すればバラバラに見えていたものがひとつ上の目線で見えるようになります。
こういうのって、人類の進歩の観点で非常に大事だと思っています。中学生以上の人だとわかると思いますが、小学生で〇〇算とか習ったと思いますが、方程式の観点で見ると、どの〇〇算もその一例に過ぎないと見えます。方程式を理解すれば実際に〇〇算を簡単に解けるようになるという実利が得られますが、他にも実際に解けなくても「一例に過ぎない」と見ることでそれ以上関わらない、関心を持たない（※２）（※３）、その代わりに方程式に関するより高度な問題（代数学や解析幾何学など）にとりかかるようになる、なれる、時間を割けるようになる。後の世代の人間は、前の世代の人間の用意してくれた見通しの良い数学を使って先に進む、次につなげる、というのがこれまでの歴史（※４）であり、今後もそれが続くのでしょう。
現状では自分が見る限りでは、見通しのいい数学としては、プログラムの領域ではAgdaやHaskellみたいな関数型プログラミングであり、論理学の領域では型理論、数学の領域では圏論なのだろうと思ってます。ただ、驚くのはこれらが出てきたのは、戦前、戦後直後という、コンピュータもない（あるにしても今ほど性能が良くない）時代に既にあったということです。多分、今の最先端の学者さんとかはこれらよりも先の数学を手に入れているのでしょうね。
（※２）もちろん、具象から抽象の方向性（演繹でなく帰納の方向）もあると思います。ソビエト（ロシア）系の数学はそういうのを大事にしていて、その姿勢を大事にした教育書もたくさん出ています（ソビエト科学アカデミーの本とか）。冒頭にマルクスとかレーニンとか出てくるので、一瞬構えてしまいますが、その後に続く数学の内容は、具体的な事例から抽象化していて非常に教育的です。ただ、その逆方向もあると思うのです。（※４）に述べた事例とかは抽象での議論をしていたところ、具体的事例にも適用できてしまった感じです。他にも例えばラマヌジャンという数学者を調べてもらうと出てきますが、何か別世界からの電波を受けているとしか思えないパターンもあります。説明のつかない神秘的な何かがまだまだあるのだと思います。
（※３）ただ、思考停止というのは方向性を誤れば損をしている向きもあります。
ひとつ目の例としては、一人の人間の成長をみても小さい時は路傍の花ひとつひとつに関心を向けていたけれども、大きくなるとどうですか？思考停止して「花」と見ている人が多いのではないでしょうか？その分抽象的な課題にとりかかることになりますが、もしかしたら思考停止をやめて、そういう花を研究することで何か出てくる可能性は十分あります、自分が知らないだけであるのでしょう。
ふたつ目の例としては、最近流行りのいわゆるA.I.（機械学習系）が成功しているのは、人間が思考停止している視点（例えば、これは花だ、その特徴は花びらとか茎とかがあって、、のような特徴ベクトル）を一度リセットしてフラットに見ている（これは二次元のRGBで構成された画像だ）からこそ、というのもあるのでしょう。ただし、その分計算コストがかかってきます。疲れない機械がやっているから良いのでしょうが、いずれ頭打ちが来る時が来る可能性があります（ムーアの法則とか成り立たなくなってきてますね。電子回路の配線の微細化にも限界があります）。大事になってくるかなと思うのは、そういうフラット（連続、実数的）な観点から思考停止（不連続、自然数的）の側にいわゆるA.I.（機械）が自動でもって行けるようにする、ということな気がします。
型理論の型ってそういうのに関係してきそうで、大事だと思っています。型に当てはめる（事例をまとめる）ことで、それらに成り立つ原理（型チェック）を用いることができる、とかです。ただし、そういうデータ型ってプログラマが自分で設定している感じで、具体的なこの混沌としたデータ（例えば文字列、自然言語）から何かを抽出する、思考停止する、という作用は働いていない感があります。
型理論のなかでも、それでは型ってどういう時に成立するのか、みたいな議論をしているところがあるので、それを拘束条件として、文字列とかを分析すれば何か出てくるんじゃないか？そんな気がしています。機械学習の自己符号化器ってそんな感（反射律）がないですか？筋がいい感じの正解を最適化パラメータの初期値として与えている（分類、型として分類する際に反射律が成り立っている場所から出発するのが当然良いだろう）みたいな。筋のいい数学（型理論やHoTT）を手に入れてから自然言語処理の機械学習学習の領域（parser(構文解析)はもうひとつの方向）もやってみると面白いと思っています。
では、こういう一歩先のA.I.をやろうとした時に、どういうプログラミング言語がいいか？、となると、
①AgdaやHaskellなどの関数型プログラミング言語
（型理論や数学（圏論）に立脚していて、parsing（構文解析）を得意とし、数学的な証明で高速化や状況に応じた最適化をかけてくれる）
②Scheme (LISP)
（プログラムをつくるプログラムを書ける（プログラム化するというのは、一つメタの観点で抽象化していることになる））
になると思っています。プログラミングの義務教育でも、この辺りを題材（少なくともこれら言語にスムーズに移行できることを視野に入れた内容）とするべきだと思います。
（※４）例えば、ニュートン力学であれば、前の時代に代数と幾何学を結びつける解析幾何学をデカルトやフェルマー達が用意していて、代数に微分積分を適用することで幾何学（惑星の軌道）をとくことができた、アインシュタインの場合はガウスやリーマンが相対性理論に使える曲面の幾何学を用意していた、量子力学も線形代数や群論が既に用意されていた、といった具合です。数学者って人たちはすごいですね。