『プログラミング言語の基礎概念』で型推論を実装する

出版社のページ プログラマーとして働いておきながらいまさら「基礎」かと思われそうなタイトルの本書ですが, 「プログラミングの基礎」ではなく「プログラミング言語の基礎」であることがポイントです. プログラミング言語を数学的に厳密に扱う意味論や, エラーを事前に検知するための型システムについての本で, プログラミングの入門本ではありません. 本書では序盤中盤に書けて, プログラミング言語分析のための枠組みについての説明がされていますが, メインは型システム, 型推論だと思います. プログラムの実行や型推論の仕組みについて厳密に扱う方法を知りたい方におすすめです. 対象としている言語は OCaml なので, ある程度 OCaml についての知識があったほうが理解がスムーズだと思います. 分析については基礎から解説してあるので, 前提知識は不要です. 導出システムについて 本書ではプログラムを厳密に扱うための枠組みとして導出システムを使います. 導出システムとは, 定義されたいくつかの規則に従って定理を導出する記述体系です. 本書の流れに沿って, 実際のプログラミング言語を扱う前に, 自然数の加算乗算を対象とした導出システムの例を見ていきます. 自然数を対象とした導出システム (natural numbers から Nat と名付けられている) では簡単のために S(...S(Z)...) のような記法で自然数を表します. 例えば以下のような感じです. 1 2 3 0 -> Z 1 -> S(Z) 2 -> S(S(Z)) 導出システムによって導出される結論を「判断」と言います. Nat での判断は以下の 2 つの形です. n1, n2, n3 は自然数で, 2 つの判断はそれぞれ加算と乗算に対応しています. 1 2 n1 plus n2 is n3 n1 times n2 is n3 式を変形するための規則「推論規則」は以下の 4 つです....

November 23, 2021 · 9 min

『論理学をつくる』で論理学をつくる

導入 記事のタイトルがトートロジーになっています. トートロジーというのは 「トマトはなぜ赤いんだ?」 「赤いから赤いんだよ」 というような, 無意味な同じ言葉の繰り返しのことです. ところで, 論理学では常に真になる文のことをトートロジーと言います. 例えば「クジラは哺乳類であるか, 哺乳類でないかのどちらかだ」というような文は, クジラについて何もわかっていかなったとしても正しいとわかるトートロジーです. では以下の文はどうでしょう. この占い師が信用できるなら, 私の明日旧友と出会う この占い師は信用できる よって, 私の明日旧友と出会う 理屈は正しそうです. ではこれはどうでしょう. この占い師が信用できるなら, 私の明日旧友と出会う 私は翌日旧友と出会った よって, この占い師は信用できる 予言が当たったのなら本物感はありますが, インチキ占い師が適当なことを言ったのにも関わらず, たまたま予言が当たったという可能性もありそうです. ということでこの理屈は間違っていると言えそうです. 常に正しい文, 論理的に正しい/間違った推論. こういった事柄を厳密に扱うのが論理学です. なんだ, 論理学は随分当たり前のことを研究するんだなぁと思うかもしれません. しかし, 推論の正しさや矛盾と言った事柄を一般的に, 明確に, 統一的に示すのは難しそうです. 普段行っている論理的判断であっても, それがなぜ正しいのか説明できなかったり, 対象が複雑になると判断がつかなくなったりします. 本書は論理学を全く学んだことのない人のための教科書です. 初学者でも独学できるように丁寧な説明や練習問題が満載です (ちゃんと練習問題に解説がついているのは嬉しいポイントです. というかなぜ大学の教科書のような本にはついてないことが多いのでしょう). 身近な例から始まって, 述語論理, 自然演繹, 非古典論理など, 様々な話題が盛り込まれています. 序文によると, このような欲張りな目標を立てたために本が分厚くなった (B5 版 400 ページ以上) という事情のようです. 論理学というといかにも堅苦しそうな分野ですが, 著者の軽妙な語り口も相まって気負わず読み進められます. 論理学には全く触れたことはないが, きちんと入門してみたいという方におすすめです. 印象に残った点 タイトル通り, 論理というものを厳密に扱うための体系を少しずつ作っていくのが本書のスタイルです. 記号と抽象の奥深い世界が広がっています. 印象的な部分をまとめます. 論理学を「つくる」とはどういうこと? 論理を研究するに当たって最初に行う作業は, 論理を厳密に扱うことができる体系を作ることです. つまり, 論理を扱うのに都合の良い言語を作って, その人口言語を操作することで話が進みます....

October 24, 2021 · 6 min

『例解 UNIX/Linux プログラミング教室』でシステムプログラミングを学ぶ

概要 UNIX/Linux の機能を使ったシステムプログラミングを解説する本です (出版社のサイト). 副題は「システムコールを使いこなすための 12 講」であり, システムコールに焦点を当てて 幅広く UNIX の概念について解説するスタイルです. ちなみに, タイトルに UNIX と Linux の 2 つの名前がありますが本書の内容はどちらにも通用するものです. この記事でも UNIX/Linux 両方について言及する時は省略して UNIX とだけ書きます. 0-4 章はよく使うコマンドなどの UNIX の基礎や C 言語の復習, ファイル入出力などの基本的な内容で, 5 章以降から本題に入る流れです. 5 章以降で扱われるトピックは, プロセス, ファイルシステム, ソケット, シグナル, 端末などです. UNIX のシステムプログラミングをしたい方や, UNIX 内部の仕組みを知りたいという方におすすめです. 印象に残ったこと 調べ方を知る 本書は割と分厚い本 (約 500 ページ) ですが辞書ではありません. 大量のシステムコールや UNIX の細かい挙動について網羅的に覚えるのではなく, 必要なときに必要なものを調べられるように概念や機能を学ぶというアプローチです. このアプローチのおかげか, 序盤に man コマンドの使い方が紹介されています. man コマンド自体はすでに知っていたのですが, 長くて分かりにくいメッセージが表示されるものという印象があってほとんど使ったことはありませんでした. しかし, どこに注目すればよいかが分かれば便利なものだと気付きました. 例えば, 今まではシステムコールやライブラリを使うのに include が必要なヘッダファイルを毎回ネットで検索していたのですが, man で見たほうが早いし正確です (環境によって微妙に必要なヘッダが違うことがあるらしいので)....

September 12, 2021 · 2 min

『プログラミング in OCaml』で関数型言語に入門

感想 関数型言語を学ぶため, 『プログラミング in OCaml』を読みました (出版社のページ). 関数型言語や関数型プログラミングといった言葉を何度か耳にして気になっていたので入門してみることにしました. OCaml という (マイナー?) な言語を選んだのにはそれほどの理由はありません. C++ を知っていれば Java や C# など他のオブジェクト指向言語もおおよそ似たようなものに感じられるように, 関数型言語を 1 つ学べば他の理解もスムーズになるだろうと思ったという程度です. 関数型言語ならではの考え方に触れたり,他言語に輸入されたであろう機能を見たりして楽しめました. 後半で詳しく書いていますが, 木のようなデータ構造を型で表現できる機能や再帰を使ったエレガントな書き方には感動しました. 基礎から説明してあるので, 関数型言語を学んだことのない方にもおすすめの本です. 印象に残ったこと いくつかピックアップして印象的な点を振り返ります. OCaml の歴史 ML というプラグラミング言語の処理系の 1 つらしいのですが, 祖先に当たる ML は元々コンピュータで数学の手切りを証明するためのシステムに起源を持つ言語のようです. この説明だけでも, ML やその派生言語が C 言語系 (ALGOL 系?) の言語と出自が異なるということが感じられます. 関数型言語では「プログラムを実行する = 関数を実行してその解を得る」という捉え方です. プログラムは複数の関数の組み合わせであり, その関数を実行していくことがプログラムの目的ということです. これが関数型と言われる所以だと思います. 強力な型推論 型推論自体は多くのメジャーな静的型付け言語に備わっている機能だと思います. 本書では, OCaml は基本的に必要がなければ型は書かなくて良いというスタンスで, これは型推論が言語の中心的な機能として最初から考えられていたからこそのものだと思いました. 例えば C++ にも 型推論の auto はあります. これは C++11 から追加された機能で, 便利ですが乱用するのは良しとされない印象があります. あまりにも長い型名 (iterator など) や冗長な型宣言を省略するというあくまでも補助的な機能のように感じます....

August 22, 2021 · 3 min

『Effective C++』は中級者への足がかりとなる濃密なガイドライン

より良い C++ コードを書くためのガイドラインとなる『Effective C++』第 3 版を読みました. (出版社のページ). 有用な知識やアドバイスが多く非常に良い勉強になりました. 学んだことや感想を記します. 感想 C++ の本として有名な本書の名前は聞いたことがあり昔軽く手にとってみたことがあったのですが, いまいちピンとこず, 大事なことが書いてあるのだろうけどよくわからない難しい本という印象をもっていました. しかし改めて読んでみると, C++ の経験をある程度積んだおかげか, 非常に有用で興味深い内容に感じられました. すでに知っていることが 3 割, 知らなかった or よく理解していなかったことが 7 割程度でした. 今までこんなにも多くのことを知らずに C++ を使っていたのかと愕然としたり, こんなに細かいことまで気にしなければならないのかと 引いたり 驚いたりしました. 印象に残ったこと 印象に残った項目をいくつかピックアップして振り返ります. 7 項, 36 項 ポリモーフィズムのための基底クラスには仮想デストラクタを宣言する 非仮想関数を派生クラスで再定義するのは NG まず本書序盤の 7 項で「ポリモーフィズムのための基底クラスには仮想デストラクタを宣言しよう」というタイトルが付けられているのですが, 最初はタイトルを見ても何のことだかさっぱり分かりませんでした. 基底クラスのデストラクタを仮想にしておかないとメモリが正常に開放されないことがあるという内容で, へぇーと思ったのですが, ちゃんと理解できたのは後半の 36 項を読んでからでした. 36 項では, 非仮想関数を派生クラスで再定義すると, 呼び出し方によって基底/派生クラスのどちらの関数が呼ばれるか変わってしまうということが説明されています. これを読んでようやく 7 項の意味が分かりました. 派生クラスは必ずデストラクタを再定義するので, 基底クラスのデストラクタは仮想にしなければならないということです. この項だけでも継承, 仮想関数, コンパイラによるコンストラクタ/デストラクタの自動生成といったことへの知識が必要になり, 自分の知識のなさや理解の浅さを実感しました. そして, もしこれを知らないままポリモーフィズムを使っていた場合, 原因不明のメモリ異常に悩まされることになっていただろうと思うと恐ろしくもありました. C++ の奥深さに気付かされた印象的な項目でした. 13 項 リソース管理にはオブジェクトを使う オブジェクトがスコープを抜けるときデストラクタが自動実行されることを利用してリソースの解法忘れを防ぐという内容です....

August 21, 2021 · 2 min

『コンピュータシステムの理論と実装』でハードとソフトをまたいでコンピュータを理解する

コンピュータを 0 から自分の手で作り上げるという意欲的な内容です. 論理ゲートから始まって高水準言語を実装し,その言語で OS を作成するという過程は旅という言葉がしっくりくるほど濃密なものでした. 内容 コンピュータの構築を通じてコンピュータ・サイエンスにおける重要なテーマを学びます ( 出版社のサイト ). ハードウェア (論理演算, CPU, メモリ) ハードとソフト全体が協調するシステムのアーキテクチャ プログラミング言語 (コンパイラ, オブジェクト指向) OS (メモリ管理, 数学/幾何アルゴリズム, I/O など) ソフトウェアエンジニアリング (モジュール化, テスト, API デザインなど) ハードウェア → ソフトウェアとボトムアップにコンピュータ構築を進めていきます. ハードウェア編では論理ゲートから始まって CPU とメモリを実装し, 最終的にノイマン型アーキテクチャのコンピュータを作り上げます. ソフトウェア編ではアセンブラ, バーチャルマシン, コンパイラと進んで高級言語を実装する過程がメインです. 最後に実装した高級言語で OS を作成します. 自分の手で作るということが本書のテーマであり, 各章には説明と仕様だけがあり答えはありません. ハードウェアの設計にはハードウェア記述言語 (HDL) を用い, シミュレータで実行するので実際に電子部品を組み立てる必要はありません. ソフトウェア編で作成するコンパイラは自分の好みの言語で実装します. 感想 ハードウェアの設計は初体験だったのですが, パズルを解くような感覚で楽しめました. 多少苦労した箇所もありましたが, ハードウェア編でかかった時間は各章 2 時間程度でした. それよりも遥かに苦戦したのはコンパイラの実装です. 今でこそ各章の内容が秩序立って理解できますが, 当初はそもそも何をすれば良いのかわからず, 何度も説明を読んだり試しに実装をしたりしてなんとか進めてきました. ソフトウェア編全体でかかった時間は 100 時間近いと思います. 本書に取り組んでいて迷ったときのコツですが, アセンブラとコンパイラは完成品が提供されているのでその挙動を見ると良いと思います. 私は最初コンパイラが何をすればよいのかさっぱりつかめなかったのですが, 提供されているコンパイラを実行して理解できました. 大変な苦労はしましたが, 全体を通じて有意義な学びが多く取り組んで良かったと思っています. コンピュータの仕組みを実際に作りながら学びたいという方には非常におすすめです....

July 18, 2021 · 1 min