学部・大学院区分
Undergraduate / Graduate
多・博前
時間割コード
Registration Code
3211038
科目区分
Course Category
A類Ⅰ(基礎科目)
Category A-1
科目名 【日本語】
Course Title
数理解析・計算機数学概論Ⅳ
科目名 【英語】
Course Title
Introduction to Computational Mathmatics and Computer SciencⅠ
コースナンバリングコード
Course Numbering Code
担当教員 【日本語】
Instructor
GARRIGUE JACQUES ○
担当教員 【英語】
Instructor
GARRIGUE JACQUES ○
単位数
Credits
2
開講期・開講時間帯
Term / Day / Period
春 水曜日 1時限
春 水曜日 2時限
Spring Wed 1
Spring Wed 2
授業形態
Course style

学科・専攻
Department / Program
多元数理科学研究科
必修・選択
Required / Selected
選択


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

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

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

証明対象はプログラムに限定されるわけではなく、通常の数学の定理も証明できる。有名なものとして、4色定理や群論のFeit-Thompson定理がCoqで証明された。型理論の表現力を活用し、数論・代数学や解析学も扱える。なお、今回の講義では、この二つの定理に使われたMathCompというライブラリーを最初から使う予定である。
授業の目的 【英語】
Goals of the Course
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.
到達目標 【日本語】
Objectives of the Course(JPN))
* 数理論理学とコンピュータによる証明の原理を理解する
* 具体的なプログラムの証明をする
* 数学の簡単な定理の証明をする
到達目標 【英語】
Objectives of the Course
* Understand the principles of mathematical logic and computer-verified proofs
* Be able to prove properties of programs
* Be able to prove simple some mathematical theorems
授業の内容や構成
Course Content / Plan
詳しい講義予定(シラバス)は第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
履修条件
Course Prerequisites
特別な知識は要求しない。

There are no prerequisites.
関連する科目
Related Courses
数理解析・計算機数学Ⅰ
成績評価の方法と基準
Course Evaluation Method and Criteria
毎回の課題および期末レポートに基づいて評価する。
教科書・テキスト
Textbook
教科書は使わないが、以下の項目で参考書をあげる.
また,過去の講義のURLから様々な資料が入手できる.
http://www.math.nagoya-u.ac.jp/~garrigue/lecture/
参考書
Reference Book
* 萩原学, アフェルト・レナルド, 「Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化」, 森北出版, 2018.
* 大堀・ Garrigue・ 西村,コンピュータサイエンス入門:アルゴリズムとプログラミング言語,岩波書店 (1999)
* Assia Mahboubi等, Mathematical Components book, https://math-comp.github.io/mcb/
課外学習等(授業時間外学習の指示)
Study Load(Self-directed Learning Outside Course Hours)
この講義は実習時間がとってあるが、課題が時間内に終わらないことが多い。
自分のパソコンで環境を整え、課題を解く時間が必要になる。それに関して講義内で指示する。
注意事項
Notice for Students
他学科聴講の可否
Propriety of Other department student's attendance
他学科聴講の条件
Conditions of Other department student's attendance
歓迎します。
レベル
Level
2
キーワード
Keyword
型理論
定理証明支援系
プログラムの証明
数学的証明
Coq/MathComp/SSReflect
履修の際のアドバイス
Advice
コンピュータによる証明は難しいが、理解は深まる。
授業開講形態等
Lecture format, etc.
対面
遠隔授業(オンデマンド型)で行う場合の追加措置
Additional measures for remote class (on-demand class)