3. Untyped Arithmetic Expressions

まずは話題の対象として、プログラミング言語の基本的な側面を持つシンプルな言語を考える。これに厳密な定義をあたえることで、数学的に扱いやすい道具とし、今後もこれを発展させながら利用していくことになる。今回は真偽値と数値のみを扱えるような言語。

言語は、文法（syntax）と意味論（semantics）を定義することで定義される。文法は計算をどのように表わすかという決まりで、それ自体では意味を持たない。これをどのように解釈して人間の考えるような意味を導き出すか、というのが意味論。どちらも厳密に定義されるので、これに従えば人間でも機会でも同じように文法を解釈し、意味を導出できる。

3.1 Introduction

ここで紹介されてる文法では succ true みたいな一見意味のない項も可能なわけで、人間はこれを見ればオイオイ、と思うけど文法的にはまったく問題ない。こういう誤りを防ぐのが型システムでもある。

3.2 Syntax

ここでは文法的な定義をしているだけなので、その意味というのは考えない。とりあえずここでは人間の考える（true/false/if だけの）計算のメンタルモデルがうまいこと形式的に表現できるように注意深く定義してやる。「意味」を考えるのはそのあと。

3.4 Semantic Styles

意味論（semantics）というのはこうやって作りあげた形式的な言語に、どうやって人間が想定するような「意味」を与えるか（どう評価するか）、というもの。これも厳密に与えることができる。

意味論にもいくつかの方法がある:

Operational semantics: 操作的意味論。項に対する操作を定義することで、項の意味を導くもの。この本ではこれを使う。
Denotational semantics: 数学的な対象を「意味」として、項から対象への関数を考えるようなもの。Domain theory と関係があるらしい。
Axiomatic semantics: 不変条件（invariant）と関係があるらしい？　項の評価じゃなくルール自体をその意味とする？　なんとなくイメージできる気はするけど具体的に分からないのでスルー。

3.5 Evaluation

Def. 3.5.2

何か直感的に分からない。ある規則を満たす（satisfy）関係は、その規則のすべてのインスタンスにおいて、結論（conculusion）がその関係に含まれているか、または前提（premise）のいずれかが関係に含まれていない。この後半がよくわからなくて、前提が関係に含まれているとどう不味いんだろう……。少なくとも今考えている言語はシンプルすぎていい具体例が挙げられなそう。

導出（derivation）というのは一つの evaluation statement \(t \longrightarrow t'\) を言語のルール（E-IFTRUE とか）から（直感的には、「縦に」）導くもの。矢印を横につなげていく操作ではない。

Thm 3.5.7

今のシンプルな言語では、全ての normal form は value であるけれど、今後そうとは限らない（run-time error となるものもある）。

Ex. 3-5-13

構造的帰納法により示す。

\[t = \mathrm{if} \; t_1 \; \mathrm{then} \; t_2 \; \mathrm{else} \; t_3\]

の場合だけ考えればよい。それ以外の場合は元の証明と同様。

\[t_1 \longrightarrow t_1', \; t_2 \longrightarrow t_2'\]

に対し、 E-If と E-Funny2 により

\[t \longrightarrow \mathrm{if} \; t_1' \; \mathrm{then} \; t_2 \; \mathrm{else} \; t_3 = t_A \\ t \longrightarrow \mathrm{if} \; t_1 \; \mathrm{then} \; t_2' \; \mathrm{else} \; t_3 = t_B\]

であり、\(t\) から導出されるのはこの \(t_A, t_B\) しか存在しない。これらに関して

\[t_A \longrightarrow^* u_A \\ t_B \longrightarrow^* u_B\]

（\(u_A, u_B\) は値）

であるとき、\(u_A = u_B\) であることを示す。

先の導出について、E-IF と E-FUNNY2 をそれぞれもう一方に適用すると

\[t_A \longrightarrow \mathrm{if} \; t_1' \; \mathrm{then} \; t_2' \; \mathrm{else} \; t_3 \\ t_B \longrightarrow \mathrm{if} \; t_1' \; \mathrm{then} \; t_2' \; \mathrm{else} \; t_3\]

であるので、帰納法の仮定より \(u_A = u_B\)。

Ex. 3.5.14

succ(false) はこれいじょう導出できない（normal form である）が値ではなくエラー。こういう項を stuck と呼ぶ。

Ex. 3.5.16

badnat, badbool, wrong による stuck の表現。

とにかく何でも評価することができて、最後には値か、そうでなければ（= stuck となる場合）wrong に評価される、という風になっていればよいと思う。なので、

すべての値または wrong を除く項が評価可能であればよい。
構造的帰納で証明できそうということで省略。

Ex. 3.5.17

Operational semantics のもう一つの一般的なスタイル、big-step (natural semantics) について。項が最終的にどんな値に評価されるか、という観点の関係 \(\Downarrow\) を用意し、それに基いた導出をおこなうスタイル。ちなみにこれまでやってきたのは small-step である。ここでこの 2 つのスタイルが一致すること、つまり \(t \longrightarrow^* v \iff t \Downarrow v\) を示す。

構造的帰納法により示す。

\[t = \mathrm{if} \; t_1 \; \mathrm{then} \; t_2 \; \mathrm{else} \; t_3\]

の場合だけを考える。

\(\Longleftarrow\) について。

\(t \Downarrow v\) とする。これを導出できたのは B-IfTrue か B-IfFalse のどちらかである。

B-IfTrue の場合を考えると、\(t_1 \Downarrow \mathrm{true}\), \(t_2 \Downarrow v\) である。すると帰納法の仮定より

\[t_1 \longrightarrow^* \mathrm{true} \\ t_2 \longrightarrow^* v\]

\(t_1 \longrightarrow^* \mathrm{true}\) のとき \(\mathrm{if} \; t_1 \; \mathrm{then} \; t_2 \; \mathrm{else} \; t_3 \longrightarrow^* t_2\) であることはすぐに示せる。結局

\[t \longrightarrow^* t_2 \longrightarrow^* v\]

B-IfFalse の場合も同様。

\(\Longrightarrow\) について。

\(t \longrightarrow^* v\) とする。

\(t_1 \longrightarrow^* \mathrm{true}\) とすると \(t \longrightarrow^* t_2\)。ここで

\[t \longrightarrow^* t_2 \longrightarrow^* v_2\]

とすると定理 3.5.11 より \(v_2 = v\)。よって

\[t_1 \Downarrow \mathrm{true} \\ t_2 \Downarrow v\]

B-IfTrue より \(t \Downarrow v\)。\(t_1 \longrightarrow^* \mathrm{false}\) の場合も同様。それ以外の場合 \(t\) は stuck する。