操作的意味論におけるスモールステップ意味論とビックステップ意味論の違い

More than 1 year has passed since last update.

『アンダースタンディング コンピュテーション』 より、自分用メモ。

プログラミングの意味論の全体像は以下の通り。この記事は、「操作的意味論」がスコープ。

意味論

`--- 操作的意味論
            `--- スモールステップ意味論
            `--- ビッグステップ意味論

`--- 表示的意味論


「操作的意味論(operational semantics)」 とは、


  • プログラムが抽象機械の上でどのように実行されるのか、その規則を定義することで、プログラミング言語の「意味」を記述する方法

  • つまり、プログラムの意味を「プログラムが何をするのか」「プログラムを実行するとなにが起こるのか」「構成要素はどのように振る舞うのか」といった操作とその結果を通してプログラムの意味を模索する方法論

である。操作的意味論には


  1. スモールステップ意味論

  2. ビックステップ意味論

に大別できる。

スモールステップ意味論 の特徴は、


  • 構文を小さなステップで繰り返し簡約(reduce)していく

  • ステップを経てこれ以上簡約できないとき、値(value)となる

  • プログラムを実行する抽象機械には、このステップを実行する反復(iterative)機能が必要

ビッグステップ意味論 の特徴は、


  • 式や文から完結した結果を直接的に得る

  • 結果を返すだけで、どのように計算がされたのか、どの実行順序なのかについての直接的証拠は残さない

  • プログラムを実行する抽象機械には、大きな式を評価するために小さな部分式を全て評価し、それらを組み合わせる再帰(recursive)機能が必要

Type
スモールステップ
ビックステップ

抽象機械の実行方法  
reduce
recursive

抽象機械に求められる機能
iterative
evaluate

式の評価
中間式を用いながら、式を別の式に簡約
文と初期の環境を最終的な環境に買える

コールスタック
多用しない(中間式がプログラムの状態・環境を、次の評価に順々に受け渡していくから)
多用する(一連の再帰呼び出しを最終的な評価までスタックで記録しているため)