学部・大学院区分多・博前
時間割コード3211036
科目区分A類Ⅰ(基礎科目)
Category A-1
科目名 【日本語】数理解析・計算機数学概論Ⅱ
科目名 【英語】Introduction to Computational Mathmatics and Computer Scienc
コースナンバリングコード
担当教員 【日本語】GARRIGUE JACQUES ○
担当教員 【英語】GARRIGUE JACQUES ○
単位数2
開講期・開講時間帯秋 水曜日 1時限
秋 水曜日 2時限
Fall Wed 1
Fall Wed 2
授業形態
学科・専攻
多元数理科学研究科
必修・選択


授業の目的 【日本語】
証明の正しさとはどうやって保証されるものなのか。自分が書いた証明に自信が持てないことはないだろうか。
多くの人が確認すれば、少し安心できるようになるが、証明が非常に大きくなるとそれも困難である。
人間と違い、正しくプログラムされた計算機は絶対に間違わない。計算機に論理の基礎を教えると、証明に間違いや不足がないことをチェックしてもらえる。定理証明支援系のCoqはそういうプログラムの一つである。
また、証明が必要なのは数学だけではない。特に、計算機のプログラムも間違いが起きやすく、その正しさを保証するのはまた証明である。プログラムが大きくなると必然的に証明が大きくなるので、ここでも計算機による証明が期待される。

この講義ではCoqを使い、数学の証明や証明付きプログラムを書く方法を習う。同時にその裏付けである関数型プログラミングと型理論にも触れることになる。

Coqは型理論に基づいた論理を基礎とし、同じ言語の中でプログラムと証明が表現できる。証明も人間が書くが、正しさがコンピュータに保証される。プログラム抽出機能により、証明されたプログラムを普通にコンパイルできる形に変換でき、高速に実行することもできる。

証明対象はプログラムに限定されるわけではなく、通常の数学の定理も証明できる。有名なものとして、4色定理や群論のFeit-Thompson定理がCoqで証明された。型理論の表現力を活用し、数論・代数学や解析学も扱える。なお、今回の講義では、この二つの定理に使われたMathCompというライブラリーを最初から使う予定である。

Can we guarantee the correctness proofs? Have you never doubted your own proofs?
If many people check it, we can get some confidence, but this is hard to do for large proofs.

Contrary to people, correctly programmed computers never make errors. If we teach the basics of logic to a computer, it is able to check that there are no errors of gaps. This is all the more important as proofs are not needed in mathematics alone. In particular, bugs in programs are very common, and the surest way to avoid them is proofs of programs. Large programs require large proofs, so that we have to rely on computers to check them.

In this course we will learn to prove mathematical theorems and programs using the Coq proof assistant. This will also lead us to functional programming and type theory.

Coq uses a logic based on type theory, and is able to express mathematical proofs and programs using the same language. Humans have to write the proofs, but the computer checks them. Thanks to program extraction, proved programs can be compiled and run efficiently.

Proofs are not limited to programs, and reach many fields of mathematics. The four-colour theorem and the Feit-Thompson theorem have been proved in Coq. Type theory is expressive enough to describe number theory, algebra, or even analysis.
In this lecture we from the start use the MathComp library, which has been instrumental in proving those two theorems.
授業の目的 【英語】
到達目標 【日本語】
* 数理論理学とコンピュータによる証明の原理を理解する
* 具体的なプログラムの証明をする
* 数学の簡単な定理の証明をする
到達目標 【英語】
授業の内容や構成
詳しい講義予定(シラバス)は第1回の講義で配布する.授業の前半を講義,後半を実習に充てる.

この講義では新しいプログラミング言語と証明言語を習うことになるので,まずはその利用原理を教える.簡単な証明の書き方に慣れて来たら,プログラムの証明方法や様々な概念の扱い方を見る.

特に以下の内容を予定している.
* Coqによる関数型プログラミング
* 命題・述語論理とCoqの論理
* SSReflectの基礎
* 帰納法と帰納的な定義
* プログラムの証明・数学的な証明
* 論理や数学の進んだ証明(MathCompの進んだ利用など)

A detailed syllabus will be provided during the first lecture.
Each lecture spans two periods, the first one for classroom teaching, and the second one for practical application using computers.

Since we will learn a new programming and proof language, we will start from its principles. When one gets used to simple proofs, we will learn proofs of programs and various concepts.

The following topics shall be covered.

* Propositional/predicate logic and Coq's logic
* Fundamentals of SSReflect
* Functional programming in Coq
* Induction and inductive definitions
* Proof of programs and mathematical theorems
* Advanced proofs about logic and mathematics using MathComp


履修条件
特別な知識は要求しない。

There are no prerequisites.
関連する科目
数理解析・計算機数学Ⅰ
成績評価の方法と基準
毎回の課題および期末レポートに基づいて評価する。
教科書・テキスト
教科書は使わないが、以下の項目で参考書をあげる.
また,過去の講義のURLから様々な資料が入手できる.
http://www.math.nagoya-u.ac.jp/~garrigue/lecture/
参考書
* 萩原学, アフェルト・レナルド, 「Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化」, 森北出版, 2018.
* 大堀・ Garrigue・ 西村,コンピュータサイエンス入門:アルゴリズムとプログラミング言語,岩波書店 (1999)
* Assia Mahboubi等, Mathematical Components book, https://math-comp.github.io/mcb/
課外学習等(授業時間外学習の指示)
注意事項
-
他学科聴講の可否
他学科聴講の条件
歓迎します。
レベル
2
キーワード
型理論
定理証明支援系
プログラムの証明
数学的証明
Coq/MathComp/SSReflect
履修の際のアドバイス
コンピュータによる証明は難しいが、理解は深まる。
授業開講形態等
遠隔授業(オンデマンド型)で行う場合の追加措置