アンダースタンディング コンピュテーション ―単純な機械から不可能なプログラムまで

2.3

 操作的意味論

41

す。

スモールステップ操作的意味論を使って、式の意味をもっと単純なラムダ計算（lambda calculus）

と呼ばれるプログラミング言語で記述する例については、「6.2.2　意味論」を参照してください。

2.3.2

　ビッグステップ意味論

これでスモールステップ操作的意味論がどんなものかがわかりました。実行状態を管理する抽象機

械を設計し、プログラム構成要素をインクリメンタルに評価する方法について記述した簡約規則を定

義し、プログラムが完全に評価されるまで簡約を繰り返しました。スモールステップ意味論には反復

（iterative）という特徴があり、簡約規則を繰り返し実行する（

Machine#run

におけるRubyの

while

ループ）ための抽象機械が必要になります。簡約規則そのものは、必要な情報を入力として受け取り、

同種の情報を出力として生成するよう構成されます。そのため、こうした繰り返しのある応用に向いて

います

†

。

スモールステップ意味論には、プログラム全体の実行という複雑な仕事を説明や解析のしやすい小

さなパーツに切り分けるという利点がありますが、やや間接的であるように感じます。これはプログラ

ム全体がどのように動くのかを説明しているのではなく、どのように少しずつ簡約できるかを示してい

るだけです。文がどのように動くのか、完結した話としてもっと直接的に説明できないのでしょうか。

はい、それも可能です。それがビッグステップ意味論（big-step semantics）の基