ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発 井上亜星(著) - ラムダノート 【利用可】 (連絡不要)
書店員向け情報 HELP
出版者情報
在庫ステータス
取引情報
ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発
- 出版社在庫情報
- 在庫あり
- 初版年月日
- 2025年9月4日
- 書店発売日
- 2025年9月4日
- 登録日
- 2025年9月2日
- 最終更新日
- 2026年8月12日
重版情報
| 2刷 | 出来予定日: 2026-09-05 |
| MORE | |
| LESS | |
紹介
ソフトウェアとして数学を扱いたい人、そして数学の力をソフトウェアに結びつけたい人にとってのプログラミング言語、Lean。本書では、動作するプログラムとして自然数と整数を構築することで、数学とソフトウェアがLeanによってどう結び付けられるかを確かめながら、Leanによりソフトウェアを開発するための基礎を身に付けます。
数学の形式化に興味がある数学者はもちろん、数学に挑戦したいプログラマーや、計算機科学の抽象概念を言葉ではなくコードとして理解したいエンジニアにも最適な一冊です。
目次
はじめに
第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 練習問題の解答
索引
上記内容は本書刊行時のものです。
