zakkyの雑記

エンジニアリング全般についての備忘録

『論理と計算のしくみ』を読んだ

計算機科学の入門書である『論理と計算のしくみ』を読んだ

タイトルの通りで、GWの前半を使って『論理と計算のしくみ』という本を読んだ。 https://www.amazon.co.jp/dp/4007305803/

実はこの本自体は、エンジニアとして仕事をし始めた5年前のタイミングで購入していた。

いわゆる積読状態だったのだが、流石に5年も寝かせたままなのもな…と思い一念発起して読んだ。

感想はと言うと、読んで良かったな〜としみじみする本だった。 それだけだと全然伝わらないと思うので、箇条書きで良かった点を書くと、

  • 基礎的な集合論や命題論理、様相論理をコンパクトに解説してくれている
  • 集合論と論理学をベースに、コンピュータにおける計算というものがどう定義されるのかを示してくれる
  • 無目的に論理学を学ぶのではなく、最終的には計算可能性やλ計算といったコンピュータサイエンスの領域へと繋がっていくのだという、明確なゴール地点を意識しながら学べたのでモチベが続いた
  • だいたいどんなトピックを追えば、計算という分野の概略を掴めるかの地図を提供してくれた
  • ゲーデル不完全性定理や型付きラムダ計算、カリー・ハワード同型対応といった「なんか聞いたことあるな〜」という程度だった概念について、なんとなく雰囲気を掴めるようになった
  • プログラムの評価順序に大きく絡んでくる、β簡約や評価戦略の話は、色んなプログラミング言語をどんな角度で捉えるかの新しい観点を提供してくれた

という具合だ。

集合論や論理学について全く知識がない状態でこの本を読むのは流石に厳しいと思うので、その辺全くの初学者だという人は別の入門書を読んでからチャレンジするとよいだろう。

というか、5年前の自分が数ページ読んだだけで挫折したのは確かそれが原因だったはず。

この本を読んで何が変わったか

劇的にプログラミングが上手になったかというと、そうではないだろう。

そういった即効性のある本ではないが、これまで自分が暗黙的に抱いていた疑問の正体が掴めるきっかけをくれたと思う。

7年前に初めてプログラミングの勉強を始めた際、Rubyを触ったときに感じた疑問は、

「このソースコードというやつは、いったいどれから先に実行されるのだろうか?」というものだった。

この問いに単純化して答えると、コードは上から書かれた順に実行されるということになるが、例えば関数定義をするようなコードはどのタイミングで実行されるのかはエンジニアとして働き始めてからもピンときていなかった。

その後、勉強をしていくなかでこの疑問というのは、「どの順番、規則でソースコードを"評価"するか?」という問いとほぼイコールであると知るのだが、その評価のやり方についての詳細は立ち入らないまま職業エンジニアとして過ごしてきた。

もちろん、「遅延評価」や「β簡約」といったワードには出会うことがありなんとなく雰囲気を理解したつもりではいたが、そうした概念が計算機科学の中でどんな文脈で登場するかについては、俯瞰して捉えることが出来ていなかった。

本書はまさに、「どの順序で、どんな規則を用いてコードを評価するか」という評価戦略の話を、論理学における論理式の導出や式変形の文脈を通して行ってくれるので、なぜこの概念が登場するかの必要性がしっくり来る構成になっている。

これまで自分が持っていた各知識を有機的に繋いでくれる本、というのが適切だろう。

次に読む本

中々こういった業務に直結しない本を読む時間を設けるのは、意識しないと難しいのだが今年はちゃんと時間を使っていきたい。

GW後半に読み始めた『プログラミング言語の基礎概念』という本が、型付きラムダ計算や型推論についてもう少し詳しく書いてくれているようなので、この勢いのまま読了したい。

https://www.amazon.co.jp/dp/4781912850