7.4 算術式

プログラミング言語に欠かせない機能の一つが式の評価である。式の処理を考える上では、式を再帰的データ型として扱うことが鍵となる。

このアプローチを説明するために、本節では \(x\) だけを変数に持つ \(3x^{2} + 2x + 1\) といった算術式を考える。こういった算術式のデータ型を \(\text{Aexp}\) と呼ぶ。その定義を次に示す:

定義 7.4.1

集合 \(\text{Aexp}\) を次のように定義する。

ベースケース:

変数 \(x\) は \(\text{Aexp}\) に属する。
任意の非負整数 \(k\) を表すアラビア数字 \(\texttt{k}\) は \(\text{Aexp}\) に属する。

構築ケース: \(e, f \in \text{Aexp}\) とする。このとき:

\({\color{red} \,\textbf{\textsf{[}}\,} e + f {\color{blue} \,\textbf{\textsf{]}}\,} \in \text{Aexp}\) が成り立つ。式 \({\color{red} \,\textbf{\textsf{[}}\,} e + f {\color{blue} \,\textbf{\textsf{]}}\,}\) を和 (sum) と呼ぶ。この和の要素 (component) とは \(e\), \(f\) を指す。
\({\color{red} \,\textbf{\textsf{[}}\,} e \ast f {\color{blue} \,\textbf{\textsf{]}}\,} \in \text{Aexp}\) が成り立つ。式 \({\color{red} \,\textbf{\textsf{[}}\,} e \ast f {\color{blue} \,\textbf{\textsf{]}}\,}\) を積 (product) と呼ぶ。この積の要素 (component) とは \(e\), \(f\) を指す。
\(- {\color{red} \,\textbf{\textsf{[}}\,} e {\color{blue} \,\textbf{\textsf{]}}\,} \in \text{Aexp}\) が成り立つ。式 \(- {\color{red} \,\textbf{\textsf{[}}\,} e {\color{blue} \,\textbf{\textsf{]}}\,}\) を負項 (negative) と呼ぶ。

\(\text{Aexp}\) の要素には完全に括弧が付いていること、そして冪乗を表す記号が存在しないことに注意してほしい。そのため多項式 \(3x^{2} + 2x + 1\) に対応する \(\text{Aexp}\) の要素は次のように書かなければならない:

\[ {\color{red} \,\textbf{\textsf{[}}\,} {\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \ast {\color{red} \,\textbf{\textsf{[}}\,} x \ast x {\color{blue} \,\textbf{\textsf{]}}\,} {\color{blue} \,\textbf{\textsf{]}}\,} + {\color{red} \,\textbf{\textsf{[}}\,} {\color{red} \,\textbf{\textsf{[}}\,} \texttt{2} \ast x {\color{blue} \,\textbf{\textsf{]}}\,} + \texttt{1} {\color{blue} \,\textbf{\textsf{]}}\,} {\color{blue} \,\textbf{\textsf{]}}\,} \tag{7.8}\]

人間にとって括弧と \(\ast\) は見にくいだけなので、これからは式 \(\text{(7.8)}\) のようには書かず \(3x^{2} + 2x + 1\) などと省略して表記する。ただ、多項式 \(3x^{2} + 2x + 1\) が \(\text{Aexp}\) の要素ではないことは重要な事実である: \(3x^{2} + 2x + 1\) は \(\text{Aexp}\) の要素 \(\text{(7.8)}\) を表す省略記法に過ぎない。

7.4.1 評価と置換

評価

\(\text{Aexp}\) の任意の要素に含まれる変数は \(x\) だけなので、その値は \(x\) の値から求まる。例えば \(x\) の値が \(3\) のとき \(3x^{2} + 2x + 1\) の値は \(34\) である。一般に、\(\text{Aexp}\) の要素 \(e\) と \(x\) の値となる整数 \(n\) が与えられたとき、\(x\) の値が \(n\) であるときの \(e\) の値 \(\operatorname{eval}(e, n)\) を計算する処理を式 \(e\) の評価 (evaluation) と呼ぶ。式の評価は再帰的に定義するのが簡単かつ有用である:

定義 7.4.2

評価関数 (evaluation function) \(\operatorname{eval}\colon \text{Aexp} \times \mathbb{Z} \to \mathbb{Z}\) は、任意の非負整数 \(n\) と式 \(e \in \text{Aexp}\) に対して次の規則で再帰的に定義される:

ベースケース:

\[ \operatorname{eval} (x, n) ::= n \hspace{14.5em} \tag{7.9}\]

\[ \operatorname{eval} (\texttt{k}, n) ::= k \quad (k \text{ はアラビア数字 } \texttt{k} \text{ が表す数値})\quad \tag{7.10}\]
構築ケース: 任意の \(e_{1}, e_{2} \in \text{Aexp}\) に対して:

\[ \operatorname{eval}({\color{red} \,\textbf{\textsf{[}}\,} e_{1} + e_{2} {\color{blue} \,\textbf{\textsf{]}}\,}, n) ::= \operatorname{eval}(e_{1}, n) + \operatorname{eval}(e_{2}, n) \tag{7.11}\]

\[ \operatorname{eval}({\color{red} \,\textbf{\textsf{[}}\,} e_{1} \ast e_{2} {\color{blue} \,\textbf{\textsf{]}}\,}, n) ::= \operatorname{eval}(e_{1}, n) \cdot \operatorname{eval}(e_{2}, n) \tag{7.12}\]

\[ \operatorname{eval}(- {\color{red} \,\textbf{\textsf{[}}\,} e_{1} {\color{blue} \,\textbf{\textsf{]}}\,}, n) ::= - \operatorname{eval}(e_{1}, n) \hspace{3.3em} \tag{7.13}\]

この再帰的定義を使うとき、\(x\) を \(2\) とした場合の \(3 + x^{2}\) の評価は次のように進行する:

\[ \begin{aligned} \operatorname{eval}({\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} + {\color{red} \,\textbf{\textsf{[}}\,} x \ast x {\color{blue} \,\textbf{\textsf{]}}\,} {\color{blue} \,\textbf{\textsf{]}}\,}, 2) &= \operatorname{eval}(\texttt{3}, 2) + \operatorname{eval}({\color{red} \,\textbf{\textsf{[}}\,} x \ast x {\color{blue} \,\textbf{\textsf{]}}\,}, 2) && (7.11 \text{ より}) \\ &= 3 + \operatorname{eval}({\color{red} \,\textbf{\textsf{[}}\,} x \ast x {\color{blue} \,\textbf{\textsf{]}}\,}, 2) && (7.10 \text{ より}) \\ &= 3 + (\operatorname{eval}(x, 2) \cdot \operatorname{eval}(x, 2)) && (7.12 \text{ より}) \\ &= 3 + (2 \cdot 2) && \ \ (7.9 \text{ より}) \\ &= 3 + 4 \\ &= 7 \end{aligned} \]

置換

変数を式で置換する操作はコンパイラや代数システムが行う基本的な操作である。例えば、\(x(x - 1)\) に含まれる \(x\) を \(3x\) に置換すると \(3x(3x-1)\) となる。一般に、\(e \in \text{Aexp}\) に含まれる全ての \(x\) を \(f \in \text{Aexp}\) で置き換えた結果を \(\operatorname{subst}(f, e)\) と表記する。例えば、先ほどの例は次の等式を表す:

\[ \operatorname{subst}(3x, x(x-1)) = 3x(3x - 1) \]

この関数は単純な再帰的定義を持つ:

定義 7.4.3

置換関数 (substitution function) \(\operatorname{subst}\colon \text{Aexp} \times \text{Aexp} \to \text{Aexp}\) は任意の \(e, f \in \text{Aexp}\) に対して次の規則で再帰的に定義される:

ベースケース:

\[ \operatorname{subst}(f, x) ::= f \tag{7.14}\]

\[ \operatorname{subst}(f,\texttt{k}) ::= \texttt{k} \tag{7.15}\]
構築ケース: 任意の \(e_{1}, e_{2} \in \text{Aexp}\) に対して:

\[ \operatorname{subst}(f, {\color{red} \,\textbf{\textsf{[}}\,} e_{1} + e_{2} {\color{blue} \,\textbf{\textsf{]}}\,}) ::= {\color{red} \,\textbf{\textsf{[}}\,} \operatorname{subst}(f, e_{1}) + \operatorname{subst}(f,e_{2}) {\color{blue} \,\textbf{\textsf{]}}\,} \tag{7.16}\]

\[ \operatorname{subst}(f, {\color{red} \,\textbf{\textsf{[}}\,} e_{1} \times e_{2} {\color{blue} \,\textbf{\textsf{]}}\,}) ::= {\color{red} \,\textbf{\textsf{[}}\,} \operatorname{subst}(f, e_{1}) \times \operatorname{subst}(f,e_{2}) {\color{blue} \,\textbf{\textsf{]}}\,} \tag{7.17}\]

\[ \hspace{-42pt}\operatorname{subst}(f, - {\color{red} \,\textbf{\textsf{[}}\,} e_{1} {\color{blue} \,\textbf{\textsf{]}}\,}) ::= -{\color{red} \,\textbf{\textsf{[}}\,} \operatorname{subst}(f, e_{1}) {\color{blue} \,\textbf{\textsf{]}}\,} \tag{7.18}\]

この再帰的定義を使って \(x(x-1)\) に含まれる \(x\) を \(3x\) で置換した結果を求めるステップを次に示す:

\[ \small\begin{aligned} & \operatorname{subst}(3x, x(x-1)) \\ & \quad = \operatorname{subst}({\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,}, {\color{red} \,\textbf{\textsf{[}}\,} x \times {\color{red} \,\textbf{\textsf{[}}\,} x + - {\color{red} \,\textbf{\textsf{[}}\,} \texttt{1} {\color{blue} \,\textbf{\textsf{]}}\,} {\color{blue} \,\textbf{\textsf{]}}\,} {\color{blue} \,\textbf{\textsf{]}}\,}) && (\text{省略記法を展開した}) \\ & \quad = {\color{red} \,\textbf{\textsf{[}}\,} \operatorname{subst}({\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,}, x) \times \operatorname{subst}({\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,}, {\color{red} \,\textbf{\textsf{[}}\,} x + - {\color{red} \,\textbf{\textsf{[}}\,} \texttt{1} {\color{blue} \,\textbf{\textsf{]}}\,} {\color{blue} \,\textbf{\textsf{]}}\,}) {\color{blue} \,\textbf{\textsf{]}}\,} && (7.17 \text{ より}) \\ & \quad = {\color{red} \,\textbf{\textsf{[}}\,} {\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,} \times \operatorname{subst}({\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,}, {\color{red} \,\textbf{\textsf{[}}\,} x + - {\color{red} \,\textbf{\textsf{[}}\,} \texttt{1} {\color{blue} \,\textbf{\textsf{]}}\,} {\color{blue} \,\textbf{\textsf{]}}\,}) {\color{blue} \,\textbf{\textsf{]}}\,} && (7.14 \text{ より}) \\ & \quad = {\color{red} \,\textbf{\textsf{[}}\,} {\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,} \times {\color{red} \,\textbf{\textsf{[}}\,} \operatorname{subst}({\color{red} \,\textbf{\textsf{[}}\,} \texttt{3}\times x {\color{blue} \,\textbf{\textsf{]}}\,}, x) \\ & \qquad\qquad\qquad\qquad\quad {} + \operatorname{subst}({\color{red} \,\textbf{\textsf{[}}\,} \texttt{3}\times x {\color{blue} \,\textbf{\textsf{]}}\,}, - {\color{red} \,\textbf{\textsf{[}}\,} \texttt{1} {\color{blue} \,\textbf{\textsf{]}}\,}) {\color{blue} \,\textbf{\textsf{]}}\,} {\color{blue} \,\textbf{\textsf{]}}\,} && (7.16 \text{ より}) \\ & \quad = {\color{red} \,\textbf{\textsf{[}}\,} {\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,} \times {\color{red} \,\textbf{\textsf{[}}\,} {\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,} + - {\color{red} \,\textbf{\textsf{[}}\,} \operatorname{subst}({\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,}, \texttt{1}) {\color{blue} \,\textbf{\textsf{]}}\,}{\color{blue} \,\textbf{\textsf{]}}\,}{\color{blue} \,\textbf{\textsf{]}}\,} && (7.14 \text{ と } 7.18 \text{ より}) \\ & \quad = {\color{red} \,\textbf{\textsf{[}}\,} {\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,} \times {\color{red} \,\textbf{\textsf{[}}\,} {\color{red} \,\textbf{\textsf{[}}\,} \texttt{3} \times x {\color{blue} \,\textbf{\textsf{]}}\,} + - {\color{red} \,\textbf{\textsf{[}}\,} \texttt{1} {\color{blue} \,\textbf{\textsf{]}}\,} {\color{blue} \,\textbf{\textsf{]}}\,} {\color{blue} \,\textbf{\textsf{]}}\,} && (7.15 \text{ より}) \\ & \quad = 3x(3x-1) && (省略記法で書き直した) \end{aligned} \]

\(x = 2\) における \(\operatorname{subst}(3x, x(x-1))\) の値を計算したいとしよう。この計算には二つのアプローチが考えられる。まず、置換を計算して \(3x(3x - 1)\) を求め、そこから \(x = 2\) における \(3x(3x - 1)\) の値 \(\operatorname{eval}(3x(3x-1), 2)\) を計算して \(30\) を得る方法がある。このアプローチは次の式で表現できる:

\[ \operatorname{eval}(\operatorname{subst}(3x, x(x-1)), 2) \tag{7.19}\]

プログラミングの言葉で、これは置換モデル (substitution model) を使った評価と呼ばれる。このアプローチでは置換の後に \(3x\) が二か所に現れ、積 \(3 \cdot 2\) の計算も二回必要になる。

二つ目のアプローチは環境モデル (environment model) を使った評価と呼ばれる。\(x = 2\) における \(\operatorname{subst}(3x, x(x-1))\) の値を計算するために、まず \(x = 2\) における \(3x\) の値 \(6\) を計算し、その値を \(x\) としたときの \(x(x-1)\) を評価し、\(6 \cdot 5 = 30\) を得る。このアプローチは次の式で表現できる:

\[ \operatorname{eval}(x(x-1), \operatorname{eval}(3x,2)) \tag{7.20}\]

環境モデルを使うと \(3x\) の値が一度しか計算されないので、置換モデルより少ない回数の乗算で同じ値を計算できる。

ここで時間を取って、ここで説明した二つのアプローチを自分の手で計算してみるとよい (問題 7.27)。

式 \(\text{(7.19)}\) と式 \(\text{(7.20)}\) の値が一致することには何の不思議もない。置換モデルと環境モデルは必ず同じ値を計算する。構造的帰納法を使うと、この事実を二つアプローチの定義から直ちに示せる。正確に言えば、証明すべき命題は次の通りである:

定理 7.4.4

全ての \(e, f \in \text{Aexp}\) と \(n \in \mathbb{Z}\) で次の等式が成り立つ:

\[ \operatorname{eval}(\operatorname{subst}(f,e), n) = \operatorname{eval}(e, \operatorname{eval}(f,n)) \tag{7.21}\]

証明 \(e\) に関する構造的帰納法で示す¹。

ベースケース:

\(e = x\) のとき、等式 \(\text{(7.21)}\) の左辺は置換関数の定義のベースケース \(\text{(7.14)}\) より \(\operatorname{eval}(f,n)\) に等しい。また、右辺は評価関数の定義のベースケース \(\text{(7.9)}\) より \(\operatorname{eval}(f,n)\) に等しい。よって等式 \(\text{(7.21)}\) は成り立つ。
\(e = \texttt{k}\) のとき、等式 \(\text{(7.21)}\) の左辺は置換関数と評価関数の定義のベースケース \(\text{(7.10)}\), \(\text{(7.15)}\) より \(k\) に等しい。また、右辺は評価関数のベースケース \(\text{(7.10)}\) より \(k\) に等しい。よって等式 \(\text{(7.21)}\) は成り立つ。

構築ケース:

\(e = {\color{red} \,\textbf{\textsf{[}}\,} e_{1} + e_{2} {\color{blue} \,\textbf{\textsf{]}}\,}\) のとき、構造的帰納法の仮定である等式 \(\text{(7.21)}\) が成り立つので、全ての \(f \in \text{Aexp},\ n \in \mathbb{Z}\) で次の等式が成り成立する:

\[ \operatorname{eval}(\operatorname{subst}(f, e_{i}), n) = \operatorname{eval}(e_{i}, \operatorname{eval}(f, n)) \tag{7.22}\]

ここで \(i = 1, 2\) である。この上で次を示せばよい:

\[ \operatorname{eval}(\operatorname{subst}(f, {\color{red} \,\textbf{\textsf{[}}\,} e_{1} + e_{2} {\color{blue} \,\textbf{\textsf{]}}\,}), n) = \operatorname{eval}({\color{red} \,\textbf{\textsf{[}}\,} e_{1} + e_{2} {\color{blue} \,\textbf{\textsf{]}}\,}, \operatorname{eval}(f, n)) \tag{7.23}\]

和に対する置換関数の定義 \(\text{(7.16)}\) より、等式 \(\text{(7.23)}\) の左辺は次に等しい:

\[ \operatorname{eval}({\color{red} \,\textbf{\textsf{[}}\,} \operatorname{subst}(f, e_{1}) + \operatorname{subst}(f, e_{2}) {\color{blue} \,\textbf{\textsf{]}}\,}, n) \]

和に対する評価関数の定義 \(\text{(7.11)}\) より、この値は次に等しい:

\[ \operatorname{eval}(\operatorname{subst}(f, e_{1}), n) + \operatorname{eval}(\operatorname{subst}(f, e_{2}), n) \]

帰納法の仮定 \(\text{(7.22)}\) より、これは次のように変形できる

\[ \operatorname{eval}(e_{1}, \operatorname{eval}(f, n)) + \operatorname{eval}(e_{2}, \operatorname{eval}(f, n)) \]

最後に、和に対する評価関数の定義 \(\text{(7.11)}\) より、これは等式 \(\text{(7.23)}\) の右辺に等しい。よって、このケースで等式 \(\text{(7.23)}\) が示せた。
\(e = {\color{red} \,\textbf{\textsf{[}}\,} e_{1} \times e_{2} {\color{blue} \,\textbf{\textsf{]}}\,}\) のときも同様に示せる。
\(e = - {\color{red} \,\textbf{\textsf{[}}\,} e_{1} {\color{blue} \,\textbf{\textsf{]}}\,}\) のときはさらに簡単に示せる。

以上で構築ケースを全てカバーできたので、構造的帰納法による証明が完了した。 ■

これは帰納法を適用する変数を読者に伝えることの重要性が分かる例と言える ── この証明が使うのは \(n\) に関する数学的帰納法ではない。 ↩︎