「型システム」とは

1. プログラミング言語的に
   プログラムの各式などをその値の種類 (型 type) に即して分類することによって、プログラムが正しく振る舞うことを保証する手法。
2. 一般的に
   論理学、数学、哲学など、広範囲。
   論理的パラドックスを解消する手段として、形式化される。
3. 計算機科学における研究的に
   - プログラミング言語への応用として (この本)
   -「計算機プログラム」と「論理学の証明」が一対一対応すること (Curry-Howard 対応) を前提に、プログラム項と論理とのつながりに着目したもの

型システムを搭載した言語を作るのならば、
型検査を考慮した上で言語設計をするべきである。
理由は以下の二つ。

• 型検査を不可能にする機能が推奨されているような言語には型システムは組み込みにくい
• 型注釈を考えた上での構文設計

型システムが使われた歴史
[1950s]整数と浮動小数点数の分類
[1950s - 1960s]データ構造、高階関数の分類
[1970s]パラメータ多相、抽象データ型
etc...

略

略

略

略

略

略

言語の抽象構文を、以下のように定義する。

定義 3.1.0 [バッカス記法 (BNF: Backus Nauer Form) による構文の定義]

t	::=	true
		false
		if t then t else t
		0
		succ t
		pred t
		iszero t

• この言語では、数字「1」は succ (0)、数字「3」は succ (succ (succ (0))) で表されるが、以下では簡単のため、アラビア数字のまま記述する。
• if false then 0 else 1 => 1
• iszero (pred (succ (0))) => true
• 評価の結果を表す項は「値」と呼ばれ、この場合、数かブール値のどちらかである。
• 結合の曖昧性は、文法には生じない。構文解析の過程で結合は一意に定まる。

定義 3.2.1 帰納的な項 による構文の定義

項の集合とは以下の条件を満たす最小の集合 Τ である。
(1) {true, false, 0} ⊆ Τ
(2) t1 ∈ Τ ならば {succ t1, pred t1, iszero t1} ⊆ Τ
(3) t1 ∈ Τ かつ t2 ∈ Τ かつ t3 ∈ Τ ならば if t1 then t2 else t3 ∈ Τ

定義 3.2.2 推論規則 による構文の定義

true ∈ Τ

false ∈ Τ

0 ∈ Τ

t1 ∈ Τ succ t1 ∈ Τ

t1 ∈ Τ pred t1 ∈ Τ

t1 ∈ Τ iszero t1 ∈ Τ

t1 ∈ Τ t2 ∈ Τ t3 ∈ Τ if t1 then t2 else t3 ∈ Τ

★これの読み方→

S1 ... Sn Sn+1

前提 S1, ... , Sn が成立するのなら、結論 Sn+1 が導出される。
前提の論理式列が空の推論規則は、公理と呼ばれる。

定義 3.2.3 具体的な項の定義

各自然数iについて、集合Siを以下のように定義する。

S0	=	Ø
Si+1	=	{true, false, 0} ∪
		{succ t1, pred t1, iszero t1|t1 ∈ Si}∪
		{if t1 then t2 else t3|t1,t2,t3 ∈ Si}

S	=	∪	Si
		i

つまり、

S0	=	Ø
S1	=	{true, false, 0}
	=	{定数}
S2	=	{定数} ∪
		{再帰部分が S1の要素(定数) で成る succ/pred/iszero/if 式}
S3	=	{定数} ∪
		{再帰部分が S2の要素(定数 or 「再帰部分が 定数 で成る succ/pred/iszero/if 式」) で成る succ/pred/iszero/if 式}
S4	=	{定数} ∪
		{再帰部分が S3の要素(定数 or 「再帰部分が 定数 or 「再帰部分が 定数 で成る ... 式」 で成る ... 式」) で成る succ/pred/iszero/if 式}
...
Sn+1	=	{定数} ∪
		{再帰部分が Snの要素で成る succ/pred/iszero/if 式}
...

演習 3.2.4 S3がもつ要素の数を答えよ。

|S1|	=	3
|S2|	=	3 + |S1| * 3 + |S1| * |S1| * |S1|
	=	39
|S3|	=	3 + |S2| * 3 + |S2| * |S2| * |S2|
	=	59439

演習 3.2.5 集合Siが累積的であることを示せ。

ここでは、

• 定数の集合を N とかく。
• 再帰部分が 集合 X の要素 からなる succ/pred/iszero/if 式の集合を、A(X)とかく。

Si ⊆ Si+1 であることを、Siについての帰納法で示す。
補題 3.2.5.1 X1 ⊆ X2 ならば、 A(X1) ⊆ A(X2) であることを示す。

任意の x ∈ X1 について、
succ x, pred x, iszero x ∈ A(X1) であり、
succ x, pred x, iszero x ∈ A(X2) (x ∈ X2 より)

任意の x, y, z ∈ X1 について、
if x then y else z ∈ A(X1) であり、
if x then y else z ∈ A(X2) (x, y, z ∈ X2 より)

すなわち、
「任意の t ∈ A(X1) について、t ∈ A(X2)」である。
したがって、 A(X1) ⊆ A(X2) ■

(1) S0 ⊆ S1
S0 = Ø ⊆ S1 = {true, false, 0}

(2) Sn ⊆ Sn+1 のとき、Sn+1 ⊆ Sn+2
*1 Sn+1 = N ∪ A(Sn)
*2 Sn+2 = N ∪ A(Sn+1)

Sn+1	=	N ∪ A(Sn)	(*1)
	⊆	N ∪ A(Sn+1)	(Sn ⊆ Sn+1, 補題 3.2.5.1)
	=	Sn+2	(*2)

命題 3.2.6 Τ = S

*1) Τは全ての「定義3.2.1にある 条件(1)(2)(3) を満たす集合」のうち、最小のものである。

(a) Τ ⊆ S

*2) Sは「定義3.2.1にある 条件(1)(2)(3) を満たす集合」である。

条件(1)
{true, false, 0} = S1 ⊆ S

条件(2)
s1 ∈ S のとき、ある n ついて s1 ∈ Sn である。
集合Sn+1は、再帰部分が 集合Snの要素 から成る succ/pred/iszero 式を全て要素に持つので、
{succ s1, pred s1, iszero s1} ⊆ Sn+1
Sn+1 ⊆ S であるから、{succ s1, pred s1, iszero s1} ⊆ S

条件(3)
s1, s2, s3 ∈ S のとき、ある n1, n2, n3 について s1 ∈ Sn1, s2 ∈ Sn2, s3 ∈ Sn3 である。
n1, n2, n3 のうち、最も左にある最大の自然数を n_max、他2つの自然数を m1, m2 とすると、
演習3.2.5 より、Sm1, Sm2 ⊆ Sn_max である。
したがって、s1, s2, s3 ∈ Sn_max
集合Sn_max+1は、再帰部分が 集合Sn_maxの要素 から成る if 式を全て要素に持つので、
if s1 then s2 else s3 ∈ Sn_max+1
Sn_max+1 ⊆ S であるから、 if s1 then s2 else s3 ∈ S

*1, *2より、Τ ⊆ S


(b) S ⊆ Τ

*1より、Sが、(Τと同様に) 全ての「定義3.2.1にある 条件(1)(2)(3) を満たす集合」のうち、最小のものであることを示せばよい。
すなわち、
「定義3.2.1にある 条件(1)(2)(3) を満たす集合」であるような任意の集合 S' について、S ⊆ S' である
ことを示せばよい。

★任意のiについて、Si ⊆ S' を示す。

1) S0 = Ø ⊆ S'

2) Si ⊆ S' ならば、Si+1 ⊆ S'

任意の s ∈ Si+1 について、

Si+1	=	N ∪ A(Si)
	⊆	N ∪ A(S')	...(補題 3.2.5.1より)
	=	N ∪ {再帰部分がS'の要素であるsucc/pred/iszero/if 式}
	⊆	N ∪ S'	...(S'が満たす条件(2)(3)より)
	=	S'	...(S'が満たす条件(1) N ⊆ S' より)

★S ⊆ S'を示す。

「X ⊆ A, Y ⊆ Aのとき、X ∪ Y ⊆ A」(証明略) なので、
S0 ⊆ S', S1 ⊆ S', ..., Sn ⊆ S', ... に対して、
( ... ( ... (S0 ∪ S1) ∪ ... ∪ Sn) ∪ ... ) = S ⊆ S'

<疑問>
下の 補題 3.2.6.1 と、(b) により、Τ = S は示せる？

補題 3.2.6.1 集合の集合A に 最小の集合が存在するのなら、それは一意に定まる。

X1, X2 ⊆ A について、X1, X2 が 最小の集合 であるとする。

1) X1 ⊆ X2
X1は前提より、任意の X ⊆ A について X1 ⊆ X である。
X2 ⊆ A であるので、 X1 ⊆ X2
2) X2 ⊆ X1
同様

1),2)より X1 = X2

<帰納的定義>
項の集合上の関数を帰納的に定義する。

定義 3.3.1. 項tに現れる定数の集合を Consts(t) と書き、次のように定義する。

Consts(true)	=	{true}
Consts(false)	=	{false}
Consts(0)	=	{0}
Consts(succ t1)	=	Consts(t1)
Consts(pred t1)	=	Consts(t1)
Consts(iszero t1)	=	Consts(t1)
Consts(if t1 then t2 else t3)	=	Consts(t1) ∪ Consts(t2) ∪ Consts(t3)

定義 3.3.2. 項tのサイズをsize(t)と書き、次のように定義する。

size(true)	=	1
size(false)	=	1
size(0)	=	1
size(succ t1)	=	size(t1) + 1
size(pred t1)	=	size(t1) + 1
size(iszero t1)	=	size(t1) + 1
size(if t1 then t2 else t3)	=	size(t1) + size(t2) + size(t3) + 1

size(t) は t の抽象構文木のノードの数に等しい。
項 t の抽象構文木の深さを求める関数 depth は以下のように定義できる。

depth(true)	=	1
depth(false)	=	1
depth(0)	=	1
depth(succ t1)	=	depth(t1) + 1
depth(pred t1)	=	depth(t1) + 1
depth(iszero t1)	=	depth(t1) + 1
depth(if t1 then t2 else t3)	=	max(depth(t1), depth(t2), depth(t3))

<帰納的証明>
項の性質を帰納的に証明する。

補題 3.3.3. ある項 t について、|Consts(t)| <= size(t)

t の深さに関する帰納法を用いる。

i) t が 定数 のとき
|Consts(t)| = 1 <= size (t) = 1

ii) t = succ t1 または t = pred t1 または t = iszero t1 のとき

|Consts(t)|	=	|Consts(t1)|	(Constsの定義より)
	<=	size(t1)	(帰納法の仮定より)
	<=	size(t1) + 1
	=	size(t)

iii) t = if t1 then t2 else t3 のとき

|Consts(t)|	=	|Consts(t1) ∪ Consts(t2) ∪ Consts(t3)|	(Constsの定義より)
	=	|Consts(t1)| + |Consts(t2)| + |Consts(t3)|
	<=	size(t1) + size(t2) + size(t3)	(帰納法の仮定より)
	<=	size(t1) + 1
	=	size(t)

定理 3.3.4. [項に関する帰納法の原理] Pが項に関する述語であるとする。

深さに関する帰納法:
「任意の項 s に対して以下が成り立つならば、P(s)が成り立つ。
depth(r) < depth(s) なる任意の r において P(r) が成り立つとき、P(s) も証明できる。」
ならば、すべてのsに対して P(s) が成り立つ。

サイズに関する帰納法:
略

構造的帰納法:
略

1. 操作的意味論
振る舞いが遷移関数で定義されるような抽象機械を考え、
その遷移関数によって起こる状態変化によって、プログラム各語句の意味を説明する。

2. 表示的意味論
プログラムの実行過程を抽象化し、プログラムの入出力を意味領域への数学的な写像に例えて説明する。
表示的意味を与えるということは、「項を特定の意味領域に写すような解釈関数を定義する」ということである。
表示的意味論を用いると、実際のプログラム評価の裏で行われるような生々しい詳細を取り去り、言語の本質的な概念を浮き彫りにすることができる。

3. 公理的意味論
数理論理学に基づいてプログラムの意味を説明する。

t	:=		項:
		true	定数真
		false	定数偽
		if t then t else t	条件式
v	:=		値:
		true	真
		false	偽

評価

	E-IfTrue
if true then t2 else t3 -> t2

	E-IfFalse
if false then t2 else t3 -> t3

t1 -> t1'	E-If
if t1 then t2 else t3 -> if t1' then t2 else t3

定義 3.5.1. 推論規則のインスタンスとは、結論部や前提部に現れるメタ変数それぞれが、具体的な一意の項に書き換えられたものである

定義 3.5.2. 規則が関係pによって満たされるとは、規則の任意のインスタンスについて、結論部がある関係pに属するか、前提のうちの一つが関係pに属さないことである。

定義 3.5.3. 1ステップ評価関係 -> とは、図3-1の三つの規則を満たす、項に関する最小の二項関係である。(t, t') がこの評価関数の元であるとき、「評価関係式 t -> t' は導出可能である」という。

導出可能な評価関係式 t -> t' としたとき、またそのときのみ、t -> t' について以下の 1, 2 どちらかが成り立つ。
1. 公理 E-IfTrue, E-IfFlase のインスタンスである。
2. 前提も同様に導出可能である 規則 E-If のインスタンスの結論部である。

評価関係式が導出可能であることの証明は
・根がその評価関係式
・葉が公理 E-IfTrue, E-IfFlase のインスタンス
・節がその直属の子を前提部とするような規則 E-If のインスタンスの結論部
であるような導出木を示せばよい。(導出木の例: p.27 上)

「評価関係式が導出可能である」ことと、「その評価関係式を根に持つ導出木が存在する」ことが同値であるという事実から、導出に関する帰納法という証明技法を直接導ける。


定理 3.5.4. [1ステップ評価の決定性] t -> t' かつ t -> t'' ならば t' = t''

t -> t' の導出に関する帰納法を使う。
すべての t -> t' より小さい導出に関して、当定理が成立することを仮定する。
(「小さい導出」 = t -> t' を根に持つ導出木を考えたとき、その前提部に構築された部分導出木の各節、葉の導出。)

i) t -> t' が公理 E-IfTrue のインスタンスである場合
*1) すなわち、ある項 t3 に対し t = if true then t' else t3

i-a) t -> t'' が公理 E-IfTrue のインスタンスである場合
ある項 t3' に対し、 t = if true then t'' else t3' である。
*1 より、 t' = t''

i-b) t -> t'' が公理 E-IfFalse のインスタンスである場合
t がある項 t2 に対し、 if false then t2 else t'' の形である必要があるが、 *1 に矛盾

i-c) t -> t'' が規則 E-If のインスタンスの結論部である場合
前提部として、ある項 t1, t1' に対し t1 -> t1' が導出可能である必要がある。
*1 より t1 = true であるが、true は何にも評価されないので、矛盾。


ii) t -> t' が公理 E-IfFalse のインスタンスである場合
すなわち、ある項 t2 に対し t = if false then t2 else t'

ii-b) t -> t'' が公理 E-IfFalse のインスタンスである場合
i) と同様にして、t' = t''

ii-a) t -> t'' が公理 E-IfTrue のインスタンスである場合
ii-c) t -> t'' が規則 E-If のインスタンスの結論部である場合
i) と同様にして、矛盾。


iii) t -> t' が公理 E-If のインスタンスの結論部である場合
すなわち、ある項 t1, t1', t2, t3 に対して、
・t1 -> t1' が導出可能
・t = if t1 then t2 else t3
・t' = if t1' then t2 else t3

ii-a) t -> t'' が公理 E-IfTrue のインスタンスである場合
t = if true then t'' else t3'、すなわち t1 = true となるが、
true は何にも評価されず、 t1 -> t1' が導出可能であることに矛盾。

ii-b) t -> t'' が公理 E-IfFalse のインスタンスである場合
同様に、矛盾。

ii-c) t -> t'' が規則 E-If のインスタンスの結論部である場合
ある項 t4, t4', t5, t6 に対して、
・t4 -> t4' が導出可能
・t = if t4 then t5 else t6
・t'' = if t4' then t5 else t6
となる。
すなわち、t1 = t4, t2 = t5, t3 = t6 であり、まとめると、
・t1 -> t1' が導出可能
・t1 -> t4' が導出可能
・t = if t1 then t2 else t3
・t' = if t1' then t2 else t3
・t'' = if t4' then t2 else t3
ここで、導出 t1 -> t1', t1 -> t4' はそれぞれ、t -> t' と t -> t'' の部分導出なので、帰納法の仮定を適用できる。
このため、 t1' = t4'
したがって、 t' = t'' である。


演習 3.5.5. 上の証明で使われている帰納法の原理を定理 3.3.4. のスタイルで抜き出せ。

導出に関する帰納法:
G が項に関する述語であると仮定する。
各導出 p に対して、
すべての p より小さい導出 p' に対して G(p') が成り立つとき、
G(p) が証明できる

ならば、すべての p に対して G(p) が成り立つ。


定義 3.5.6 項が正規形であるとは、当てはまる評価規則がない、つまり t -> t' となる t' が存在しないということである。

true, false は正規形である。

定理 3.5.7. すべての値は正規形である

この体系では定理 3.5.7. の逆も成り立つ。
つまり、「すべての正規形は値である。」
一般的に、これは成り立たたず、値ではない正規形も存在する。
値ではない正規形は、後の章で実行時エラーの解析する際に重要になる。

定理 3.5.8. t が正規形であるならば、t は値である。

対偶「t が値がでないなら、t は正規形でない」を
t に対する構造的帰納法で示す。
t は値ではないので、ある t1, t2 t3 に対し、
if t1 then t2 else t3 の形をしているはずである。

i) t1 = true の場合
E-IfTrue の左側に適合する (当てはまる評価規則が存在する) ため、t は正規形でない。

ii) t1 = false の場合
i と同様にして、t は正規形でない。

iii) それ以外の場合
t1 は値ではない。
帰納法の仮定により、 t1 は正規形でない。
つまり、ある t1' が存在し、 t1 -> t1' が導出可能である。
このことより、t は、t1 -> t1' を前提として規則 E-If を適合可能である。
したがって、t は正規形でない。


定義 3.5.9. 多ステップ評価関係 ->* とは 1ステップ評価の反射的推移的閉包である。つまり、以下の3条件を満たす最小の関係である。
(1) t -> t' ならば t ->* t'
(2) 任意の t に対し、 t ->* t
(3) t ->* t' かつ t' ->* t'' ならば、 t ->* t''

演習 3.5.10. 定義 3.5.9. を推論規則の形で再定義せよ。

t -> t' t ->* t'

t ->* t

t ->* t' t' ->* t'' t ->* t''

定理 3.5.11 [正規形の一意性] t ->* u かつ t ->* u' で、u と u' が両方正規形ならば、 u = u'

t ->* u の導出に関する帰納法で示す。

i) t = u, t = u' のとき
同値関係 = についての推移律より、u = u'

ii) t = u, t != u' のとき
u は正規形なので、t も正規形
一方、t != u' なので、t ->* u' の導出には 1ステップ以上の評価が必要である。
すなわち、ある t1 に対し、 t -> t1, t1 ->* u'
これは t が正規形であることに矛盾。

iii) t != u, t = u' のとき
ii と同様に矛盾。

iv) t != u, t != u' のとき
t != u, t != u' なので、ある t1, t1' に対して、
t -> t1, t1 ->* u
t -> t1', t1' ->* u'
1ステップ評価の決定性 (定理 3.5.4) より、t1 = t1' である。
さらに、t1 ->* u, t1' (= t1) ->* u' は
それぞれ t ->* u, t ->* u' の部分導出であるので、
帰納法の仮定より、u = u' である。


定理 3.5.12 [評価の停止性] すべての項 t に対して、ある正規形 t' が存在し、t ->* t'

i) t = true の場合
t ->* true が導出可能。

ii) t = false の場合
t ->* false が導出可能。

iii) t = if t1 then t2 else t3 の場合
a) t1 = true の場合
規則 E-IfTrue より、t -> t2、つまり t ->* t2
t2 は t の部分項。
帰納法の仮定より、ある正規形 t'' が存在し、t2 ->* t''
t ->* t2, t2 ->* t'', ->* の推移律より、t ->* t'' (t'' は正規形)

b) t1 = false の場合
同様

c) t1 = if t1' then t2' else t3' の場合
t1 は t の部分項なので、帰納法の仮定より、
t1 には 正規形 t1'' が存在する。 t1 ->* t1''
t1 は値ではないので、t1 ->* t1'' には1ステップ以上の評価が必要。
つまり、 t1 -> x, x ->* t1''
規則 E-If と、t1 -> x より、
if t1 then t2 else t3 -> if x then t2 else t3
この操作を繰り返すことにより、
if t1 then t2 else t3 ->* if t1'' then t2 else t3
が導出可能である。
t1'' は正規形であるので、定理 3.5.8.より、t1'' は値。

c-i) t'' = true の場合
t ->* if true then t2 else t3,
if true then t2 else t3 -> t2 (規則 E-IfTrueより)
t2 に帰納法の仮定を適用すると、ある正規形 t2'' に対し、 t2 ->* t2''
つまり、t ->* t2''

c-ii) t'' = false の場合
同様

演習 3.5.13.
(1) 図3-1に次の規則を追加する。

	E-Funny1
if true then t2 else t3 -> t3

このとき、定理 3.5.4, 3.5.7, 3.5.8, 3.5.11., 3.5.12 のうち成り立つままの定理はどれか。

- 定理 3.5.4: t -> t', t -> t'' ならば t' = t''
i-d) t -> t'' が規則 E-Funny1 のインスタンスである場合
ある項 t2 に対し、 t = if true then t2 else t''
一方、*1 より t = if true then t' else t3 なので、
t' = t2, t'' = t3
つまり、t' = t'' であるためには、
t がある項 x に対して、if true then x else x の形でなければならず、
これは一般的には成り立たない。

- 定理 3.5.7: すべての値は正規形である
この体系では、true, false が値であるが、これに当てはまる評価規則は相変わらずない。ゆえに、すべての値は正規形である。

- 定理 3.5.8: t が正規形ならば、tは値である。
今までと同様に示せる。

- 定理 3.5.11: t ->* u, t ->* u' で、u と u' が正規形なら、u = u'
定理3.5.4が成り立たないので、不成立。

- 定理 3.5.12: すべての項 t に対して、ある正規形 t' が存在し、t ->* t'
今までの規則で「ある正規形 t' が(すくなくとも一つ)存在する」ことは言えていたので、新たな規則が追加された上でも成立する。


(2) 次の規則を代わりに追加する。

t2 -> t2'	E-Funny2
if t1 then t2 else t3 -> if t1 then t2' else t3

このとき、上の定理のうち成り立つままのものはどれか。それぞれの証明は変更する必要があるか。

(1)のように、証明をなぞらえるだけなので、省略。


以降、評価の定義を算術式に拡張する。

t	:=		項:
		0	定数ゼロ
		succ t	後者値
		pred t	前者値
		iszero t	ゼロ判定
v	:=		値:
		nv	数値
nv	:=		数値:
		0	ゼロ
		succ nv	後者値

t1 -> t1'	E-Succ
succ t1 -> succ t1'

	E-PredZero
pred 0 -> 0

	E-PredSucc
pred (succ nv1) -> nv1

t1 -> t1'	E-Pred
pred t1 -> pred t1'

	E-IsZeroZero
iszero 0 -> true

	E-IsZeroSucc
iszero (succ nv1) -> false

t1 -> t1'	E-IsZero
iszero t1 -> iszero t1'

演習 3.5.14. 定理3.5.4 が算術演算の評価関係に関しても成り立つことを示せ。すなわち、t -> t' かつ t -> t'' ならば t' = t''

・定理3.5.4 の証明と同様。
・t -> t' の導出による帰納法で示す。
・t -> t', t -> t'' がどの規則を適用して得られたものか、で場合分けを行う。

言語の操作的意味論を形式化すると、全ての項の振る舞いが規定される。
pred 0 は 0 と定義してある一方、
succ false には評価規則が定義されていない。(正規形である)
このような項を行き詰まり状態であるという。

定義 3.5.15. 項が正規形であるが値ではないとき、その項は行き詰まり状態であるという。

この「行き詰まり状態」によって、実行時エラーを単純に表すことができる。
直感的には、プログラムが「無意味な状態」に辿り着き、これ以上の評価方法がわからない、という状況である。
言語の具体的な実装には実際にはさまざまな種類の不具合 (セグメンテーション等) があるが、それら全てまとめてここでは「行き詰まり状態」と呼ぶ。

演習 3.5.16.
wrong と呼ばれる新しい項を導入し、今の意味論では行き詰まり状態になってしまう状況すべてで wrong を明示的に生成するため、新しい構文規則を二つ加える。

badnat	:=		数でない正規形:
		wrong	実行時エラー
		true	定数真
		false	定数偽
badbool	:=		ブール値でない正規形:
		wrong	実行時エラー
		nv	数値

	E-If-Wrong
if badbool then t1 else t2 -> wrong

	E-Succ-Wrong
succ badnat -> wrong

	E-Pred-Wrong
pred badnat -> wrong

	E-IsZero-Wrong
iszero badnat -> wrong

実行時エラーの二つの取り扱いが一致することを、(1)正確に説明し、(2)証明せよ。

(1)
今までの公理規則には、
・succ/pred/iszero式は再帰部分に数値だけが現れる
・if式は条件部分にブール値だけが現れる
ものしかなかったが、これが行き詰まり状態を起こす原因となっていた。
これを解消するため(実行時エラーを捕捉するため)
・succ/pred/iszero式は再帰部分にブール値が現れる
・if式は条件部分に数値が現れる
ような規則を追加し、行き詰まり状態に陥入れば、必ず wrong に評価されるように評価関係を追加している点で、二つの取り扱いは一致している。

(2)
-

演習 3.5.17. 操作的意味論には、評価の遷移を1ステップごとに書き出す「小ステップスタイル」、多数回の評価ステップを通じ最終的にどんな値に評価されるのかを定式化する「大ステップ意味論(自然意味論)」がある。

	B-Value
v ↓ v

t1 ↓ true	t2 ↓ v2	B-IfTrue
if t1 then t2 else t3 ↓ v2

t1 ↓ false	t3 ↓ v3	B-IfFalse
if t1 then t2 else t3 ↓ v3

t1 ↓ nv1	B-Succ
succ t1 ↓ succ nv1

t1 ↓ 0	B-PredZero
pred t1 ↓ 0

t1 ↓ 0	B-PredSucc
pred t1 ↓ nv1

t1 ↓ succ nv1	B-IsZeroSucc
iszero t1 ↓ false

この言語において、小ステップと大ステップの意味論が一致すること、つまり、t ->* v のとき、かつそのときに限り t ↓ v が成り立つことを示せ。

(i) t ->* v ならば t ↓ v

a) t = v
t ->* v であるが、規則B-Valueにより、v ↓ v

b) t = succ t1
t1 ->* v1 とする。
規則E-Succのステップ数ぶんの適用により、
succ t1 ->* succ v1
(つまり、t ->* succ v1)

帰納法の仮定より、t1 ↓ v1
規則 B-Succ により、succ t1 ↓ succ v1

c) t = pred t1
同様

d) t = iszero t1
d-i) t1 = 0
規則 E-IsZeroZeroより、t ->* true
規則 B-Value, 規則 B-IsZeroZero より、t ↓ true

d-ii) t1 = succ t1'
t1' ->* v1 とすると、
規則 E-Succ の多数回の適用により、
succ t1' ->* succ v1
つまり、t1 ->* succ v1
規則 E-IsZero の多数回の適用により、
iszero t1 ->* iszero (succ v1)
規則 E-IsZeroSucc より、
iszero (succ v1) -> false
したがって、t ->* false

帰納法の仮定から、t1' ↓ v1
規則 B-Succ から、 succ t1' ↓ succ v1
規則 B-IsZeroSucc から、 iszero (succ t1') ↓ false

e) t = if t1 then t2 else t3
e-i) t1 = true
t -> t2 (規則 E-IfTrue より)
t2 ->* v を仮定すると、
帰納法の仮定から、t2 ↓ v
規則 B-IfTrue より、t ↓ v

e-ii) t1 = false
同様

e-iii) それ以外
t1 ->* v1 を仮定する。
規則 E-If の多数回の適用により、
t ->* if v1 then t2 else t3

e-iii-i) v1 = true
規則 E-IfTrue より、t ->* t2
t2 ->* v を仮定する。(つまり、t ->* v)
帰納法の仮定より、t2 ↓ v
規則 B-IfTrue より、 t ↓ v

e-iii-ii) v1 = false
規則 E-IfFalse より、t ->* t3
t3 ->* v を仮定する。(つまり、t ->* v)
昨日法の仮定より、t3 ↓ v
規則 B-IfFalse より、 t ↓ v


(ii) t ↓ v ならば t ->* v

a) t = v
t ->* v (0ステップ)

b) t = succ t1
b-i) 最後に適用した規則が B-Succ
ある数値 nv1 に対し、
・t1 ↓ nv1
・v = succ nv1
帰納法の仮定から、t1 ->* nv1
これに 規則E-Succ を複数ステップ適用することにより、
succ t1 ->* succ nv1
つまり、t ->* v を得る。

c) t = pred t1
同様

d) t = iszero t1
d-i) 最後に適用した規則が B-IsZeroZero
・t1 ↓ 0
・v = true
帰納方の仮定から t1 ->* 0
規則 E-IsZeroより、iszero t1 ->* iszero 0
規則 E-IsZeroZeroより、iszero t1 ->* true、
すなわち、 t ->* v が導ける。

d-ii) 最後に適用した規則が B-IsZeroSucc
ある数値 nv1 に対し、
・t1 ↓ succ nv1
・v = false
帰納法の仮定から t1 ->* succ nv1
規則 E-IsZero から、 iszero t1 ->* iszero (succ nv1)
規則 E-IsZeroSucc から、iszero t1 ->* false、
すなわち、t ->* v が導ける。

e) t = if t1 then t2 else t3
e-i) 最後に適用した規則が B-IfTrue
ある値 v2 に対して、
・t1 ↓ true
・t2 ↓ v
帰納法の仮定から、t1 ->* true, t2 ->* v
規則 E-If から、t ->* if true then t2 else t3
規則 E-IfTrue から、t ->* t2
したがって、 t ->* v

e-ii) 最後に適用した規則が B-IfFalse
同様


演習 3.5.18. 評価戦略を変えて、 if t1 then t2 else t3 が t2, t3, t1 の順で評価されるようにしたいとする。評価規則をどう変更すればよいか。

t2 -> t2'
if t1 then t2 else t3 -> if t1 then t2' else t3

t3 -> t3'
if t1 then v else t3 -> if t1 then v else t3'

t1 -> t1'
if t1 then v2 else v3 -> if t1' then v2 else v3

if true then v2 else v3 -> v2

if false then v2 else v3 -> v3

略