-
紙書籍をお届けします（PDFがついてきます）
- 通常はご注文から2～3営業日で発送します。
- 年末年始や大型連休など、1週間から10日程度、配送のお休みをいただく場合があります。詳しくはお知らせをご覧ください。
プログラミングと数学をつなぐ
- 井上亜星 著
- 228ページ
- A5判/1色刷
- ISBN：978-4-908686-21-4
- 2025年9月4日 第1版第1刷
- 正誤など
ソフトウェアとして数学を扱いたい人、そして数学の力をソフトウェアに結びつけたい人にとってのプログラミング言語、Lean。本書では、動作するプログラムとして自然数と整数を構築することで、数学とソフトウェアがLeanによってどう結び付けられるかを確かめながら、Leanによりソフトウェアを開発するための基礎を身に付けます。
数学の形式化に興味がある数学者はもちろん、数学に挑戦したいプログラマーや、計算機科学の抽象概念を手触りで確かめたいエンジニアにも最適な一冊です。
本書は『n月刊ラムダノートVol.5, No.1（2025）』に掲載された記事「自然数を作って学ぶLean言語」を基に内容を加筆して書籍として刊行したものです。
著者紹介
井上亜星
1997年滋賀県生まれ。京都大学理学部卒、京都大学大学院理学研究科数学・数理解析専攻修士課程修了。Proxima Technology勤務。2022年、就職を機にプログラミングを始めた。2023年8月ごろにLeanを知って夢中になり、Lean言語を日本に広めるべく活動していこうと決意する。最大の野望は、LeanをTeX言語に続いて、数学科の卒業生全員が知っているプログラミング言語にすること。Leanの日本語コミュニティlean-jaの立ち上げから関わっているほか、Leanのオンライン日本語リファレンス「Lean by Example」の執筆を行う。
目次
はじめに
第1章 ゼロから始めるLean言語入門
1.1 Leanの特徴
1.2 Leanによるプログラミングの例
第2章 Leanによる初めての証明
2.1 環境構築
2.2 自然数を定義して1 + 1 = 2を証明する
第3章 Leanにおける論理
3.1 命題論理
3.2 証明を楽にするコツ
3.3 述語論理
3.4 排中律と直観主義論理
3.5 選択原理
3.6 カリー・ハワード同型対応
3.7 依存型
第4章 帰納法で、足し算の性質を証明する
4.1 型クラスで見やすく綺麗に
4.2 帰納法で0 + n = nを証明する
4.3 等式変形による単純化を自動化する
4.4 足し算の交換法則と結合法則を解放する
4.5 帰納法を改善する
第5章 分配法則を証明し、マクロで再利用可能にする
5.1 掛け算を定義して交換法則、結合法則、分配法則を示す
5.2 分配法則を再利用可能にする
第6章 自然数の順序と、計算を利用する証明
6.1 a + b = a + c → b = cを証明する
6.2 順序を定義する
6.3 狭義順序を定義する
6.4 記法の展開を楽にする
6.5 足し算が順序を保つことを示す
6.6 a ≤ b → b ≤ a → a = bを示す
6.7 順序関係を決定可能にする
第7章 同値関係で割って整数を作る
7.1 同値関係
7.2 商とQuotient
7.3 整数を作る
第8章 Mathlibを使って整数の性質を証明する
8.1 Mathlibのインポート方法
8.2 代数系について
8.3 整数が足し算に関してアーベル群であることを利用する
8.4 整数は環
8.5 整数は前順序
8.6 整数は半順序
8.7 整数は足し算に関して可換な順序群
8.8 整数の順序関係は決定可能
8.9 整数は全順序
8.10 整数は順序環
第9章 grindタクティク
9.1 grindタクティクの使い方
9.2 MyNat再訪
おわりに
付録A 練習問題の解答
索引
