情報科学概論
第7回
1
関係としての評価
Inductive aevalR : aexp → nat → Prop :=
| E_ANum : ∀(n: nat),
aevalR (ANum n) n
| E_APlus : ∀(e1 e2: aexp) (n1 n2: nat),
aevalR e1 n1 →
aevalR e2 n2 →
aevalR (APlus e1 e2) (n1 + n2)
| E_AMinus: ∀(e1 e2: aexp) (n1 n2: nat),
aevalR e1 n1 →
aevalR e2 n2 →
aevalR (AMinus e1 e2) (n1 - n2)
| E_AMult : ∀(e1 e2: aexp) (n1 n2: nat),
aevalR e1 n1 →
aevalR e2 n2 →
aevalR (AMult e1 e2) (n1 * n2).
Notation "e '⇓' n" := (aevalR e n) : type_scope.
2
Theorem aeval_iff_aevalR' : ∀a n,
(a ⇓ n) ↔ aeval a = n.
Proof.
関数による定義
split. 関係による定義
Case "→".
intros H; induction H; subst; reflexivity.
Case "←".
generalize dependent n.
induction a; simpl; intros; subst; constructor;
try apply IHa1; try apply IHa2; reflexivity.
Qed.
3
推論規則の記法
| E_APlus : ∀ (e1 e2: aexp) (n1 n2: nat),
aevalR e1 n1 →
aevalR e2 n2 →
aevalR (APlus e1 e2) (n1 + n2)
e1 ⇓ n1
コンストラクタ
e2 ⇓ n2
------------------- (E_APlus)
APlus e1 e2 ⇓ n1+n2
4
5
変数をもつ式
6
識別子(Impでは数)
簡単のため
natを識別子に
Inductive id : Type :=
Id : nat → id.
ラップする
Definition beq_id X1 X2 :=
match (X1, X2) with
(Id n1, Id n2) => beq_nat n1 n2
end.
7
状態
Definition state := id → nat.
簡単のため
すべての変数に
定義(全域に)
Definition empty_state : state :=
fun _ => 0.
Definition update (st : state) (X:id) (n : nat) : state :=
fun X' => if beq_id X X' then n else st X'.
8
構文
Inductive aexp : Type :=
| ANum : nat → aexp
| AId : id → aexp (* <----- NEW *)
| APlus : aexp → aexp → aexp
| AMinus : aexp → aexp → aexp
| AMult : aexp → aexp → aexp.
9
変数名
Definition X : id := Id 0.
Definition Y : id := Id 1.
Definition Z : id := Id 2.
10
bexp の定義(前と同じ)
Inductive bexp : Type :=
| BTrue : bexp
| BFalse : bexp
| BEq : aexp → aexp → bexp
| BLe : aexp → aexp → bexp
| BNot : bexp → bexp
| BAnd : bexp → bexp → bexp.
11
aexpの評価
Fixpoint aeval (st : state) (e : aexp) : nat :=
match e with
| ANum n => n
| AId X => st X (* <----- NEW *)
| APlus a1 a2 => (aeval st a1) + (aeval st a2)
| AMinus a1 a2 => (aeval st a1) - (aeval st a2)
| AMult a1 a2 => (aeval st a1) * (aeval st a2)
end.
12
bexpの評価
Fixpoint beval (st : state) (e : bexp) : bool :=
match e with
| BTrue => true
| BFalse => false
| BEq a1 a2 => beq_nat (aeval st a1) (aeval st a2)
| BLe a1 a2 => ble_nat (aeval st a1) (aeval st a2)
| BNot b1 => negb (beval st b1)
| BAnd b1 b2 => andb (beval st b1) (beval st b2)
end.
13
コマンド
14
構文(BNF)
com ::= 'SKIP’
| X '::=' aexp
| com ';' com
| 'WHILE' bexp 'DO' com 'END'
| 'IFB' bexp 'THEN' com 'ELSE' com 'FI'
例．Impの階乗関数
Z ::= X;
Y ::= 1;
WHILE not (Z = 0) DO
Y ::= Y * Z;
Z ::= Z - 1
END
構文
Inductive com : Type :=
| CSkip : com
| CAss : id → aexp →
| CSeq : com → com →
| CIf : bexp → com →
| CWhile : bexp → com
com
com
com → com
→ com.
16
記法の導入
Notation "'SKIP'" :=
CSkip.
Notation "X '::=' a" :=
(CAss X a) (at level 60).
Notation "c1 ; c2" :=
(CSeq c1 c2) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
(CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
(CIf e1 e2 e3) (at level 80, right associativity).
Definition fact_in_coq : com :=
Z ::= AId X;
Y ::= ANum 1;
WHILE BNot (BEq (AId Z) (ANum 0)) DO
Y ::= AMult (AId Y) (AId Z);
Z ::= AMinus (AId Z) (ANum 1)
END.
17
例．Impの階乗関数
Definition fact_in_coq : com :=
Z ::= AId X;
Y ::= ANum 1;
WHILE BNot (BEq (AId Z) (ANum 0)) DO
Y ::= AMult (AId Y) (AId Z);
Z ::= AMinus (AId Z) (ANum 1)
END.
18
例：代入
Definition plus2 : com :=
X ::= (APlus (AId X) (ANum 2)).
Definition XtimesYinZ : com :=
Z ::= (AMult (AId X) (AId Y)).
Definition subtract_slowly_body : com :=
Z ::= AMinus (AId Z) (ANum 1) ;
X ::= AMinus (AId X) (ANum 1).
19
例：繰り返し
Definition subtract_slowly : com :=
WHILE BNot (BEq (AId X) (ANum 0)) DO
subtract_slowly_body
END.
Definition subtract_3_from_5_slowly : com :=
X ::= ANum 3 ;
Z ::= ANum 5 ;
subtract_slowly.
20
無限の繰り返し
Definition loop : com :=
WHILE BTrue DO
SKIP
END.
21
評価
22
評価関数(失敗)
Fixpoint ceval_fun_no_while
(st : state) (c : com) : state :=
match c with
| SKIP =>
st
| l ::= a1 =>
update st l (aeval st a1)
| c1 ; c2 =>
let st' := ceval_fun_no_while st c1 in
ceval_fun_no_while st' c2
| IFB b THEN c1 ELSE c2 FI =>
if (beval st b)
Coqが
then ceval_fun_no_while st c1
else ceval_fun_no_while st c2
停止性を
| WHILE b1 DO c1 END =>
言えるように
st (* bogus *)
書けない
end.
23
評価関数(失敗)
Fixpoint ceval_fun (st : state) (c : com) : state :=
match c with
...
| WHILE b1 DO c1 END =>
if (beval st b1)
then ceval_fun st (c1; WHILE b1 DO c1 END)
else st
end.
このようには
書けない
(停止すると
いえる？)
24
関係としての評価
c / st ⇓ st'
25
Example ceval_example1:
証明が必要
(X ::= ANum 2;
IFB BLe (AId X) (ANum 1)
THEN Y ::= ANum 3
ELSE Z ::= ANum 4
FI)
/ empty_state
⇓ (update (update empty_state X 2) Z 4).
Proof.
(* We must supply the intermediate state *)
apply E_Seq with (update empty_state X 2).
Case "assignment command".
apply E_Ass. reflexivity.
Case "if command".
apply E_IfFalse.
reflexivity.
apply E_Ass. reflexivity. Qed.
26
評価の決定性
Theorem ceval_deterministic: ∀c st st1 st2,
c / st ⇓ st1 →
c / st ⇓ st2 →
st1 = st2.
27
プログラムの論証
28
例
Definition plus2 : com :=
X ::= (APlus (AId X) (ANum 2)).
Theorem plus2_spec : ∀st n st',
st X = n →
plus2 / st ⇓ st' →
st' X = n + 2.
Proof.
intros st n st' HX Heval.
(* Inverting Heval essentially forces Coq to expand one
step of the ceval computation - in this case revealing
that st' must be st extended with the new value of X,
since plus2 is an assignment *)
inversion Heval. subst. clear Heval. simpl.
apply update_eq. Qed.
29
まとめ
30
再掲示
授業概要
ソフトウェアの基礎的な概念や技術を学ぶ
1.
2.
3.
4.
プログラミング言語理論と数理論理学
プログラミング言語を設計・実装
様々な性質の証明
型システム・型安全性
31
再掲示
評価
レポート100%
32
再掲示
本講義で扱う 5 つの内容
1. 論理学
プログラムに関するクレームの作成・確認
2. 証明支援
厳密な論理的議論を構築
3. 関数型プログラミング
プログラミング方法およびプログラミングと論理学
の橋渡し
4. 形式的手法
プログラムの性質の論証
5. 型システム
プログラムの振舞いが適切である保証
33