pptx - 横山てつお

情報科学概論第1回
1
授業概要
ソフトウェアの基礎的な概念や技術を学ぶ
1.
2.
3.
4.
プログラミング言語理論と数理論理学
プログラミング言語を設計・実装
様々な性質の証明
型システム・型安全性
2
評価
レポート100%
3
テキストと参考書
• テキスト(以下の有志の和訳)
http://proofcafe.org/sf/
• 参考書
Pierce, B.C. et. al., Software Foundations,
http://www.cis.upenn.edu/~bcpierce/sf/index.html
• 日本語のスライドとテキストを用いて欲
しいという要望に2016年度から応えます
4
証明支援系 Coq
• The Coq Proof Assistant
http://coq.inria.fr/
• ダウンロード先
http://coq.inria.fr/download
• 各自で環境を用意すること
（予習・復習のときにも使うこと）
5
開発環境
• CoqIDE を推奨
– 去年度まで全学生が CoqIDE を使用
• Emacs+ProofGeneral
– (私はこちらを使っています)
– ショートカットキーが便利
– 他のツールとの連携
6
われわれの直面する課題
• 社会基盤を支えるソフトウェア
• ソフトウェアの不具合の社会への影響
• 高信頼ソフトウェア
7
計算機科学やソフトウェア工学の
成果
• プロジェクト管理
• 開発チームの組織化—XP
• ライブラリの設計手法—MVC,
Publish/Subscribe
• プログラミング言語—OOP, AOP, FP
• 数学的手法ーSWの性質の規定・論証
• ツールーSWの性質の妥当性確認の支援
8
本講義で扱う 5 つの内容
1. 論理学
–
プログラムに関するクレームの作成・確認
2. 証明支援
–
厳密な論理的議論を構築
3. 関数型プログラミング
–
プログラミング方法およびプログラミングと論理学
の橋渡し
4. 形式的手法
–
プログラムの性質の論証
5. 型システム
–
プログラムの振舞いが適切である保証
9
1. 論理学
• cf. 学部の『情報数学』，『数理論理学』，
院の『数理論理学研究』
• 命題論理・述語論理・様相論理・・・
• 証明が研究対象
• 本講義では，計算機科学における
論理学の役割を学ぶ
• 例：帰納法による証明 →
プログラムのクレーム
10
2. 論理的命題の証明を構築するツール
• 計算機科学から論理学への貢献のひとつ
• 大きく2つに分けられる
1. 自動定理証明系：
SATソルバ，SMTソルバ，モデル検査器
2. 証明支援系：
Isabelle, Agda, Coq
11
2. CSや数学におけるCoqの活躍
• プログラミング言語のモデリング：
– JavaCard, x86, LLVM
• 正しさが形式的に証明された開発環境：
– CompCert, Certicrypt
• 依存型を用いたプログラミングの環境：
– Ynot
• 高階論理の証明支援：
– 4色問題, Feit-Thompson Theorem
12
3. 関数型プログラミング
• cf. 学部の『プログラミング言語』
• プログラミング方式 or プログラミング言語
•
•
•
•
•
長い歴史
純粋性
理解しやすく論証しやすい
並列性
論理学と計算機科学の橋渡し
13
4. プログラム検証
• cf. 学部の『プログラミング言語』
• cf. 大学院の『正当性検証と妥当性確認』
『ソフトウェア工学演習』
• 高信頼性ソフトウェア(とハードウェア)の構築
– プログラムの性質の証明
– プログラミング言語の性質の証明
• 復習：抽象構文, セマンティクス, ホアの3つ組
14
5. 型システム
• プログラムの性質を記述できる
• お手軽な形式手法
– 背景にある知識が無くても使える
– 型付きプログラムは「悪さ」をしない
• Coqのコア：単純型付きラムダ計算
15
Basics
Coq における
関数型プログラミング
16
関数型プログラミング
• 関数型プログラミングは数学に近い
• 関数型プログラミングにおける関数
– 入力→出力
– 第一級の値
• 他の関数の引数，返り値，データ構造への格納
• 代数データ型，パターンマッチ，
多相型システム，．．．
17
型
day
sunday
friday
tuesday
monday
saturday
wednesday
thursday
18
型 monday
:
tuesday
:
wednesday :
thursday :
friday
:
saturday :
sunday
:
day
day
day
day
day
day
day
19
列挙型の定義：曜日
Inductive day
| monday
| tuesday
| wednesday
| thursday
| friday
| saturday
| sunday
:
:
:
:
:
:
:
:
Type :=
day
列挙により
day
新しい型を
day
定義
day
day
day
day.
20
関数定義：次の平日
Definition next_weekday (d:day) : day :=
match d with
| monday
=> tuesday
| tuesday
=> wednesday
| wednesday => thursday
| thursday => friday
| friday
=> monday
| saturday => monday
| sunday
=> monday
end.
21
動作の確認方法１：評価
simplification (単純化)
Eval simpl
in (next_weekday friday).
(* ==> monday : day *)
Eval simpl
in (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)
22
動作の確認方法２：言明
Example test_next_weekday:
(next_weekday (next_weekday saturday))
= tuesday.
期待する結果を書いておく
23
動作の確認方法３：抽出
• OCaml, Scheme, Haskellなどの
プログラミング言語に抽出する
• 正しさが証明されたプログラムを
構築することができる
24
関数定義：前の平日
Definition prev_weekday (d:day) : day :=
match d with
| monday
=> friday
| tuesday
=> monday
| wednesday => tuesday
| thursday => wednesay
| friday
=> thursday
| saturday => friday
| sunday
=> friday
end.
25
動作の確認方法１：評価
Eval simpl
in (prev_weekday monday).
(* ==> friday : day *)
Eval simpl
in (prev_weekday (prev_weekday saturday)).
(* ==> thursday : day *)
26
真偽値型
型定義
Inductive bool : Type :=
| true : bool
| false : bool.
真偽値型上の関数１
Definition orb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => true
| false => b2
end.
27
orbの正しさの証明
反射性
Example test_orb1: (orb true false) = true.
Proof. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. reflexivity. Qed.
真理値表で与えられる仕様を
完全にチェックしたのに同じ
28
negb
NEGは，引数がtrueならばfalse，falseならばtrueを返す
Definition negb (b:bool) : bool :=
match b with
| false => true
| true => false
end.
29
nandb
NANDは，引数の両方もしくはどちらかがfalseならばtrueを返す
Definition nandb (b1:bool) (b2:bool) : bool :=
match b1 with
| false => true
| true => match b2 with
| false => true
| true => false
end
end.
30
別解: nandb
NANDは，引数の両方もしくはどちらかがfalseならばtrueを返す
Definition nandb (b1:bool) (b2:bool) : bool :=
negb (andb b1 b2).
以下の言明はCoqによって正しいことが確かめられる
Example test_nandb1: (nandb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb2: (nandb false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb3: (nandb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb4: (nandb true true) = false.
Proof. simpl. reflexivity. Qed.
31
andb3
引数のどれかがfalseならばfalseを返す
Definition andb3 (b1:bool) (b2:bool)
(b3:bool) : bool :=
match b1 with
| false => false
| true => match b2 with
| false => false
| true => match b3 with
| false => false
| true => true
end
end
end.
32
別解: andb3
引数のどれかがfalseならばfalseを返す
Definition andb3 (b1:bool) (b2:bool)
(b3:bool) : bool :=
andb b1 (andb b2 b3).
33
Check: 関数の型を調べるコマンド
Check true.
(* ===> true : bool *)
Check (negb true).
(* ===> negb true : bool *)
Check negb.
(* ===> negb : bool -> bool *)
関数型
34
自然数の帰納的定義
Inductive nat : Type :=
| O : nat
| S : nat
→
nat.
• O は nat
• S は nat を取って nat を返すコンストラクタ
自然数の集合 nat は以下のように作られる
• O は nat に属する
• n が nat に属するなら S n も nat に属する
• この2規則にしたがうもののみが nat に属する
35
自然数の例
•例
–O
–S O
–S (S O)
–S (S (S O))
• 反例
–true
–andb true false
–S (S false)
型エラー
36
前者関数
Definition pred (n : nat) : nat :=
match n with
O の前者は O とする
| O
=> O
| S n' => n'
end.
もし n がある式 n' に対して S n' と
いう形をしていたら n' を返す
37
入れ子パターン
Definition minustwo (n : nat) : nat :=
match n with
| O
=> O
| S O
=> O
| S (S n') => n'
end.
38
アラビア数字表記
built-in
の nat
Check (S (S (S (S O)))).
(* ===> 4 : nat *)
Eval simpl in (minustwo 4).
(* ===> 2 : nat *)
39
コンストラクタと関数
関数型をもつコンストラクタ
Check S.
(* ===> S : nat → nat *)
Check pred.
(* ===> pred : nat → nat *)
Check minustwo.
(* ===> minustwo : nat → nat *)
関数は計算を伴う
40
再帰関数
キーワード
Fixpoint evenb (n:nat) : bool :=
match n with
| O
=> true
| S O
=> false
| S (S n') => evenb n'
end.
再帰
Coqの関数は、最初の引数が減少している必要がある
→ 最終的に停止する
41
クイズ
正しいものを選びなさい
1. 任意のプログラムは必ず停止する
2. 任意のプログラムが
停止するか停止しないか判定できる
3. 任意のプログラムが
停止するか停止しないかは判定できない
42
複数引数関数
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O
=> m
| S n' => S (plus n' m)
end.
43
複数引数関数
Fixpoint plus (n m : nat) : nat :=
match n with
| O
=> m
| S n' => S (plus n' m)
end.
まとめることができる
44
Fixpoint plus (n m : nat) : nat :=
match n with
| O
=> m
| S n' => S (plus n' m)
end.
Eval simpl in (plus (S (S (S O))) (S (S O))).
plus (S (S (S O))) (S (S O))
簡約
==> S (plus (S (S O)) (S (S O)))
by the second clause of the match
==> S (S (plus (S O) (S (S O))))
by the second clause of the match
==> S (S (S (plus O (S (S O)))))
by the second clause of the match
==> S (S (S (S (S O))))
by the first clause of the match
45
複数引数関数
Fixpoint mult (n m : nat) : nat :=
match n with
| O => O
| S n' => plus m (mult n' m)
end.
Example test_mult1: (mult 3 3) = 9.
Proof. reflexivity. Qed.
46
複数式の同時マッチ
Fixpoint minus (n
match n, m with
| O ,
_
=>
| S _ , O
=>
| S n', S m' =>
end.
m:nat) : nat :=
O
n
minus n' m'
ワイルドカードパターン
. 常にマッチが成功する
. 束縛はしない
47
別解: nandb
NANDは，引数の両方もしくはどちらかがfalseならばtrueを返す
Definition nandb (b1 b2:bool) : bool :=
match b1, b2 with
| true, true => false
| _
, _
=> true
end.
48
exp
指数
Fixpoint exp (base power : nat) : nat :=
match power with
| O
=> S O
| S p => mult base (exp base p)
end.
49
factorial
階乗
Fixpoint factorial (n:nat) : nat :=
match n with
| O
=> S O
| S n => mult (S n) (factorial n)
end.
Example test_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.
Example test_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity. Qed.
50
記法の導入
Notation "x + y" :=
(plus x y)
(at level 50, left associativity)
: nat_scope.
Check ((0 + 1) + 1).
51
記法の導入
Notation "x - y" :=
(minus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x * y" :=
(mult x y)
(at level 40, left associativity)
: nat_scope.
52
自然数の等しさを真偽値で返す関数
natural
numbers
eqality
boolean
Fixpoint beq_nat (n m
match n with
| O
=> match m
| O
| S m'
end
| S n' => match m
| O
| S m'
end
end.
: nat) : bool :=
with
=> true
=> false
with
=> false
=> beq_nat n' m'
53
• ble_nat, beq_nat  blt_nat
54
blt_nat
Definition blt_nat (n m : nat) : bool :=
match beq_nat n m with
| true => false
| false => ble_nat n m
end.
Example test_blt_nat1: (blt_nat 2 2) = false.
Example test_blt_nat2: (blt_nat 2 4) = true.
Example test_blt_nat3: (blt_nat 4 2) = false.
55
単純化による証明
• 性質の言明と証明
• これまでのExampleによる
言明とその証明
– 関数定義によって両辺を
単純化して一致させる
• この「単純化による証明」を用いて
より興味深い性質を証明していく
56
復習: 単位元
0+1=1
0+2=2
0+3=3
:
⇒
抽象化
∀x∈nat.
0+x=x
0を足しても元のまま
57
復習: 単位元
∀x∈nat.
0+x=x
nat = {0,1,2,...}
+ : (nat × nat)  nat
0が単位元
∀x∈nat.
1×x=x
nat = {0,1,2,...}
× : (nat × nat)  nat
1が単位元
∀x∈bool.
true∧x= x
bool = {true, false}
∧ : (bool × bool)  bool
trueが単位元
58
復習: 単位元
∀x∈nat.
0+x=x
∀x∈nat.
1×x=x
∀x∈bool.
true∧x= x
⇒
抽象化
∀x∈X.
ex=x
 : (X × X)  X
e∈X
59
復習: 単位元
e:Xは
:(X×X)Xの
左単位元
e:Xは
:(X×X)Xの
右単位元
∀x∈X.
ex=x
∀x∈X.
xe=x
 : (X × X)  X
e∈X
 : (X × X)  X
e∈X
60
定理： 0 は + の左単位元
Theorem plus_O_n : ∀n : nat, 0 + n = n.
Proof. reflexivity. Qed.
以下はCoqに
とっては同じ
Example
Lemma
Fact
Remark
+ は第一引数上を再帰する
Fixpoint plus (n m : nat) : nat :=
match n with
| O
=> m
| S n' => S (plus n' m)
end.
61
定理： 0 は + の右単位元
Theorem plus_O_n :
∀n
: nat, n + 0 = n.
単純化による証明は不可
（後でまた考える）
Fixpoint plus (n m : nat) : nat :=
match n with
| O
=> m
| S n' => S (plus n' m)
end.
62
タクティック
• simpl, reflexivity, ...
• Proof と Qed の間に書いて
命題をどのように確認するかを指示する
63
intros タクティック
Theorem plus_O_n'' : ∀n:nat, 0 + n = n.
Proof. intros n. reflexivity. Qed.
< Proof.
======================
∀n : nat, 0 + n = n
< intros n.
量化子を
文脈(仮定の列)へ
n : nat
======================
0 + n = n
< reflexivity. Qed.
64
以下も同様
Theorem plus_1_l : ∀n:nat, 1 + n = S n.
Proof.
intros n. reflexivity. Qed.
Theorem mult_0_l : ∀n:nat, 0 * n = 0.
Proof.
intros n. reflexivity. Qed.
65
書換えによる証明
Theorem plus_id_example :
∀n
m:nat,
n = m →
n + n = m + m.
< Proof. intros n m H.
n : nat
m : nat
H : n = m
================
n + n = m + m
書換え
< rewrite -> H.
n : nat
m : nat
H : n = m
================
m + m = m + m
66
練習問題
Theorem plus_id_exercise :
∀n
m o : nat,
n = m → m = o → n + m = m + o.
Proof.
intros n m o H H'.
rewrite -> H.
rewrite <- H'.
reflexivity. Qed.
67
定理の使い方
Theorem mult_0_plus : ∀n m : nat,
(0 + n) * m = n * m.
Proof.
すでに証明した
intros n m.
plus_O_nを用いて
書き換え
rewrite → plus_O_n.
reflexivity. Qed.
68
練習問題
Theorem mult_1_plus : ∀n m : nat,
(1 + n) * m = m + (n * m).
Proof.
すでに証明した
intros n m.
plus_1_lを用いて
rewrite → plus_1_l.
書き換え
reflexivity.
Qed.
1+n=Sn
の左辺は S n に
単純化される
(plusの定義)
69
単純化による証明の限界
Theorem plus_1_neq_0_firsttry :
beq_nat (n + 1) 0 = false.
Proof.
intros n.
simpl. (* 単純化できない *)
Admitted.
n : nat
∀n
: nat,
===========================
beq_nat (n + 1) 0 = false
再掲 Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
70
場合分けによる証明
Theorem plus_1_neq_0 : ∀n : nat,
beq_nat (n + 1) 0 = false.
intro
Proof.
パターン
intros n. destruct n as [| n'].
reflexivity.
beq_nat (0 + 1) 0
= false
reflexivity.
beq_nat (S n' + 1) 0 = false
Qed.
Inductive nat : Type :=
| O : nat
| S : nat
→
nat.
Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
71
negation is involutive
Theorem negb_involutive : ∀b : bool,
negb (negb b) = b.
Proof.
intros b. destruct b.
reflexivity.
reflexivity. Qed.
as以下を省略
(コンストラクタが
引数を持たないため)
72
練習問題
Theorem zero_nbeq_plus_1 : ∀n : nat,
beq_nat 0 (n + 1) = false.
Proof.
intros.
destruct n as [|n'].
reflexivity.
reflexivity.
Qed.
73
練習問題
Theorem identity_fn_applied_twice :
∀(f : bool → bool),
(∀(x : bool), f x = x) →
∀(b : bool), f (f b) = b.
Proof.
intros f. intros H. intros b.
destruct b.
(* Case "b = true". *)
rewrite H. rewrite H. reflexivity.
(* Case "b = false". *)
rewrite H. rewrite H. reflexivity.
74
Qed.
練習問題
Theorem negation_fn_applied_twice :
∀(f : bool → bool),
(∀(x : bool), f x = negb x) →
∀(b : bool), f (f b) = b.
Proof.
intro f. intro H. intro b.
destruct b.
(* Case "b = true". *)
rewrite H. rewrite H.
rewrite negb_involutive. reflexivity.
(* Case "b = false". *)
rewrite H. rewrite H.
rewrite negb_involutive. reflexivity.
Qed.
75
Theorem andb_eq_orb :
∀(b c : bool),
(andb b c = orb b c) →
b = c.
Proof.
いくつか
補題が必要
intros b c H.
destruct c.
destruct b.
reflexivity.
rewrite <- andb_f_t_f. rewrite H.
reflexivity.
destruct b.
rewrite <- andb_t_f_f. rewrite H.
reflexivity.
reflexivity.
Qed.
76
Lemma andb_f_t_f : andb false true = false.
Proof. reflexivity. Qed.
Lemma andb_t_f_f : andb true false = false.
Proof. reflexivity. Qed.
77
練習問題 binary
Inductive bin : Type :=
| BO : bin
| T : bin -> bin
| T1 : bin -> bin.
binary number *)
(*
(*
(*
(*
(a) *)
zero *)
twice a binary number *)
one more than twice a
Fixpoint inc_bin (n : bin) : bin := (* (b) *)
match n with
| BO
=> T1 BO
| T n' => T1 n'
| T1 n' => T (inc_bin n')
end.
Fixpoint bin2nat (b : bin) : nat :=
match b with
| BO
=> O
| T b' => double (bin2nat b')
| T1 b' => S (double (bin2nat b'))
end.
78
練習問題 binary(続き)
Example binary_unary_comm : forall b:bin,
bin2nat (inc_bin b) = S (bin2nat b).
Proof.
intros b.
induction b as [| b' | b' ].
Case "b = BO".
reflexivity.
Case "b = T b'". reflexivity.
Case "b = T1 b'".
simpl. rewrite IHb'. reflexivity.
Qed.
79
練習問題 binary
Example binary_unary_comm : forall b:bin, (* (c) *)
bin2nat (inc_bin b) = S (bin2nat b).
b
bin2nat b
S (bin2nat b)
=
increment b
bin2nat (inc_bin b)
80
まとめ
•
•
•
•
•
•
•
型定義
関数定義
単純化による証明
タクティック（simpl, reflexivity, intros）
書換えによる証明(rewrite)
場合分けによる証明(destruct)
帰納法による証明(intros)
81

Download Report