はじめに
これはRetailAI Adventurers Advent Calendar 2023の3日目の記事です．
昨日は@mizoguchi_ryosukeさんの記事「初めてのpython cvxpy」でした
最近，社内の読書会で「プログラミング言語の形式的意味論」という本を読み進めています．まだまだ勉強中ではありますが，得られた知見をまとめていきます．
本稿の中では，取り扱う主題の性質上，数式を使わせていただきます．また，あまり聞き慣れない用語も出てくるかと思いますのでご留意ください．
早速本題へ
「一言で説明してください！」と言われても適切な言葉が出てこないので，早速本書の冒頭の一文を引用します．
プログラミング言語に形式的な意味論を与えるとは，数学的なモデルを与えることである．これによって，プログラムの挙動に関する理解や推論の基礎づけが可能となる．
「プログラミング言語を数学的に扱おう」ということです．この数学的なモデルというのがまた引っかかるところですが，単に意味を与えると言っても様々な与え方があり，それをざっくりと表しているくらいで捉えてください．この意味の与え方から，操作的意味論，表示的意味論，公理的意味論の大きく3つの分野に分けられます．本稿では操作的意味論についてどういったものかをできるだけ簡単に説明します．操作的意味論では，プログラムの動作を数学的モデルで表します．
扱う対象を考える
まず，「そのモデルの中で取り扱う対象は何か？」ということを考える必要があります．整数を扱う問題を解くとすると，当然整数が必要になります．$\cdots -3,-2,-1,0,1,2,3,\cdots$のように，正の数，負の数，0ですね．ただ，これらをいちいち羅列するのは面倒なので，集合$\mathbf{N}$としてまとめておきます．また，この後の議論で集合$\mathbf{N}$の要素を表すときに$m$，$n$の文字を使うことがあります．
次に，整数に対する算術式$m*n$も考えます．ひとまず四則演算$+, -, \times, \div$を見てみます．2つの整数$m$，$n$に対して，$m + n$，$m - n$，$m \times n$の結果はいずれも整数になりますが，$m \div n$は（1つの数で表すなら）必ずしも整数になるとは限りません．よって，$+, -, \times$を扱います．これらを集合$\mathbf{Aexp}$としてまとめておきます．
上と同じように，真偽値の集合$\mathbf{T}$，プログラム変数の集合$\mathbf{Loc}$，ブール式の集合$\mathbf{Bexp}$，コマンドの集合$\mathbf{Com}$というようにまとめておきます．大事なのは，扱う対象を閉じた集合として定義することです．
状態を定義する
状態とはなんですか？？ 引用します．
状態とはプログラム変数から整数への関数$\sigma: \mathbf{Loc} \to \mathbf{N}$のことである．すなわち，$\sigma \left(X\right)$は状態$\sigma$のもとでの変数$X$の値を返す．
例えばあるプログラムを書いて，変数$X$に5を代入したとします．このような状態を$\sigma$とすると
$$
\left< X, \sigma\right> \to \sigma \left(X\right) \to 5
$$
というように，5が返されます．直観的には，至極当たり前のことだと思いますが，厳密なモデル構築のために必要な定義です．任意の算術式は状態$\sigma$によって値を返され，このことを評価といいます．
状態を定義しても，変数$X$が常に5を返すように，ずっと同じ状態を維持していたのでは面白くないですね．何かしら状態が変化しないといつまでも問題は解けません．上でさらっと出しましたが，コマンドがその役割を担います．上の例で，「変数$X$に5を代入した」と書きましたが，最初から5が入っているわけではありません．
$$
X:=5
$$
という操作を行う必要があります．先程，$\left< , \sigma \right>$の記法を出しましたが，初期状態（定義済みのすべてのプログラム変数の値が0の状態）を$\sigma_{0}$として
$$
\left< X:=5, \sigma_{0} \right> \to \sigma
$$
というように状態が$\sigma$に遷移します．コマンド$c \in \mathbf{Com}$の実行によって状態が遷移していきます．
前提から結論を導出する
これも直観的に至極当たり前の話だと思いますが，前提があって結論が導かれます．プログラム中で，$3+5$という演算をするときに，任意の状態$\sigma$において，$\left<3,\sigma\right> \to 3$，$\left<5,\sigma\right> \to 5$という前提が成立するから，$\left<3+5,\sigma\right> \to 8$という結論が導かれます．$\left<3,\sigma\right> \to 4$となるプログラムでは上記の結論は導かれません．書籍の記法を使って，
$$
\frac{\left<3, \sigma \right> \to 3 \qquad \left<5, \sigma \right> \to 5}{\left<3+5,\sigma\right> \to 8}
$$
と書きます．前提0で得られる結論を公理といい，プログラム中では当たり前に成り立つもの（$\left<3, \sigma \right> \to 3$など）を指します．
$$
\frac{}{\left<3, \sigma \right> \to 3}
$$
公理からスタートし，前提から結論を導き，導いた結論を前提に次の結論を導くというプロセスで解くべき問題を導出してやります．これを導出木といいます．
閑話休題
導出木を書くための良いツールを探していたのですが，見つけられませんでした．．．
まとめ
本記事では，形式的意味論のなかの操作的意味論についてざっくり説明しました．具体的な問題の例示もなく，話がかなり抽象的になってしまいました．また，かなり端折って書いたことで，情報の欠損が多々あるかと思いますので，コメントで忌憚なきご意見をお聞かせ願います．今後別の記事で，さらに詳しく説明していきたいと思います．
明日は引き続き，@yoshitake_tatsuhiroが別の内容で担当します．