学部・大学院区分
Undergraduate / Graduate

理学部

時間割コード
Registration Code

0619100

科目区分
Course Category

専門科目
Specialized Courses

科目名　【日本語】
Course Title

数理解析・計算機数学Ⅲ

科目名　【英語】
Course Title

Computational Mathematics and Computer Science III

コースナンバリングコード
Course Numbering Code

担当教員　【日本語】
Instructor

GARRIGUE JACQUES ○

担当教員　【英語】
Instructor

GARRIGUE JACQUES ○

単位数
Credits

開講期・開講時間帯
Term / Day / Period

春水曜日１時限
春水曜日２時限
Spring Wed 1
Spring Wed 2

授業形態
Course style

講義及び演習

学科・専攻
Department / Program

多元数理科学研究科

必修・選択
Compulsory / 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

詳しい講義予定(シラバス)は第１回の講義で配布する．授業の前半を講義，後半を実習に充てる．

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

特に以下の内容を予定している．
* 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

特別な知識は要求しない。
4年生対象科目。
There are no prerequisites.