理論計算機科学入門― 有限と無限のあいだ
数学的理論から，AI・自動運転

蓮尾 一郎
国立情報学研究所 システム設計数理国際研究センター センター長
同 アーキテクチャ研究系 准教授
総合研究大学院大学 准教授
JST ERATO 蓮尾メタ数理システムデザインプロジェクト 研究総括

理論計算機科学入門 ― 有限と無限のあいだ
アウトライン
理論計算機科学とは― 有限と無限のせめぎあい

いろいろな無限― 対角線論法

オートマトン理論入門
包含問題を解くアルゴリズム ― 有限の方法で無限の対象を操作
オートマトンの表現能力― 有限性の限界

形式検証― オートマトンを用いたシステム品質保証

AI 時代の形式検証― 研究紹介2

理論計算機科学とは？
https://
commons.wikimedia.o

応用数学の一分野です

rg/wiki/File:%E5%8B%95%E6%9
1%A9%E6%93%A6%
E3%81%A8%E5%8A%9B%E5%AD%A6%
E7%9A%84%E3%82%A8%E3%83%8D%E
3%83%AB%E3%82%
AE%E3%83%BC.svg

By User:SilverStar - Own work,
CC BY 2.5, https://commons.wikimedia.org/w/
index.php?curid=14504053理論計算機科学とは？
https://
commons.wikimedia.o

応用数学の一分野です

rg/wiki/File:%E5%8B%95%E6%9
1%A9%E6%93%A6%
E3%81%A8%E5%8A%9B%E5%AD%A6%

理論物理学：

E7%9A%84%E3%82%A8%E3%83%8D%E
3%83%AB%E3%82%
AE%E3%83%BC.svg

物理現象の数学的研究

By User:SilverStar - Own work,
CC BY 2.5, https://commons.wikimedia.org/w/
index.php?curid=14504053理論計算機科学とは？
https://
commons.wikimedia.o

応用数学の一分野です

rg/wiki/File:%E5%8B%95%E6%9
1%A9%E6%93%A6%
E3%81%A8%E5%8A%9B%E5%AD%A6%

理論物理学：

E7%9A%84%E3%82%A8%E3%83%8D%E
3%83%AB%E3%82%
AE%E3%83%BC.svg

物理現象の数学的研究
理論経済学：
経済現象の数学的研究

By User:SilverStar - Own work,
CC BY 2.5, https://commons.wikimedia.org/w/
index.php?curid=14504053理論計算機科学とは？
https://
commons.wikimedia.o

応用数学の一分野です

rg/wiki/File:%E5%8B%95%E6%9
1%A9%E6%93%A6%
E3%81%A8%E5%8A%9B%E5%AD%A6%

理論物理学：

E7%9A%84%E3%82%A8%E3%83%8D%E
3%83%AB%E3%82%
AE%E3%83%BC.svg

物理現象の数学的研究
理論経済学：
経済現象の数学的研究
理論計算機科学：
情報現象の数学的研究

By User:SilverStar - Own work,
CC BY 2.5, https://commons.wikimedia.org/w/
index.php?curid=14504053理論計算機科学とは？
https://
commons.wikimedia.o

応用数学の一分野です

rg/wiki/File:%E5%8B%95%E6%9
1%A9%E6%93%A6%
E3%81%A8%E5%8A%9B%E5%AD%A6%

理論物理学：

E7%9A%84%E3%82%A8%E3%83%8D%E
3%83%AB%E3%82%
AE%E3%83%BC.svg

物理現象の数学的研究
理論経済学：
経済現象の数学的研究
理論計算機科学：
情報現象の数学的研究
数学基礎論：
数学者の営為の数学的研究
3

By User:SilverStar - Own work,
CC BY 2.5, https://commons.wikimedia.org/w/
index.php?curid=1450405

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, vonDefinition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ B
A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B···Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R)
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

original (discrete)···.

Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.
Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

automata
automata
program logic
safety by invariants(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.

e.2.7 Metamathematical Transfer Our approach is then explained as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e
4• we parametrize both a theory T (discrete,from software science) and a new

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, vonDefinition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ B
A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B···Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R)
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

やっ
ぱ
（時
り後
間が
で
あれ
ば）
···

.

Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.
Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

original (discrete)
automata
automata
program logic
safety by invariants(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.

e.2.7 Metamathematical Transfer Our approach is then explained as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e
4• we parametrize both a theory T (discrete,from software science) and a new

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, vonDefinition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ B
A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B···Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R)
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

やっ
ぱ
（時
り後
間が
で
あれ
ば）
···

.

Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.
Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

original (discrete)
automata
automata
program logic
safety by invariants(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.
Image by Robin
Higgins from Pixabay

e.2.7 Metamathematical Transfer Our approach is then explained
数学者as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e
4• we parametrize both a theory T (discrete,from software science) and a new

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, vonDefinition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ B
A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B···Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R)
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

やっ
ぱ
（時
り後
間が
で
あれ
ば）
···

.
Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.

Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

メタ数学者
original (discrete)

automata
automata
program logic
Image by Robinsafety by invariants

Higgins from Pixabay(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.
Image by Robin
Higgins from Pixabay

e.2.7 Metamathematical Transfer Our approach is then explained
数学者as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e
4• we parametrize both a theory T (discrete,from software science) and a new

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, von
どんなにがんばっても
Definition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ Bそれは証明できないよ…

A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B···Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R)
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

やっ
ぱ
（時
り後
間が
で
あれ
ば）
···

.
Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.

Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

メタ数学者
original (discrete)

automata
automata
program logic
Image by Robinsafety by invariants

Higgins from Pixabay(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.
Image by Robin
Higgins from Pixabay

e.2.7 Metamathematical Transfer Our approach is then explained
数学者as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e
4• we parametrize both a theory T (discrete,from software science) and a new

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, von
どんなにがんばっても
Definition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ Bそれは証明できないよ…

A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B…ということを······Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R) 私は証明できます！
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

やっ
ぱ
（時
り後
間が
で
あれ
ば）

.
Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.

Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

メタ数学者
original (discrete)

automata
automata
program logic
Image by Robinsafety by invariants

Higgins from Pixabay(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.
Image by Robin
Higgins from Pixabay

e.2.7 Metamathematical Transfer Our approach is then explained
数学者as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e
4• we parametrize both a theory T (discrete,from software science) and a new

理論計算機科学とは？
応用数学の一分野です
純粋数学「応用する気のない数学」「応用できない数学」「役に立たない数学」とは違う本人にその気がなくても，時々応用で大ホームランを飛ばす
あなどれない！！

5理論計算機科学とは？
応用数学の一分野ですやっぱ「応用する気のない数学」（時「応用できない数学」「役に立たない数学」とは違う
り後間がで本人にその気がなくても，
あれば
時々応用で大ホームランを飛ばす）
あなどれない！！
純粋数学

5いろいろな数学いろいろな数学いろいろな数学いろいろな数学いろいろな数学

p

p^q
p

r

r
(p ^ q)(pr)

r(p ^ q)r

いろいろな数学
今日は理論計算機科学で使う数学を見てみます

p

p^q
p

r

r
(p ^ q)(pr)

r(p ^ q)r

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit>

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit<latexit

理論計算機科学とは？
A

速さ（アルゴリズム，計算量理論）

正しさ（「バグがないか？」．形式手法，プログラミング言語理論）

使う数学：

論理学，代数学，グラフ理論など

離散的（
連続的）

有限（記号の世界）と無限（イデアの世界）をはっきり重視
7

AB

https://www.publicdomainpictures.net/en/view-

image.php?image=42208&picture=computer-silhouette

RRZEicons, CC BY-SA 3.0

https://publicdomainvectors.org/en/free-clipart/Generic-computer-chip-vector-image/13455.html

計算機，計算機システムの振る舞いを数学的に研究
https://svgsilh.com/image/294276.html

Bsha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit>

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit<latexit

理論計算機科学とは？
A

使う数学：

論理学，代数学，グラフ理論など

離散的（
連続的）

有限（記号の世界）と無限（イデアの世界）をはっきり重視
7

A
B
B

https://www.publicdomainpictures.net/en/view-

image.php?image=42208&picture=computer-silhouette

RRZEicons, CC BY-SA 3.0

https://publicdomainvectors.org/en/free-clipart/Generic-computer-chip-vector-image/13455.html

計算機，計算機システムの振る舞いを数学的に研究
https://svgsilh.com/image/294276.html

速さ（アルゴリズム，計算量理論）

正しさ（「バグがないか？」．形式手法，プログラミング言語理論）

人間の手の届かない無限を，有限の記号列で表現

理論計算機科学入門 ― 有限と無限のあいだ
アウトライン
理論計算機科学とは― 有限と無限のせめぎあい

いろいろな無限― 対角線論法

オートマトン理論入門
包含問題を解くアルゴリズム ― 有限の方法で無限の対象を操作
オートマトンの表現能力― 有限性の限界

形式検証― オートマトンを用いたシステム品質保証

AI 時代の形式検証― 研究紹介8いろいろな「無限」
自然数

0, 1, 2, ...

整数..., -2, -1, 0, 1, 2, ...

p
有理数

実数

「分数」 q
循環小数
有理数 ＋ 無理数
π= 3.141592... とかいろいろな「無限」
自然数含まれる整数
含まれる

有理数
含まれる

実数

0, 1, 2, ...
..., -2, -1, 0, 1, 2, ...

p「分数」 q
循環小数
有理数 ＋ 無理数
π= 3.141592... とかいろいろな「無限」
自然数含まれる整数
含まれる

有理数
含まれる

実数

0, 1, 2, ...
..., -2, -1, 0, 1, 2, ...

p「分数」 q
循環小数
有理数 ＋ 無理数
π= 3.141592... とか「個数」は本当に違うの？

いろいろな「無限」
自然数

0, 1, 2, ...

整数..., -2, -1, 0, 1, 2, ...

p
有理数

実数

「分数」 q
循環小数
有理数 ＋ 無理数
π= 3.141592... とか「個数」は本当に違うの？

いろいろな「無限」
定義 1対1対応が付くとき，「個数が同じ」（「濃度が同じ」という）いろいろな「無限」
もれがないペアリング

定義 1対1対応が付くとき，「個数が同じ」（「濃度が同じ」という）いろいろな「無限」
もれがないペアリング

定義 1対1対応が付くとき，「個数が同じ」（「濃度が同じ」という）自然数と整数は，濃度が同じ

いろいろな「無限」
もれがないペアリング

定義 1対1対応が付くとき，「個数が同じ」（「濃度が同じ」という）自然数と整数は，濃度が同じ
...

-2

-1

0

1

2

...

いろいろな「無限」
もれがないペアリング

定義 1対1対応が付くとき，「個数が同じ」（「濃度が同じ」という）自然数と整数は，濃度が同じ
...

-2

-1

0

0

1

2

...

いろいろな「無限」
もれがないペアリング

定義 1対1対応が付くとき，「個数が同じ」（「濃度が同じ」という）自然数と整数は，濃度が同じ
...

-2

-1

0

1

0

1

2

...

いろいろな「無限」
もれがないペアリング

定義 1対1対応が付くとき，「個数が同じ」（「濃度が同じ」という）自然数と整数は，濃度が同じ
...

-2

-1

0

1

2

0

1

2

...

いろいろな「無限」
もれがないペアリング

定義 1対1対応が付くとき，「個数が同じ」（「濃度が同じ」という）自然数と整数は，濃度が同じ
...

-2

-1

0

1

2

2

0

1

3

...

いろいろな「無限」
もれがないペアリング

定義 1対1対応が付くとき，「個数が同じ」（「濃度が同じ」という）自然数と整数は，濃度が同じ
...

-2

-1

0

1

2

4

2

0

1

3

...

いろいろな「無限」
もれがないペアリング

定義 1対1対応が付くとき，「個数が同じ」（「濃度が同じ」という）自然数と整数は，濃度が同じ
...

-2

-1

0

1

2

...

...

4

2

0

1

3

...

いろいろな「無限」
有理数と自然数も，濃度が同じ
1/1

2/1

3/1

...

1/2

2/2

3/2

...

1/3

2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ
1/1

2/1

3/1

...

1/2

2/2

3/2

...

1/3

2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ

01/1

2/1

3/1

...

1/2

2/2

3/2

...

1/3

2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ

01/1

1 2/1

3/1

...

1/2

2/2

3/2

...

1/3

2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ

01/1

1 2/1

3/1

...

21/2

2/2

3/2

...

1/3

2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ

01/1

1 2/1

3 3/1

...

21/2

2/2

3/2

...

1/3

2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ

01/1

1 2/1

3 3/1

...

21/2

2/2

3/2

...

41/3

2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ

01/1

1 2/1

3 3/1

5 ...

21/2

2/2

3/2

...

41/3

2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ

01/1

1 2/1

3 3/1

5 ...

21/2

2/2

6 3/2

...

41/3

2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ

01/1

1 2/1

3 3/1

5 ...

21/2

2/2

6 3/2

...

41/3

7 2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ

01/1

1 2/1

3 3/1

5 ...

21/2

2/2

6 3/2

...

41/3

7 2/3

3/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
有理数と自然数も，濃度が同じ

01/1

1 2/1

3 3/1

5 ...

21/2

2/2

6 3/2

...

41/3

7 2/3

113/3

...

⋮

⋮

⋮

⋱

いろいろな「無限」
自然数

0, 1, 2, ...

整数..., -2, -1, 0, 1, 2, ...

p
有理数

実数

「分数」 q
循環小数
有理数 ＋ 無理数
π= 3.141592... とか「個数」は本当に違うの？

いろいろな「無限」
自然数

0, 1, 2, ...

整数..., -2, -1, 0, 1, 2, ...

p
有理数

実数

「分数」 q
循環小数
有理数 ＋ 無理数
π= 3.141592... とか「個数」は本当に違うの？

対角線論法定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．

対角線論法定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

対角線論法定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮

0 . 1 8 2 6 ...
0 . 4 0 3 7 ...
0 . 2 1 5 6 ...
0 . 3 1 4 1 ...
⋮ ⋮ ⋮ ⋮ ⋱

対角線論法定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮

0 . 1 8 2 6 ...
0 . 4 0 3 7 ...
0 . 2 1 5 6 ...
0 . 3 1 4 1 ...
⋮ ⋮ ⋮ ⋮ ⋱

対角線論法定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮

0 . 1 8 2 6 ...
0 . 4 0 3 7 ...
0 . 2 1 5 6 ...
0 . 3 1 4 1 ...
⋮ ⋮ ⋮ ⋮ ⋱対角線を見て，実数0.1051... を作る

対角線論法定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮

0 . 1 8 2 6 ...
0 . 4 0 3 7 ...

対角線を見て，実数0.1051... を作る

0 . 2 1 5 6 ...

各桁の数字をずらして，

0 . 3 1 4 1 ...

0.2162... を考えよう⋮ ⋮ ⋮ ⋮ ⋱

対角線論法定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮

0 . 1 8 2 6 ...
0 . 4 0 3 7 ...

対角線を見て，実数0.1051... を作る

0 . 2 1 5 6 ...

各桁の数字をずらして，

0 . 3 1 4 1 ...

0.2162... を考えよう⋮ ⋮ ⋮ ⋮ ⋱0.2162... は何番目の実数？

対角線論法定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮
k

0 . 1 8 2 6 ...
0 . 4 0 3 7 ...

対角線を見て，実数0.1051... を作る

0 . 2 1 5 6 ...

各桁の数字をずらして，

0 . 3 1 4 1 ...

0.2162... を考えよう⋮ ⋮ ⋮ ⋮ ⋱0.2162... は何番目の実数？

0 . 2 16 2…

対角線論法定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮
k

0 . 1 8 2 6 ...
0 . 4 0 3 7 ...

対角線を見て，実数0.1051... を作る

0 . 2 1 5 6 ...

各桁の数字をずらして，

0 . 3 1 4 1 ...

0.2162... を考えよう⋮ ⋮ ⋮ ⋮ ⋱0.2162... は何番目の実数？

0 . 2 16 2…

対角線論法定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮
k

0 . 1 8 2 6 ...
0 . 4 0 3 7 ...

対角線を見て，実数0.1051... を作る

0 . 2 1 5 6 ...

各桁の数字をずらして，

0 . 3 1 4 1 ...

0.2162... を考えよう⋮ ⋮ ⋮ ⋮ ⋱0.2162... は何番目の実数？

0 . 2 16 2…

➜ ない！ （矛盾）

対角線論法（予備スライド）
定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮

0 . 1 8 2 6 ...
0 . 4 0 3 7 ...
0 . 2 1 5 6 ...
0 . 3 1 4 1 ...
⋮ ⋮ ⋮ ⋮ ⋱0.2162... は何番目？
➜ ない！ （矛盾）

対角線から作られる実数（の10進表記）を
0. n1 n2 n3 …としよう．
あらたな実数 0. m1 m2 m3 … を，n1 m1 , n2 m2 , … （＊）となるように作る（たとえば，数字をひとつずらそう）
0. m1 m2 m3 … は左の対応表に現れるはずk 番目としよう．
しかし，すると0. m1 m2 m3 … が対角線とぶつかるところの数字 mk は，nk と同じはず➜ 上の（＊）に矛盾！ 証明終わり．

対角線論法（予備スライド）
定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮
k

0 . 1 8 2 6 ...
0 . 4 0 3 7 ...
0 . 2 1 5 6 ...
0 . 3 1 4 1 ...
⋮ ⋮ ⋮ ⋮ ⋱0 . m1 m2 m3 …

0.2162... は何番目？
➜ ない！ （矛盾）

対角線から作られる実数（の10進表記）を
0. n1 n2 n3 …としよう．
あらたな実数 0. m1 m2 m3 … を，n1 m1 , n2 m2 , … （＊）となるように作る（たとえば，数字をひとつずらそう）
0. m1 m2 m3 … は左の対応表に現れるはずk 番目としよう．
しかし，すると0. m1 m2 m3 … が対角線とぶつかるところの数字 mk は，nk と同じはず➜ 上の（＊）に矛盾！ 証明終わり．

対角線論法（予備スライド）
定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮
k

0 .
0 .
0 .
0 .

n1
1 8 2 6 ...
n2
4 0 3 7 ...
n3
2 1 5 6 ...
n4
3 1 4 1 ...

あらたな実数 0. m1 m2 m3 … を，n1 m1 , n2 m2 , … （＊）となるように作る（たとえば，数字をひとつずらそう）⋮ ⋮ ⋮ ⋮ ⋱0. m1 m2 m3 … は左の対応表に現れるはずk 番目としよう．

0 . m1 m2 m3 …

0.2162... は何番目？
➜ ない！ （矛盾）

対角線から作られる実数（の10進表記）を
0. n1 n2 n3 …としよう．

しかし，すると0. m1 m2 m3 … が対角線とぶつかるところの数字 mk は，nk と同じはず➜ 上の（＊）に矛盾！ 証明終わり．

対角線論法（予備スライド）
定理 実数と自然数は，濃度がちがう．
つまり，1対1対応がない．
証明（背理法）仮に，1対1対応があるとしよう．（矛盾を導く）

0
1
2
3
⋮
k

0 .
0 .
0 .
0 .

n1
1 8 2 6 ...
n2
4 0 3 7 ...
n3
2 1 5 6 ...
n4
3 1 4 1 ...

あらたな実数 0. m1 m2 m3 … を，n1 m1 , n2 m2 , … （＊）となるように作る（たとえば，数字をひとつずらそう）⋮ ⋮ ⋮ ⋮ ⋱0. m1 m2 m3 … は左の対応表に現れるはずk 番目としよう．

0 . m1 m2 m3 …

0.2162... は何番目？
➜ ない！ （矛盾）

対角線から作られる実数（の10進表記）を
0. n1 n2 n3 …としよう．

しかし，すると0. m1 m2 m3 … が対角線とぶつかるところの数字 mk は，nk と同じはず➜ 上の（＊）に矛盾！ 証明終わり．

対角線論法
定義
集合 X の power set P(X) とは，X の部分集合全体の集合
例 X = {a, b, c} なら，
P(X) = { {}, {a}, {b}, {c}, {b,c}, {c,a}, {a,b}, {a,b,c} }練習問題
有限集合 X （元は n 個）に対して，P(X) の元の個数は？

対角線論法
定義
集合 X の power set P(X) とは，X の部分集合全体の集合
例 X = {a, b, c} なら，
P(X) = { {}, {a}, {b}, {c}, {b,c}, {c,a}, {a,b}, {a,b,c} }練習問題
有限集合 X （元は n 個）に対して，P(X) の元の個数は？
答え： 2n 個

対角線論法定理 任意の集合 X に対して，X と P(X) の間に1対1対応はない

対角線論法定理 任意の集合 X に対して，X と P(X) の間に1対1対応はない
証明（背理法）仮に，1対1対応 f: X ➔ P(X) があるとしよう．（矛盾を導く）（アイデア： ヤバそうな P(X) の元を持ってくる）
U = {x | x は f(x) に含まれない } と定義する．U は P(X) の元．
f: X ➔ P(X) は1対1対応なので，X の元 u であって，f(u) = Uとなるものが存在する．ここで，u が U に含まれるかを考える．
u が U に含まれる場合： f(u) = U より，u は f(u) に含まれる．
U の定義より，u は U に含まれない ➜ 矛盾！
u が U に含まれない場合： f(u) = U より，u は f(u) に含まれない．
U の定義より，u は U に含まれる ➜ 矛盾！

対角線論法なんかモヤモヤする．．．
➜ 本質は「嘘つきのパラドックス」と同じ定理 任意の集合 X に対して，X と P(X) の間に1対1対応はない
証明（背理法）仮に，1対1対応 f: X ➔ P(X) があるとしよう．（矛盾を導く）（アイデア： ヤバそうな P(X) の元を持ってくる）
U = {x | x は f(x) に含まれない } と定義する．U は P(X) の元．
f: X ➔ P(X) は1対1対応なので，X の元 u であって，f(u) = Uとなるものが存在する．ここで，u が U に含まれるかを考える．
u が U に含まれる場合： f(u) = U より，u は f(u) に含まれる．
U の定義より，u は U に含まれない ➜ 矛盾！
u が U に含まれない場合： f(u) = U より，u は f(u) に含まれない．
U の定義より，u は U に含まれる ➜ 矛盾！

うそつきのパラドックス

うそつきのパラドックス「私の言っていることはウソである」

うそつきのパラドックス「私の言っていることはウソである」「クレタ人はうそつきばっかりだ」『ところであなた，ご出身は？』「クレタです！」うそつきのパラドックス

Bさんの言ってることは本当ですA

Aさんの言ってることはウソですBうそつきのパラドックス「私の言っていることはウソである」➜ 否定的なメタ言及
対角線論法の本質．
対角線論法はいろんなところで使われる
自然数と実数の濃度の違いの証明
停止問題の決定不可能性の証明
ゲーデルの不完全性定理の証明

理論計算機科学入門 ― 有限と無限のあいだ
アウトライン
理論計算機科学とは― 有限と無限のせめぎあい

いろいろな無限― 対角線論法

オートマトン理論入門
包含問題を解くアルゴリズム ― 有限の方法で無限の対象を操作
オートマトンの表現能力― 有限性の限界

形式検証― オートマトンを用いたシステム品質保証

AI 時代の形式検証― 研究紹介20

オートマトン
機械仕掛けの自動人形
左：野坂オートマタ美術館所蔵（静岡県伊東市）「手紙を書くピエロ」
レオポール・ランベール
作
https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A1%E3%82%A4%E3%83%AB:Pierrot_%C3%A9crivain.jpg

1900年… この話ではありません
21

有限オートマトン
計算モデルのうち，単純なものの一つ
計算モデル：「計算とは何か？」の数学的定義
さまざまな計算モデル

1

有限オートマトン

0
0

<…

1

< プッシュダウン・オートマトン<…
< チューリングマシン

22

有限オートマトン
計算モデルのうち，単純なものの一つ
計算モデル：「計算とは何か？」の数学的定義
さまざまな計算モデル

1

有限オートマトン

0
0

<…

1

< プッシュダウン・オートマトン<…
< チューリングマシン

22

Church の提題：
「チューリングマシンでできることを『計算』と呼ぼう」

有限オートマトン
有限個の状態 （ここでは2個）
状態間の遷移（矢印）1

各遷移は文字でラベル付け（ここでの文字は0,1）

0
0

1

初期状態
（左の状態．矢印で表現）状態の「色付け」．2色：○： 非受理状態◎： 受理状態23

有限オートマトン
機能：有限長の文字列を読んで，「受理 (OK!)」あるいは「非受理 (NG!)」と言う

1
0
0

1

初期状態から，文字列に沿って遷移をたどっていって，
最後にたどり着いた状態が◎ なら「受理」○ なら「非受理」
24

有限オートマトン
機能：有限長の文字列を読んで，「受理 (OK!)」あるいは「非受理 (NG!)」と言う

10
000 は非受理1

初期状態から，文字列に沿って遷移をたどっていって，
最後にたどり着いた状態が◎ なら「受理」○ なら「非受理」
24

有限オートマトン
機能：有限長の文字列を読んで，「受理 (OK!)」あるいは「非受理 (NG!)」と言う

10
000 は非受理
001 は受理1

初期状態から，文字列に沿って遷移をたどっていって，
最後にたどり着いた状態が◎ なら「受理」○ なら「非受理」
24

有限オートマトン
機能：有限長の文字列を読んで，「受理 (OK!)」あるいは「非受理 (NG!)」と言う

1
0
0

1

00 は非受理
1100 は?
001 は受理

初期状態から，文字列に沿って遷移をたどっていって，
最後にたどり着いた状態が◎ なら「受理」○ なら「非受理」
24

有限オートマトン
機能：有限長の文字列を読んで，「受理 (OK!)」あるいは「非受理 (NG!)」と言う

1
0
0

1

00 は非受理
1100 は?
001 は受理

初期状態から，文字列に沿って遷移をたどっていって，
最後にたどり着いた状態が空列（長さ0の文字列）は？

◎ なら「受理」○ なら「非受理」
24

有限オートマトン
機能：有限長の文字列を読んで，「受理 (OK!)」あるいは「非受理 (NG!)」と言う

1
0
0

1

00 は非受理
1100 は?
001 は受理… 一般的な特徴づけができるか

初期状態から，文字列に沿って遷移をたどっていって，
最後にたどり着いた状態が空列（長さ0の文字列）は？

◎ なら「受理」○ なら「非受理」
24

有限状態オートマトン
機能：
有限の文字列を読んで，「受理 (OK!)」あるいは「非受理 (NG!)」と言う

1
0
0

1

初期状態から，文字列に沿って遷移をたどっていって，最後にたどり着いた状態が◎ なら「受理」○ なら「非受理」
25

有限状態オートマトン
機能：
有限の文字列を読んで，「受理 (OK!)」あるいは「非受理 (NG!)」と言う

1
0
0

1

文字列 w が受理される⇔
w の最後の文字が 1

初期状態から，文字列に沿って遷移をたどっていって，最後にたどり着いた状態が◎ なら「受理」○ なら「非受理」
25

有限状態オートマトン
機能：
有限の文字列を読んで，「受理 (OK!)」あるいは

1「非受理 (NG!)」と言う

00

すなわち，オートマトン M は，

1

文字列の集合 L(M) を表現する（ひきおこす）．

文字列 w が受理される⇔
w の最後の文字が 1

ここでは，
L(M) = { w1 : w は任意の文字列}= {1, 01, 11,001, 011, 101, 111,…}26

有限状態オートマトン
M は有限．
特に，計算機上で表現・処理可能

States: 2
Start: 0
Acceptance: 1
char: "0" "1"--BODY-State: 0
[0] 0
[1] 1
State: 1
[0] 0
[1] 1
--END--

機能：
有限の文字列を読んで，「受理 (OK!)」あるいは

1「非受理 (NG!)」と言う

00

すなわち，オートマトン M は，

1

文字列の集合 L(M) を表現する（ひきおこす）．

文字列 w が受理される⇔
w の最後の文字が 1

ここでは，
L(M) = { w1 : w は任意の文字列}= {1, 01, 11,001, 011, 101, 111,…}26

有限状態オートマトン
M は有限．
特に，計算機上で表現・処理可能

States: 2
Start: 0
Acceptance: 1
char: "0" "1"--BODY-State: 0
[0] 0
[1] 1
State: 1
[0] 0
[1] 1
--END--

機能：

L(M) は（一般には）は無限集合．
有限の文字列を読んで，計算機上で（そのままでは）表現・処理不可能「受理 (OK!)」あるいは

1「非受理 (NG!)」と言う

00

すなわち，オートマトン M は，

1

文字列の集合 L(M) を表現する（ひきおこす）．

文字列 w が受理される⇔
w の最後の文字が 1

ここでは，
L(M) = { w1 : w は任意の文字列}= {1, 01, 11,001, 011, 101, 111,…}
26

有限オートマトン
つまり…
無限の数学的実体 L(M) を有限のフォーマリズムであるオー
トマトンMが表現している

1
0
0

有限と無限のせめぎあい
1

これからの話題
オートマトンのアルゴリズム処理（「有限で良かった！」）
オートマトンの表現能力の限界
27

理論計算機科学入門 ― 有限と無限のあいだ
アウトライン
理論計算機科学とは― 有限と無限のせめぎあい

いろいろな無限― 対角線論法

オートマトン理論入門
包含問題を解くアルゴリズム ― 有限の方法で無限の対象を操作
オートマトンの表現能力― 有限性の限界

形式検証― オートマトンを用いたシステム品質保証

AI 時代の形式検証― 研究紹介28

オートマトンの包含問題
0

M
1

Mʼ
1

1

0

0
0

0

1

クイズ 次は成り立つ？ L(M) ⊆ L(M′)

291オートマトンの包含問題
0

M
1

Mʼ
1

1

0

0
0

0

1

クイズ 次は成り立つ？ L(M) ⊆ L(M′)
答え Yes!
L(M) = { 11 で終わる文字列全体 }L(Mʼ) = { 1 で終わる文字列全体 }291

オートマトンの包含問題
0

M
1

Mʼ
1

1

0

0
0

0

1

1

クイズ 次は成り立つ？ L(M) ⊆ L(M′)
答え Yes!
L(M) = { 11 で終わる文字列全体 }L(Mʼ) = { 1 で終わる文字列全体 }
29

人間の頭を
使った答え

包含問題を自動で解きたい
0

M
1

1

0
1

0

Mʼ
1

L(M) ⊆ L(M′)

001

Yes/No30

包含問題を自動で解きたいM

10,000状態

Mʼ

L(M) ⊆ L(M′)

20,000状態

Yes/No31

問題
入力：
有限オートマトン M, Mʼ
出力： 次が成り立つかどうか

L(M) ⊆ L(M′)

32

問題
入力：
有限オートマトン M, Mʼ
出力： 次が成り立つかどうか

L(M) ⊆ L(M′)（間違った答え）
文字列 w それぞれについて，「w が M に受理されるならば，w は Mʼ にも受理される」ことを確かめる

32

問題
入力：
有限オートマトン M, Mʼ
出力： 次が成り立つかどうか

L(M) ⊆ L(M′)

w は無限個ある．一方，人生は有限（間違った答え）（cf. 「数え上げおねえさん」で検索）
文字列 w それぞれについて，「w が M に受理されるならば，w は Mʼ にも受理される」ことを確かめる

32

問題
入力：
有限オートマトン M, Mʼ
出力： 次が成り立つかどうか

L(M) ⊆ L(M′)

w は無限個ある．一方，人生は有限（間違った答え）（cf. 「数え上げおねえさん」で検索）
文字列 w それぞれについて，「w が M に受理されるならば，w は Mʼ にも受理される」ことを確かめる
L(M), L(Mʼ) は無限集合 ➜ 直接操作できない
アイデア： 有限の表現たる M, Mʼ を使ってがんばる
32

問題
入力：
有限オートマトン M, Mʼ
出力： 次が成り立つかどうか

L(M) ⊆ L(M′)
以下，アルゴリズムの詳細を説明します．
材料1, 2, 3 の組み合わせ
材料1： 空判定
材料2： 同期積
材料3： 言語反転
数式多数 ➜ わかりにくいかも
寝ちゃった方は起こしますので，ご安心を :)
33

材料1：
空判定
入力：
有限オートマトン M
出力： 次が成り立つかどうか

L(M) = ∅

34

材料1：
空判定
入力：
有限オートマトン M

空集合（からっぽ）

出力： 次が成り立つかどうか

L(M) = ∅

34

材料1：
空判定
入力：
有限オートマトン M

空集合（からっぽ）

出力： 次が成り立つかどうか

L(M) = ∅オートマトン M はどの文字列も受理しない

34

材料1：
空判定
入力：
有限オートマトン M

空集合（からっぽ）

出力： 次が成り立つかどうか

L(M) = ∅オートマトン M はどの文字列も受理しない「初期状態（→○）から受理状態（◎）に辿り着けない」と同じ

34

材料1：
空判定
入力：
有限オートマトン M

空集合（からっぽ）

出力： 次が成り立つかどうか

L(M) = ∅オートマトン M はどの文字列も受理しない「初期状態（→○）から受理状態（◎）に辿り着けない」と同じ「初期状態（→○）から辿り着ける状態」を列挙して（有限だからできる），◎が含まれないかどうかチェック34

35

「初期状態（→○）から辿り着ける状態」を列挙して（有限だからできる），◎が含まれないかどうかチェック

35

材料1：
空判定（詳細）入力：
有限オートマトン M
出力： 次が成り立つかどうか

L(M) = ∅36

材料1：
空判定（詳細）入力：
有限オートマトン M
出力： 次が成り立つかどうか

L(M) = ∅グラフ探索アルゴリズムで解ける
Sn = { 初期状態から n 歩以内でS0 = { 初期状態 } とする

到達できる状態全体 }n = 0, 1, 2, … に対して，
Sn+1 = Sn ∪ { Sn から一歩で到達できる状態全体 }とする

増えなくなったら（Sn+1 = Sn になったら）終わり
そのとき，Sn = { 初期状態から到達可能な状態全体 }Sn ⋂ { 受理状態 } = ∅かどうかを調べればよい
36

材料1：
空判定（詳細）入力：
必ず終わる．なぜか？
有限オートマトン M… 終わらないとすると，状態集合
出力： 次が成り立つかどうか

L(M) = ∅S0, S1, S2, … はどんどん，際限なく大きくなる．

グラフ探索アルゴリズムで解ける

しかし状態は有限個しかないから，これは不可能
Sn = { 初期状態から n 歩以内で
S
=
{
初期状態
}
とする
0
➜ 有限オートマトンでよかった！！
到達できる状態全体 }n = 0, 1, 2, … に対して，
Sn+1 = Sn ∪ { Sn から一歩で到達できる状態全体 }とする

増えなくなったら（Sn+1 = Sn になったら）終わり
そのとき，Sn = { 初期状態から到達可能な状態全体 }Sn ⋂ { 受理状態 } = ∅かどうかを調べればよい
37

材料2：
オートマトンの同期積
入力： 有限オートマトン M, Mʼ
出力：L(M ⊗ M′) = L(M) ∩ L(M′)となるオートマトン M ⊗ M′

材料2：
オートマトンの同期積
入力： 有限オートマトン M, Mʼ
出力：L(M ⊗ M′) = L(M) ∩ L(M′)となるオートマトン M ⊗ M′

材料2：
オートマトンの同期積
入力： 有限オートマトン M, Mʼ
出力：L(M ⊗ M′) = L(M) ∩ L(M′)となるオートマトン M ⊗ M′

M ⊗ M′ は，Mと Mʼ の両方に受理される文字列（そしてそれらのみ）を受理

材料2：
オートマトンの同期積
入力： 有限オートマトン M, Mʼ
出力：L(M ⊗ M′) = L(M) ∩ L(M′)となるオートマトン M ⊗ M′

M ⊗ M′ は，Mと Mʼ の両方に受理される文字列（そしてそれらのみ）を受理

文字列集合の交わり intersection

L(M) ∩ L(M′) を表現

材料2：
オートマトンの同期積
入力： 有限オートマトン M, Mʼ
出力：L(M ⊗ M′) = L(M) ∩ L(M′) 文字列集合の交わり intersectionとなるオートマトン M ⊗ M′

L(M) ∩ L(M′) を表現

材料2：
オートマトンの同期積
入力： 有限オートマトン M, Mʼ
出力：L(M ⊗ M′) = L(M) ∩ L(M′) 文字列集合の交わり intersection
L(M) ∩ L(M′) を表現となるオートマトン M ⊗ M′

作り方： 「2つのオートマトンを両方同時に動かす」

M

s

a

⟹ M ⊗ Mʼ

Mʼ

t

s, M
s’

a

s’

t, t’

a

t’

材料2：
オートマトンの同期積
入力： 有限オートマトン M, Mʼ
出力：L(M ⊗ M′) = L(M) ∩ L(M′) 文字列集合の交わり intersection
L(M) ∩ L(M′) を表現となるオートマトン M ⊗ M′

作り方： 「2つのオートマトンを両方同時に動かす」

M

s

a

⟹ M ⊗ Mʼ
クイズ：
初期状態は？ 受理状態は？

Mʼ

t

s, M
s’

a

s’

t, t’

a

t’

材料3：
オートマトンの言語反転
入力： 有限オートマトン M
出力：c

L(M ) = L(M) = Σ*∖L(M)cとなるオートマトン M

Mc と M とでは，受理と非受理がひっくり返っている

40

材料3：
オートマトンの言語反転
入力： 有限オートマトン M
出力：c

L(M ) = L(M) = Σ*∖L(M)cとなるオートマトン M
作り方：○と◎を反転Mc と M とでは，受理と非受理がひっくり返っている

40

材料3：
オートマトンの言語反転
入力： 有限オートマトン M
出力：c

L(M ) = L(M) = Σ*∖L(M)cとなるオートマトン M
作り方：○と◎を反転Mc と M とでは，受理と非受理がひっくり返っている
Warning! （詳細，念の為）
決定性オートマトンだからこれでOK
非決定性オートマトンではダメ（一度決定化が必要）
40

解答：
包含関係を解く
0

L(M ) ✓ L(M )() L(M ) \ L(M 0 ) = ;() L(M ⌦ (M 0 )c ) = ;

L(M′)

L(M’)
L(M)

アルゴリズム：(Mʼ)c を作る (○ ◎，材料３)M ⊗ (M′)c を作る （オートマトンの同期積，材料２）M ⊗ (M′)c の空判定（◎が到達可能かどうか探索，材料１）41

理論計算機科学入門 ― 有限と無限のあいだ
アウトライン
理論計算機科学とは― 有限と無限のせめぎあい

いろいろな無限― 対角線論法

オートマトン理論入門
包含問題を解くアルゴリズム ― 有限の方法で無限の対象を操作
オートマトンの表現能力― 有限性の限界

形式検証― オートマトンを用いたシステム品質保証

AI 時代の形式検証― 研究紹介42

有限状態オートマトン
機能：
有限の文字列を読んで，「受理 OK!」あるいは「非受理 NG!」と言う

1
0
0

1

すなわち，オートマトン Mは，文字列の集合 L(M) を表現する（ひきおこす）．
ここでは，
L(M) ={ w1 : w は任意の文字列}43

有限状態オートマトン
オートマトン M は，文字列の集合 L(M) を表現する．
L(M) = { Mに受理される文字列全体 }44

有限状態オートマトン
オートマトン M は，文字列の集合 L(M) を表現する．
L(M) = { Mに受理される文字列全体 }逆に，次は成り立つか？
かってな文字列集合 L について，
これを表現するオートマトン M がある（L = L(M)）

44

有限状態オートマトン
オートマトン M は，文字列の集合 L(M) を表現する．
L(M) = { Mに受理される文字列全体 }答え： 成立しない！

逆に，次は成り立つか？

かってな文字列集合 L について，
これを表現するオートマトン M がある（L = L(M)）

44無限の濃度がちがう
N：自然数全体の集合≡ ： 「一対一対応がある」
文字集合（アルファベット）は有限，とする

45

無限の濃度がちがう
N：自然数全体の集合≡ ： 「一対一対応がある」
文字集合（アルファベット）は有限，とする{ 文字列全体 } ≡ N
長さ n の文字列の個数は有限，∀ n45

無限の濃度がちがう
N：自然数全体の集合≡ ： 「一対一対応がある」
文字集合（アルファベット）は有限，とする{ 文字列全体 } ≡ N
長さ n の文字列の個数は有限，∀ n{ 文字列集合 L 全体 } ≡ P(N)45

無限の濃度がちがう
N：自然数全体の集合≡ ： 「一対一対応がある」
文字集合（アルファベット）は有限，とする{ 文字列全体 } ≡ N
長さ n の文字列の個数は有限，∀ n{ 文字列集合 L 全体 } ≡ P(N){ 有限オートマトン全体 } ≡ N
状態数 n の有限オートマトンは（同型をのぞいて）有限個しかない，∀ n45

無限の濃度がちがう
N：自然数全体の集合≡ ： 「一対一対応がある」
文字集合（アルファベット）は有限，とする{ 文字列全体 } ≡ N
長さ n の文字列の個数は有限，∀ n{ 文字列集合 L 全体 } ≡ P(N)ずれ
N ≡ P(N) は成り立たない！

{ 有限オートマトン全体 } ≡ N

状態数 n の有限オートマトンは（同型をのぞいて）有限個しかない，∀ n45

46

対角線論法（再掲）定理 任意の集合 X に対して，X と P(X) の間に1対1対応はない
証明（背理法）仮に，1対1対応 f: X ➔ P(X) があるとしよう．（矛盾を導く）（アイデア： ヤバそうな P(X) の元を持ってくる）
U = {x | x は f(x) に含まれない } と定義する．U は P(X) の元．
f: X ➔ P(X) は1対1対応なので，X の元 u であって，f(u) = Uとなるものが存在する．ここで，u が U に含まれるかを考える．
u が U に含まれる場合： f(u) = U より，u は f(u) に含まれる．
U の定義より，u は U に含まれない ➜ 矛盾！
u が U に含まれない場合： f(u) = U より，u は f(u) に含まれない．
U の定義より，u は U に含まれる ➜ 矛盾！

オートマトンの表現能力の限界0

M
1

クイズ 具体例は？

1

0
0

48

…

オートマトンの表現能力の限界0

M
1

クイズ 具体例は？

10

L = { 0n1n : n は 自然数 }= {ε, 01, 0011, 000111, …}は有限オートマトンで表現不可

48

0

…

オートマトンの表現能力の限界0

M
1

クイズ 具体例は？

10

L = { 0n1n : n は 自然数 }= {ε, 01, 0011, 000111, …}は有限オートマトンで表現不可

0

証明 （アイデア）
オートマトンは左から右に文字を読む
読んだ文字は次々に忘れていく
それでもなんとか記憶を残そうとする
唯一の記憶装置は「今どの状態にいるか？」➜ 決められた個数（有限個）しかない！
➜ たくさん 0 を読んでいるうちに「あふれる」
48…

オートマトンの表現能力の限界0M
1定理
L = { 0n1n :10n は 自然数 }0= {ε, 01, 0011, 000111, …}…

は有限オートマトンで表現不可
証明 （背理法）
L = L(M) となる有限オートマトン M が存在すると仮定
M の状態数を n とする
文字列 0n1n を考える．これは M に受理されるはず．
オートマトンの実行トレース

0

0

…

0

がとれる．
49

1

1

…

1

オートマトンの表現能力の限界0M
1定理
L = { 0n1n :10n は 自然数 }0= {ε, 01, 0011, 000111, …}…

は有限オートマトンで表現不可
証明 （背理法）
L = L(M) となる有限オートマトン M が存在すると仮定
M の状態数を n とする
文字列 0n1n を考える．これは M に受理されるはず．
オートマトンの実行トレース

0

0

…

0

1

1

…

1

状態 n+1個 ➜ 重複がある！

がとれる．
49

オートマトンの表現能力の限界

0

M
1

1

0
証明 （背理法）
0
L = L(M) となる有限オートマトン M が存在すると仮定…

M の状態数を n とする
文字列 0n1n を考える．これは M に受理されるはず．
オートマトンの受理トレース

0

0

…

0

1

1

…

1

状態 n+1個 ➜ 重複がある！

がとれる．

重複をショートカットしたら，0n-k1n の受理トレースができる (k はショートカットの長さ）．
➜ L = L(M) に矛盾！ 証明終．
50

理論計算機科学入門 ― 有限と無限のあいだ
アウトライン
理論計算機科学とは― 有限と無限のせめぎあい

いろいろな無限― 対角線論法

オートマトン理論入門
包含問題を解くアルゴリズム ― 有限の方法で無限の対象を操作
オートマトンの表現能力― 有限性の限界

形式検証― オートマトンを用いたシステム品質保証

AI 時代の形式検証― 研究紹介51

自己紹介• 理学士（東大 数学）
理学修士（東工大 数理・計算科学）
PhD （Computer Science, Radboud University Nijmegen, NL)• 専門分野✓◆theory of coalgebras
Defn. T (e) =, where B is a monadin K`(B )- 理論計算機科学における圏論的構造 (category theory)
Thm. Coalgebraic proof methods (such as (bi)simulations) are val- 特に，オートマトンの圏論的余代数によるモデリングと一般論
Proof. By the following characterizations in K`(B ).
Ff /F beh /
F OZ
FX
FX
FY
- 数学的抽象性が生み出す新奇な応用
O
O
O
c
c
w
final
d
/
/
X
X
Z
Y
beh
f
➜ 自動運転システムの品質保証手法
system behavior
simulation
e

e

e

c

c

- 特に，定理証明とモデル検査．
「システムが安全なことを証明」
52

圏論の歩き方（日本評論社）ビジネスでの証明

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明

この駐車場，
どうっすか！？

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明

この駐車場，
どうっすか！？

ゴンドラが衝突したりしない？ 大丈夫？

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明

絶対大丈夫っす！

この駐車場，
どうっすか！？

ゴンドラが衝突したりしない？ 大丈夫？

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明

絶対大丈夫っす！

この駐車場，
どうっすか！？

ホントに？ なんで？

ゴンドラが衝突したりしない？ 大丈夫？

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明
オレが責任持つっす！

絶対大丈夫っす！

この駐車場，
どうっすか！？

ホントに？ なんで？

ゴンドラが衝突したりしない？ 大丈夫？

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明
オレが責任持つっす！

絶対大丈夫っす！

この駐車場，
どうっすか！？

．．．
（ダメだこいつ）

ホントに？ なんで？

ゴンドラが衝突したりしない？ 大丈夫？

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明

この駐車場，
どうでしょう．

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明

この駐車場，
どうでしょう．

ゴンドラが衝突したりしない？ 大丈夫？

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明
はい，大丈夫です．
なぜなら，任意の状態 s に対して，ゴンドラ g1 の位置
を x1 とすると，．．．

この駐車場，
どうでしょう．

ゴンドラが衝突したりしない？ 大丈夫？

https://www.pexels.com/ja-jp/photo/63294/

ビジネスでの証明
はい，大丈夫です．
なぜなら，任意の状態 s に．．．（読んでる）
なるほど．それでは1
基いただこう．

対して，ゴンドラ g1 の位置
を x1 とすると，．．．

この駐車場，
どうでしょう．

ゴンドラが衝突したりしない？ 大丈夫？

https://www.pexels.com/ja-jp/photo/63294/

定理証明によるシステム品質保証
例: Hoare 論理による定理証明，プログラムの品質保証
イメージ： 紙とペンで証明を書くのと同じ
しかし，人力だと間違えるので，計算機上で．
記号列で証明を表現 ➜ 各ステップの正当性をプログラム（証明支援系）がチェックできれば証明の自動探索（定理証明器）（原理上は）無限の入力空間をすべてカバーできる
証明では「i を入力の自然数とする」とかけますね
数学的証明という，強い品質保証

program

Theorem forall_exists : (forall P : Set->Prop,(forall x, ~(P x)) -> ~(exists x, P x)).
Proof.
intros P.
intros forall_x_not_Px.
unfold not.
intros exists_x_Px.
destruct exists_x_Px as [ witness proof_of_Pwitness].
pose (not_Pwitness := forall_x_not_Px witness).
unfold not in not_Pwitness.
pose (proof_of_False := not_Pwitness proof_of_Pwitness).
case proof_of_False.
Qed.

Proof
searchhoge

specificationk = N!
after
execution

proof
55

A Coq proof of ∀x. ¬P(x) → ¬ ∃x. P(x)

証明で金もうけ
定理証明のコスト：
たとえば，ヨーロッパの計算機科学の博士課程（有給，3­4年）

https://
www.needpix.com/photo/178834/nerd-cartoongeek-character-glassesisolated-funny-face-smart

1000万円をゆうに超えるモデル検査によるシステム品質保証
基本的ワークフロー
システムモデルを，オートマトン M として表現
求める安全性をオートマトン Mʼ として表現．
「Mʼ に受理される文字列はすべて安全」

L(M) ⊆ L(M′) を示す（今日のアルゴリズムで）すると，M の振る舞い（＝受理される文字列）がすべて安全であると結論できる

オートマトンによる自動証明
システムモデル（駐車場の設計図など）

M

100,000状態
求める安全性を表現

Mʼ（「仕様」）

L(M) ⊆ L(M′)

50状態

Yes/No58

ソフトウェア品質保証におけるスペクトル
形式手法

テスト test

自動定理証明

モデル検査
低

コスト

ブラックボックス

対話定理証明高

ホワイトボックスモデルを要求

モデルを許容高自動化の度合い低自動

経験論的保証専門家を月・年単位で拘束低保証の網羅性

高低保証の数学的厳密性

高数学的保証 ➜ 「形式検証」
59

理論計算機科学入門 ― 有限と無限のあいだ
アウトライン
理論計算機科学とは― 有限と無限のせめぎあい

いろいろな無限― 対角線論法

オートマトン理論入門
包含問題を解くアルゴリズム ― 有限の方法で無限の対象を操作
オートマトンの表現能力― 有限性の限界

形式検証― オートマトンを用いたシステム品質保証

AI 時代の形式検証― 研究紹介60

形式手法の歴史（超ダイジェスト）
ソフトウェアの大規模化
ネットワー
ク，分散並列1970頃 形式手法によるソフトウェア品質保証（ソフトウェア検証）の研究開始．定理証明，モデル検査
1990頃 ソフトウェア検証のツール化・実応用加速定理証明： Isabelle, Coq, PVS, …
モデル検査： SPIN, SMV/NuSMV, mCRL2, PRISM, Uppaal, …

物理システムとの融合

統計的機械学2006 物理情報システム (Cyber-Physical Systems, CPS)への応用開始．ソフトウェア検証 ＋ 制御理論
（この経緯は [奥村，研究 技術 計画 2017] に詳しい）習の能力向上2016 機械学習システムへの応用．
形式的推論と統計的推論

61

ソフトウェア品質保証におけるスペクトル
形式手法

テスト test

自動定理証明

モデル検査
低

コスト

ブラックボックス

対話定理証明高

ホワイトボックスモデルを要求

モデルを許容高自動化の度合い低自動

経験論的保証専門家を月・年単位で拘束低保証の網羅性

高低保証の数学的厳密性

高数学的保証 ➜ 「形式検証」
62

ソフトウェア品質保証におけるスペクトル
形式手法

テスト test

自動定理証明

モデル検査
低

コスト

対話定理証明高システムの正しさを数学的に証明
ホワイトボックスモデルを要求➜ システムの「定義」が必要．

ブラックボックス
モデルを許容高自動化の度合い低「定義」＝ システムモデル． 専門家を月・年
自動低低

経験論的保証

単位で拘束
設計図，保証の網羅性
高システムの完全な記述
保証の数学的厳密性

高数学的保証 ➜ 「形式検証」
62

Uncertainties in
Cyber-Physical Systems 2020
Take automated driving…
perception

object recognition

local planningbehavior planning

path tracking

path planningsensingl
ica
ys
ph lityrea

actuation

63

Uncertainties in
Cyber-Physical Systems 2020
Take automated driving…
perception

object recognition

local planningbehavior planning

path tracking

path planningsensingl
ica
ys
ph lityrea

actuation

External uncertainties:
other traffic participants, weather,sunlight, comets, earthquakes, …

63

Uncertainties in
Cyber-Physical Systems 2020

Internal uncertainties:

Take automated driving…

never trust neural nets!

perception

object recognition

local planningbehavior planning

path tracking

path planningsensingl
ica
ys
ph lityrea

actuation

External uncertainties:
other traffic participants, weather,sunlight, comets, earthquakes, …

63

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit>

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit<latexit

統計的機械学習 vs 演繹的形式推論
A

統計的機械学習
演繹的形式推論

データのノイズを 入力の
誤り
許容
公理は絶対
誤りは想定せず

保証されない結論の正しさ

論理的に保証

高い
スケーラ

低い

データから自動で特徴量発見

ビリティ
公理の準備は人力（cf. エキスパートシステム）

説明可
能性

高い

低い

判断の理由はパラメータ（重み）64（cf. 数学的証明）

推論過程が証明として明示的AB
B

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit>

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit<latexit

統計的機械学習 vs 演繹的形式推論
ニューラルネットなど．

重要な応用対象

統計的機械学習
演繹的形式推論

データのノイズを 入力の
誤り
許容
公理は絶対
誤りは想定せず

保証されない結論の正しさ

論理的に保証

高い
スケーラ

低い

データから自動で特徴量発見

ビリティ
公理の準備は人力（cf. エキスパートシステム）

説明可
能性

高い

低い

判断の理由はパラメータ（重み）

今日の話

64

A

（cf. 数学的証明）

推論過程が証明として明示的

A
B
B

You walk in the dark,

65

Hasuo (NII, Tokyo)

www.istockphoto.com

You walk in the dark,
guided by an apparatus

65

Hasuo (NII, Tokyo)

www.istockphoto.com

… which itself is a black box!

https://pixabay.com/illustrations/cube-block-black-box-3d-geometric-250082/

66

Hasuo (NII, Tokyo)

ERATO MMSD 紹介
JST ERATO プロジェクト
2016/10-2022/03.
総勢50名規模の基礎研究プロジェクト

プロジェクト目標： 工業製品の設計サポート
形式手法の拡張．ソフトウェアから物理情報システムへ
安全性・信頼性，Veriﬁcation & Validation．
「システムが期待通り動作するか」
特に自動運転を戦略的ターゲットに．U Waterloo と協働
www.autonomoose.net
67

ERATO MMSD 紹介
JST ERATO プロジェクト
2016/10-2022/03.
総勢50名規模の基礎研究プロジェクト

プロジェクト目標： 工業製品の設計サポート
形式手法の拡張．ソフトウェアから物理情報システムへ
安全性・信頼性，Veriﬁcation & Validation．
「システムが期待通り動作するか」
特に自動運転を戦略的ターゲットに．U Waterloo と協働
www.autonomoose.net
67

ERATO MMSD 紹介
アプローチ
テストと形式検証（証明）のミックス
環境の不確かさ，統計的機械学習，…
➜ すべてを証明することは不可能 ✓Defn.

T (e) =

theory of coalgebrasin K`(Be )◆, where Be is a monad suited for e

それでもできるだけ証明・説明をThm. Coalgebraic proof methods (such as (bi)simulations) are valid in T (e) too.
（cf. 自動運転車の安全性）
Proof. By the following characterizations in K`(B ).
e

証明を用いたテスト効率化

FX
O
c
X

現代数学（特に圏論）を軸にした異分野協働，科学的ブレークスルー

F behc /

F OZ
final
/Z

behc
system behavior

FX
O
c
X

Ff
w

/ FY
O
d
/Y

f
simulation

たとえばオートマトンは余代数として抽象化できます（… また次の機会に）68

圏論の歩き方
（圏論の歩き方委員会 編）
日本評論社，2015

理論計算機科学入門 ― 有限と無限のあいだ
アウトライン
理論計算機科学とは― 有限と無限のせめぎあい

いろいろな無限― 対角線論法

オートマトン理論入門
包含問題を解くアルゴリズム ― 有限の方法で無限の対象を操作
オートマトンの表現能力― 有限性の限界

形式検証― オートマトンを用いたシステム品質保証

AI 時代の形式検証― 研究紹介69

参考文献
思いつくところを少し挙げます．完全なリストには程遠いです．
いろいろな無限 ― 対角線論法
数学科の2年で習う「集合・位相」の冒頭部分です
集合への30講，志賀 浩二，朝倉書店 （読みやすい）
集合・位相入門，松坂 和夫，岩波書店 （ハードコア）
オートマトン理論入門
情報科学科の2年で習う「形式言語理論」の最初の半分を，形式検証向けにアレンジしました
J. Hopcroft, R. Motowani, J. Ullman 著，野崎 昭弘， 高橋 正子，町田 元，山崎 秀記 訳
『オートマトン，言語理論，計算論Ｉ, 第2版』 サイエンス社
形式検証
ツールがたくさんあるので，ダウンロードして遊んでみると楽しいのでは
SPIN モデル検査：検証モデリング技法，中島 震，近代科学社 （モデル検査）
コンピュータは数学者になれるのか？ 数学基礎論から証明とプログラムの理論へ，照井 一成，青土社（定理証明と論理学入門，おすすめ）理論計算機科学入門 ― 有限と無限のあいだ
まとめ
理論計算機科学とは― 有限と無限のせめぎあい

いろいろな無限― 対角線論法

オートマトン理論入門
包含問題を解くアルゴリズム ― 有限の方法で無限の対象を操作
オートマトンの表現能力― 有限性の限界

形式検証― オートマトンを用いたシステム品質保証

AI 時代の形式検証― 研究紹介71

ご清聴ありがとうございました
http://group-mmm.org/~ichiro/

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, vonDefinition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ B
A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B···Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R)
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

original (discrete)···.

Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.
Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

automata
automata
program logic
safety by invariants(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.

e.2.7 Metamathematical Transfer Our approach is then explained as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e72• we parametrize both a theory T (discrete,from software science) and a new

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, vonDefinition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ B
A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B···Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R)
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

original (discrete)···.

Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.
Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

automata
automata
program logic
safety by invariants(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.
Image by Robin
Higgins from Pixabay

e.2.7 Metamathematical Transfer Our approach is then explained
数学者as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e72• we parametrize both a theory T (discrete,from software science) and a new

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, vonDefinition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ B
A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B···Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R)
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

···.
Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.

Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

メタ数学者
original (discrete)

automata
automata
program logic
Image by Robinsafety by invariants

Higgins from Pixabay(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.
Image by Robin
Higgins from Pixabay

e.2.7 Metamathematical Transfer Our approach is then explained
数学者as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e72• we parametrize both a theory T (discrete,from software science) and a new

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, von
どんなにがんばっても
Definition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ Bそれは証明できないよ…

A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B···Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R)
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

···.
Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.

Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

メタ数学者
original (discrete)

automata
automata
program logic
Image by Robinsafety by invariants

Higgins from Pixabay(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.
Image by Robin
Higgins from Pixabay

e.2.7 Metamathematical Transfer Our approach is then explained
数学者as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e72• we parametrize both a theory T (discrete,from software science) and a new

in rigorous mathematical terms. Typically mathematical logic is the language
Hilbert, Gödel, Church,
See Fig. 9, where the distinction between object-level proofs (trees subject to d
さっそく脱線：
Gentzen, Cohen, Turing, …
proofs (in English) is especially notable. Metamathematics have brought about n➜ computers!
数学基礎論，メタ数学
retically and practically—one of them is computers themselves, by Turing, von
どんなにがんばっても
Definition. A proof is a finite tree subject to the derivation
rules:∨Γ ⇒ ∆, A ∨ Bそれは証明できないよ…

A, Γ ⇒ ∆, B
Γ ⇒ ∆, A B, Π ⇒ Σ
(⊃-L)
(⊃-R)
⇒
A ⊃ B, Γ, Π ⇒ ∆, ΣΓ ⇒ ∆, A ⊃ B…ということを······Γ ⇒ ∆, A A, Π ⇒ ΣA, Γ ⇒ ∆Γ ⇒ ∆, A
(Cut)
(¬-L)
(¬-R) 私は証明できます！
.
Γ, Π ⇒ ∆, Σ¬A, Γ ⇒ ∆
Γ ⇒. ∆, ¬A.
A theorem is a formula A with a proof ⇒ A.

.
Theorem (cut elimination). ..
Any theorem A has a proof ⇒ A where the (C UT) rule is never used.

Proof. Let Π be a proof of a theorem A. We turn Π into a cut-free
proof Π′ by induction. . .

Fig. 9: Metamathematics. Distinguish object-level notions (thatare symbolic, i.e. syntactic constructs) from meta-level notions.

メタ数学者
original (discrete)

automata
automata
program logic
Image by Robinsafety by invariants

Higgins from Pixabay(bi)simulation

Fig. 10: Existing Appra one-by-one manner,oretical work.
Image by Robin
Higgins from Pixabay

e.2.7 Metamathematical Transfer Our approach is then explained
数学者as follow
数学者の営為の数学的研究
In most of the existing attempts to heterogeneity and quantity, it is an individua
that定義，定理，証明などの概念が数学的に定義される
is extended, accounting for a single new concern at a time. See Fig. 10 for e72• we parametrize both a theory T (discrete,from software science) and a new

理論計算機科学とは？
応用数学の一分野です
純粋数学「応用する気のない数学」「応用できない数学」「役に立たない数学」とは違う本人にその気がなくても，時々応用で大ホームランを飛ばす
あなどれない！！

73