- 紙書籍をお届けします（PDFがついてきます）
- 通常はご注文から2～3営業日で発送します。
- 年末年始や大型連休など、1週間から10日程度、配送のお休みをいただく場合があります。詳しくはお知らせをご覧ください
計算機好きのための技術解説情報誌
- エヌゲッカンラムダノート（不定期刊行）
- 116ページ
- A5判
- 紙書籍は1色刷
- 2025年3月1日 第5巻第1号／通巻10号 発行
n月刊ラムダノートは、nヶ月ごとに刊行される、計算機好きのための技術解説情報誌。コンセプトは「いろんなIT系技術書から1章ずつ選んできた解説記事の集まり」です。今号は3本の記事をお送りします。
目次
#1 自然数を作って学ぶLean言語（井上亜星）
高度な型システムを備えた定理証明支援系として注目を集めるLean。特に言語機能が大きく強化されたLean 4 は、実用的なソフトウェア開発が可能な汎用の純粋関数型プログラミング言語でもある。この特徴からLean 4 では、厳密な証明を通してプログラムを組み上げていくスタイルでのソフトウェア開発が可能になっている。
本稿では、ペアノの公理に基づいて自然数を定義し、その加法や乗法の性質を証明していく過程を通して、Lean による証明の書き方と、ソフトウェアとしての数学理論の実装の仕方を概説する。Lean による定理証明に興味がある人はもちろん、多くのソフトウェアエンジニアにとっても、証明がプログラミングと縁遠いものではないことが体験できるチュートリアルになるだろう。
#2 Chromiumはテキストをどのように描画しているのか（佐藤可奈留）
ウェブブラウザの画面に表示されるコンテンツは、ピクセルの集合として画面に描画される。テキストデータであれば、指定されたスタイルや言語ごとの規則に従ってフォントデータから取り出した文字の形状を並べるという処理が施されている。
本稿では、Chromium の実装を紐解いていくことで、その処理の背景にどのような概念や機構があるかを概説する。横書き表示される通常のテキスト本体の描画だけでなく、テキスト上下の罫線や打ち消し線や、いわゆる圏点、さらには縦書きの実現方法などについても紹介する。
#3 実用Raft（太田 健）
Raft は複数のステートマシンを同期させて強い整合性と永続化を実現できる分散合意アルゴリズムである。明快で理解しやすいアルゴリズムにより、データの一貫性を維持しつつシステムの可用性を高められることから、さまざまな用途で広く用いられている。
本稿では、サーバーにRaft を組み込んで冗長化するという観点で、アルゴリズムの解説に留まらないRaft の実践的な知見を概説する。シンプルな分散キーバリューストアを実装し、その性能を測定することで、いかにして実装や運用の工夫によりRaft の性能を高められるかを考察する。
執筆者紹介
井上亜星（#1）
1997年滋賀県生まれ。京都大学理学部卒、京都大学大学院理学研究科数学・数理解析専攻修士課程修了。ITベンチャー企業勤務。2022年、就職を機にプログラミングを始めた。2023年8月ごろにLeanを知って夢中になり、Lean言語を日本に広めるべく活動していこうと決意する。Leanの日本語コミュニティlean-jaの立ち上げに関わったほか、Leanのオンライン日本語リファレンス「Lean by Example」の執筆などのOSS活動を行う。
佐藤可奈留（#2）
マッキンゼー・アンド・カンパニーでビジネスコンサルタントとして勤務した後、ウェブエンジニアとしてテックタッチ株式会社に入社。現在はGMO Flatt Security株式会社で脆弱性診断業務に従事している。バグハントやブラウザへのコントリビューションを楽しみつつ、計算理論や型理論にも興味を持つ。趣味はゲーム、マンガ、レコード収集。
太田 健（#3）
過去には株式会社ドワンゴでRaftライブラリーとそれを用いた分散オブジェクトストレージの開発・運用を経験。現在は株式会社時雨堂で、主力製品であるWebRTC SFU Soraの、Raftを使った分散機能の開発などを担当。趣味ではもっぱらRustを用いて雑多なライブラリーやツールを作っている。共著に『Optunaによるブラックボックス最適化』（オーム社）。
目次
1. 自然数を作って学ぶLean言語
1.1 Leanとは
1.2 環境構築
1.3 自然数を定義して1 + 1 = 2を証明する
1.4 型クラスで見やすく綺麗に
1.5 帰納法で0 + n = nを証明する
1.6 等式変形による単純化を自動化する
1.7 加法の交換法則と結合法則を解放する
1.8 帰納法を改善する
1.9 加法がキャンセルできることを示す
1.10 乗法の基本的な性質を示す
1.11 おわりに
1.12 参考文献
2. Chromiumはテキストをどのように描画しているのか
2.1 ChromiumとBlink、Skia
2.2 レイアウト過程では何を計算するか
2.3 ペイント過程で起こること
2.4 テキストの回転
2.5 おわりに
2.6 参考資料
3. 実用Raft
3.1 Raftの特徴
3.2 Raftを使った分散キーバリューストアの実装
3.3 分散キーバリューストアを動かしてみる
3.4 Raftアルゴリズム概説
3.5 Raftの性能
3.6 おわりに
3.7 謝辞
3.8 参考文献
