プログラミング言語の基礎概念を学んでる

プログラミング言語の基礎概念 (ライブラリ情報学コア・テキスト)

この本を読んで学んでる。まだ半分くらいで関数の定義とかについて勉強してる。

プログラミング言語の動作を数学的に厳密に記述する方法を順番に教えてくれるという内容で、記述には導出システムが用いられてる。基本的な算術式からはじまって、変数の定義や関数の定義、パターンマッチや型システムなど、様々な言語の機能を推論規則によって定義する方法を教えてくれる。与えられた規則が意味的に意図したものを表しているかの証明だけでなく、証明のやり方もくわしく説明されていて丁寧でたすかる。

おもしろいのはこの本のためのオンラインの演習システムというのがあって、本の中で与えられた導出システムに基づいて式が正しいことを導出する練習問題をすることができる。サイト内に検証器がうごいていて、自分が与えた導出が正しいかを判定してくれる。どこまで問題を解いたか記録してくれたりもするし、ゲームっぽい感じで勉強できておもしろい。

プログラミング言語の基礎概念 演習システム

雰囲気だけお伝えすると、2 + 0 が 2に評価できることを導出するために、以下の様に書くと正解という感じ。S(S(Z))ていうのはペアノ自然数の表現で、チャーチ数みたいなやつ。by E-Plus みたいなのはどのような推論規則を適用したかという雰囲気。詳しくは本読むか演習システムのドキュメント読むと雰囲気わかる。

S(S(Z)) + Z evalto S(S(Z)) by E-Plus {
    S(S(Z)) evalto S(S(Z)) by E-Const {};
    Z evalto Z by E-Const {};
    S(S(Z)) plus Z is S(S(Z)) by P-Succ {
        S(Z) plus Z is S(Z) by P-Succ {
            Z plus Z is Z by P-Zero {}
        }
    }
}

そんなに複雑な問題はないんだけど、たまにきついのがあるっぽくて油断できない。以下の様な式が正しいことを導出するっていう問題があって、たしかに面倒そうな気はするなーと思ってとりくんだら、めっちゃ大層なことになった。

let twice = fun f -> fun x -> f (f x) in twice twice (fun x -> x * x) 2 evalto 65536

問題を解くのは難しいわけではなくて、ルールにしたがって丁寧に間違えずに式を変換していけば、いずれ導出がえられる。ただ、少しでもまちがえると全部おかしくなるので、まちがえずに丁寧にやる必要がある。同じようなことを何度も丁寧にまちがえずにやる必要があって、コンパイラの気持ちが体験できる。