ここまで見てきた評価器(例えばaexpのもの、bexpのもの、コマンドのもの) はビッグステップスタイルで記述されてきました。 つまり、与えられた式がどのように最終的な値になるか (またはコマンドと記憶状態(store)の組がどのように最終記憶状態になるか)を特定していました。 「すべてが1つの大きなステップ」で行われました。

このスタイルは単純で多くの目的のために自然な方法です(実際、Gilles Kahn は、 この使用を広めた人ですが、彼はこれを自然意味論(natural semantics)と呼びました)。 しかし、これではうまくいかないときもあります。 特に、この方法は、並列プログラミング言語について話す自然な方法を提供してくれません。 並列プログラミング言語の場合、プログラムの「意味」、つまり プログラムがどのように振る舞うかの本質は、 入力状態が出力状態にどのように写像されるかだけではなく、途中で通過する状態も含みます。 なぜなら、中間状態は並列実行されるコードからも観測されるからです。

ビッグステップスタイルのもう1つの欠点は、より技術的なことですが、 ある種のアプリケーションには致命的です。 ImpList_J.v で導入した、リストを持つImpの変種を考えましょう。 0 + nilのようなプログラムの意味を、数値が期待されるコンテキストでリストが現れたときには、 それを0と解釈するものとして定義する方法をとりました。しかしこれはその場限りのものでした。 単純に、 そのようなプログラムの振る舞いは「未定義」(undefined)と言ってしまった方がよかったでしょう。 つまりどのような結果にも評価されないということです。 そうすることは簡単にできるでしょう。 aevalとbevalの定義方法として(Fixpoint ではなく)帰納的命題を使うだけです。 すると、全関数(total function)ではなく部分関数(partial function)にすることができます。

しかしながら、この方法で Imp を定義することには深刻な欠陥があります。 この言語には、コマンドが初期状態を終了状態に写像するのに失敗するまったく異なる2種類の理由があります。 1つは評価が無限ループに陥ることによるもの、もう1つは、どこかの地点でプログラムが、 ブール値の次の値をとるなどの意味のない操作をしようとして、 どの評価規則も適用できなくなることによるものです。

この2つの結果、つまり「停止しないこと」と「間違った設定によって行き詰まること」は、まったく別物です。 特に、1つ目は許容し(無限ループの可能性を許すことは、 プログラミングに while のような一般的ループ構造を使う便利さの代償です)、 2つ目(これはただの間違いです)は禁じたいのです。 これは例えば言語に何らかの「型チェック」(typechecking)を追加することで実現できます。 実のところ、これはこのコースの残りの部分の主要なトピックです。 最初のステップとして、停止しないことと、 間違いによる「行き詰まり状態」を区別することができる別の意味提示方法が必要です。

このように、いろいろな理由で、 プログラムの振る舞いを定義し推論するよりきめの細かい方法が欲しいのです。 これがこの章のトピックです。 与えられたプログラムに対して計算の「アトミックなステップ」 がどのように行なわれるかを定める「スモールステップ」の関係によって、 「ビッグステップ」のeval関係を置き換えます。

おもちゃの言語

無駄な議論を省くため、定数と足し算だけの極端に単純な言語に戻りましょう。 この章の終わりには、同じテクニックをImp言語全体に適用する方法がわかるでしょう。

次がこの言語の標準的な評価器です。 ここまでやってきたのと同じ(ビッグステップの)スタイルで記述されています。

次は同じ評価器を、まったく同じスタイルながら、帰納的に定義された関係によって定式化したものです。 再び、「tがnに評価される」を記法 t ⇓ n で表しています。

                                ------ (E_Const)
                                n ⇓ n

                               t1 ⇓ n1
                               t2 ⇓ n2
                        --------------------- (E_Plus)
                        t1 + t2 ⇓ plus n1 n2

2つ目の規則で n1 + n2 ではなく plus n1 n2 と書いています。 これは、⇓ の左側にある+が抽象構文木のノードであるのに対し、 ⇓ の右側の加算は数値 n1 と n2 の数学的な和であることを強調するためです。 形式的なCoqのバージョンではこの区別についてより堅苦しくなっています。

次はわずかに変わっています。まだビッグステップスタイルですが、 項の最終結果が数値そのものではなく、また項になっています。

(非形式的な規則では、定数「項」nとそのままの「数値」nの区別を省いているので、 何も変わらないことに注意します。)

そして、次がスモールステップ版です。

                        ---------------------- (ST_PlusConstConst)
                        n1 + n2 ⇒ plus n1 n2

                              t1 ⇓ t1'
                         ------------------- (ST_Plus1)
                         t1 + t2 ⇓ t1' + t2

                              t2 ⇓ t2'
                         ------------------- (ST_Plus2)
                         n1 + t2 ⇓ n1 + t2'

なお、ここでは記法を簡単にするため変数名を使っています。慣習として、n1とn2は定数 (tm_constで構成されるもの)のみを指します。一方t1とt2は任意の項を指します。 形式的規則では明示的なコンストラクタを使ってこの区別をします。

注目すること:

• 定義しているのは簡約のちょうど1ステップです。 そこでは1つのtm_plusノードがその値に置き換えられます。
  
  
• 各ステップでは「最左」の準備ができている(つまり、引数が両方とも定数である) tm_plusノードを探して、それをその場で書き換えます。 最初の規則はtm_plusノードをどのように書き換えるかを定めます。 残りの2つの規則は、それをどう探すかを定めます。
  
  
• 定数の項は、ステップを進めません。

step関係を使った推論の例を2つ...

もしt1が1ステップでt1'になるならば、 tm_plus t1 t2 は1ステップで plus t1' t2 になります:

練習問題: ★★ (test_step_2)

和の右側がステップを進むことができるのは、左側が終了したときだけです: もしt2が1ステップでt2'になるならば、 tm_plus (tm_const n) t2 は1ステップで tm_plus (tm_const n) t2' になります。(次の証明を完成させなさい):

☐

関係 ⇒ のおもしろい性質の1つは、 Imp プログラムの言語の評価関係と同様、決定性を持つ(deterministic)ということです。

「定理」: 各tに対して、tが1ステップでt'になる(t ⇒ t' が証明可能な) t'は高々1つである。 形式的には、これは、⇒が部分関数であるというのと同じです。

「証明スケッチ」:xが1ステップでy1とy2のどちらにもなるとき、y1とy2 が等しいことを、step x y1 の導出についての帰納法で示す。 この導出と step x y2 の導出のそれぞれで使われた最後の規則によって、 いくつかの場合がある。

• もし両者とも ST_PlusConstConst ならば、一致は明らかである。
  
  
• 導出が両者とも ST_Plus1 または ST_Plus2 で終わるならば、 帰納法の仮定から成立する。
  
  
• 一方が ST_PlusConstConst で、他方が ST_Plus1 または ST_Plus2 であることはあり得ない。なぜなら、そうなるためには、 x が tm_plus t1 t2 の形で(ST_PlusConstConstより) t1とt2が両者とも定数であり、かつt1またはt2が tm_plus ... の形でなければならない。
  
  
• 同様に、一方が ST_Plus1 で他方が ST_Plus2 であることもあり得ない。 なぜなら、そのためには、x は tm_plus t1 t2 の形で、 t1 が tm_plus t1 t2 の形でも tm_const n の形でもなければならないからである。☐

値

定義した1ステップ簡約の定義をちょっとだけ一般化するために少し時間をとりましょう。

関係 ⇒ を抽象機械(abstract machine)の定義と考えるのは便利です:

• どの時点でも、機械の状態(state)は項です。
  
  
• 機械のステップ(step)は、計算のアトミックな単位です。ここでは、1つの加算処理です。
  
  
• 機械の停止状態(halting states)は、さらなる計算が存在しない状態です。

このとき、項tは以下のように評価できます:

• tを機械の開始状態としてとります。
  
  
• 次のような機械の状態の列を見つけるために、⇒ 関係を繰り返し使います。 見つけるのは、tから始まり、それぞれの状態から1ステップでその次の状態になる列です。
  
  
• もう簡約ができなくなったとき、機械の最終状態を、実行結果として「読み出し」ます。

直観的には、機械の最終状態が常に、 あるnについての tm_const n という形の項になることは明らかです。 そのような項を「値」(values)と呼びます。

値の概念を導入したので、これを ⇒ 関係の定義に使うことで、 ST_Plus2 規則をもう少しだけ直観的なものにできます:

                        ---------------------- (ST_PlusConstConst)
                        n1 + n2 ⇒ plus n1 n2

                              t1 ⇓ t1'
                         ------------------- (ST_Plus1)
                         t1 + t2 ⇓ t1' + t2

                              t2 ⇓ t2'
                         ------------------- (ST_Plus2)
                         v1 + t2 ⇓ v1 + t2'

再び、変数名が重要な情報を担っています: 慣習として、v1は値のみを変域とし、一方t1とt2は任意の項を変域とします。 規則のCoqバージョンでは、同じ目的のために明示的なvalue仮定を使います。

練習問題: ★★★, recommended (redo_determinacy)

この変更のサニティチェックのため、決定性を再検証しましょう。

証明スケッチ: もしxが1ステップでy1にもy2にも進むならば、 y1とy2が等しいことを示さなければならない。 step x y1 と step x y2 の導出の最後の規則を考える。

• もし両者ともST_PlusConstConstならば、一致は明らかである。
  
  
• 一方が ST_PlusConstConst で、他方が ST_Plus1 または ST_Plus2 であることはあり得ない。なぜなら、そうなるためには、 x が tm_plus t1 t2 の形で(ST_PlusConstConstより) t1とt2が両者とも定数であり、かつt1またはt2が tm_plus ... の形でなければならない。
  
  
• 同様に、一方が ST_Plus1 で他方が ST_Plus2 であることもあり得ない。 なぜなら、そのためには、x が tm_plus t1 t2 の形で、 t1 は tm_plus t1 t2 の形であり、かつ( tm_const n の形であるから) 値でもなければならないからである。
  
  
• 導出が両者とも ST_Plus1 または ST_Plus2 で終わるならば、 帰納法の仮定から成立する。☐

証明のほとんどは前のものと同じです。しかし、練習問題の効果を最大にするために、 ゼロから証明を書き、前のものを見るのは行き詰まった時だけにしなさい。

☐

強進行と正規形

おもちゃの言語に対する1ステップの簡約の定義はかなり単純です。 しかし、より大きな言語に対しては、何か規則を忘れてしまうことは簡単に起き、 項が完全に値に簡約されていないのにステップを進めなくなってしまうことが発生します。 次の定理は、このような間違いをしていないことを示します。

「定理(強進行)」(Strong Progress):すべての t:tm について tは値であるか、ある項t'があって t ⇒ t' となる。

「証明」: tについての帰納法で証明する。

• t = tm_const n とする。すると、t は value(値)である。
  
  
• t = tm_plus t1 t2 と仮定する。ここで(帰納仮定から) t1は値であるか、1ステップであるt1'になり、また、t2は値であるか、 1ステップであるt2'になる。 ここで必要なのは、tm_plus t1 t2が値であるか、 あるt'に1ステップで進むということを示すことである。
  
  
  • もしt1とt2がともに値なら、ST_PlusConstConstにより tはステップを進むことができる。
    
    
  • もしt1が値でt2がステップを進むことができるならば、ST_Plus2により tもステップを進むことができる。
    
    
  • もしt1がステップを進むことができるならば、ST_Plus1により tもステップを進むことができる。 ☐

この重要な性質は「強進行」(strong progress)と呼ばれます。 これは、すべての項が値であるか、別の項に「進行できる」("make progress") ことからきた名称です。「強」("strong")という修飾句は、 後の章のより細分されたバージョン(単に「進行」("progress")と呼ばれる) と区別するためのものです。

「進行する」という概念の拡張から、value(値)についての興味深い性質がわかります: 値とはこの意味で進行「できない」項のことに他なりません。 この事実を述べるために、進行できない項に名前をつけましょう。そういう項を「正規形」 (normal form)と呼びます。

この定義は実際には、任意の集合Xの上の「任意の」関係Rについて、 何が正規形であるかを定めています。 今興味対象としている、項の上の特定の1ステップ簡約関係に限るものではありません。 このコースで後に、別の関係の議論において同じ用語法を用います。

強進行定理の洞察を一般化するためにこの用語を使います。 この言語では、正規形と値とは実質的に同じものです。

なぜこれが興味深いのでしょう？ 2つの理由があります:

• なぜならvalue(値)は構文的概念です。つまり項の形を見ることで定義されます。 一方normal_form(正規形)は意味論的なものです。 つまり項がどのようにステップを進むかによって定義されます。 この2つの概念が一致することは自明ではないのです!
  
  
• 実際、正規形と値の概念が一致「しない」言語はたくさん存在します。

これがどうして起こるのか調べてみましょう...

例えば、value(値)の定義を間違えていて、 簡約が完了していない項を含んでいるかもしれません。

練習問題: ★★★, recommended (value_not_same_as_normal_form)

☐

あるいは、stepの定義を間違えていて、 値とされたものをさらに簡約するようになっているかもしれません。

練習問題: ★★★, recommended (value_not_same_as_normal_form)

☐

最後に、valueとstepの定義を間違えていて、ある項について、値でもなく、 step関係で1ステップ進むこともできなくなっているかもしれません。 そのような項は「行き詰まり」(stuck)と呼ぶべきでしょう。

(ST_Plus2 がないことに注意します。)

練習問題: ★★★ (value_not_same_as_normal_form')

☐

練習問題

以下は、別の非常に簡単な言語です。項は、加算と数値の代わりに、 真理値 true と false、および条件式です...

練習問題: ★ (smallstep_bools)

以下の命題のうち証明できるものはどれでしょう？ (これは単に頭の体操です。 しかしさらなるチャレンジとしてCoqで自分の答えを自由に証明してみなさい。)

☐

練習問題: ★★★, recommended (progress_bool)

加算式についてと同様に、ブール式についても進行定理が証明できます。 (やってみなさい。)

☐

練習問題: ★★, optional (step_deterministic)

☐

練習問題: ★★ (smallstep_bool_shortcut)

条件式のthenとelseの枝が同じ値のとき(ともにtm_trueであるか、 ともにtm_falseであるかのとき)、ガードが値に簡約されていなくても、 条件式全体を枝の値に簡約するように、ステップ関係にバイパスを追加したいとします。 例えば次の命題を証明できるようにしたいとします:
         tm_if
            (tm_if tm_true tm_true tm_true)
            tm_false
            tm_false
     ⇒
         tm_false.

ステップ関係にこのための追加の節を記述し、bool_step_prop4を証明しなさい。

☐

☐

練習問題: ★★★ (properties_of_altered_step)

講義ノートのステップ関係についての決定性定理と強進行定理が、 上記のステップの定義についても証明できます。 ST_ShortCircuit節を追加した後で...

• step関係はそれでも決定性を持つでしょうか？ yes または no と書き、簡潔に(1文で)その答えを説明しなさい。
  
  Optional: Coq でその答えが正しいことを証明しなさい。

• 強進行定理は成立するでしょうか？ yes または no と書き、簡潔に(1文で)その答えを説明しなさい。
  
  Optional: Coq でその答えが正しいことを証明しなさい。

• 一般に、オリジナルのステップ関係から1つ以上のコンストラクタを取り除いて、 強進行性を持たなくする方法はあるでしょうか？ yes または no と書き、簡潔に(1文で)その答えを説明しなさい。

☐

マルチステップ簡約

ここまでは、1ステップ簡約関係 ⇒ に取り組んできました。 これは、プログラムを実行する抽象機械の1つのステップを形式化したものです。

この機械を使って、プログラムを完全に簡約してみるのもおもしろいでしょう。 つまり、その最後の結果がどうなるかを調べることです。 これは以下のように形式化できます:

• 最初に、「マルチステップ簡約関係」(multi-step reduction relation) ⇒* を定義します。 この関係は、tから1ステップ簡約を何らかの回数回行うことでt'に到達できるとき、 tとt'を関係づけるものです。
  
  
• 次に項tの結果("result")を、 tがマルチステップ簡約で到達できる正規形tとして定義します。

マルチステップ簡約

マルチステップ簡約(multi-step reduction)関係 ⇒* は1ステップ関係 ⇒の反射推移閉包です。

例えば...

以下は別証です。 eapplyを使うことで、すべての中間的な項を明示的に構成する必要をなくしたものです。

練習問題: ★ (test_stepmany_2)

☐

練習問題: ★ (test_stepmany_3)

☐

練習問題: ★★ (test_stepmany_4)

☐

正規形再び

tが0以上のステップでt'に簡約され、t'が正規形のとき、 「t'はtの正規形である」と言います。

1ステップ簡約が決定性を持つことを既に見ました。 つまり、項が1ステップ進む方法は高々1種類だということです。 このことから、tが正規形に到達するならば、その正規形は1つに決まることになります。 つまり、normal_form_of は部分関数です。言い換えると、 normal_form t t' を、 (「t'はtの正規形である」と読む以外に) 「tの正規形はt'である」と読んでよいということです。 (訳注：原文では "the normal form of t" と定冠詞を使ってよいことと記述されています。)

練習問題: ★★★, optional (test_stepmany_3)

☐

実のところ、この言語については、より強いことが成立します (これは他のすべての言語で成立することではありません): 「任意の」項tはいつかは正規形に到達する、ということです。 つまり normal_form_of は全関数です。 形式的には、step関係は正規化性を持つ(normalizing)と言います。

stepが正規化性を持つことを証明するため、二つの補題を必要とします。

一つは、tがt'に何ステップかで簡約されるならば、 tが tm_plus ノードの左側の子ノードとして現れるときには、 t内で同じ簡約ステップ列が可能である、ということ、 そしてまた同様のことが、 tが(左側の子ノードが値である)tm_plus の右側の子ノードとして現れるときにも言える、ということです。

練習問題: ★★

☐

「定理」: step 関数は正規化性を持つ。つまり、 任意のtに対して、あるt'があって、tからステップを進めるとt'に到達し、 かつt'は正規形である、が成立する。

「証明スケッチ」:項についての帰納法を使う。考える対象は2つの場合である:

• あるnについて t = tm_const n である場合。 このとき、tはステップを進めることができないことから、 t' = t である。左辺は反射性から導出され、 右辺は、(a)(nf_same_as_valueより)値は正規形であること、 (b)(v_constより)tは値であること、から導出される。
  
  
• あるt1、t2について、t = tm_plus t1 t2 である場合。 帰納仮定よりt1とt2はそれぞれ正規形t1'とt2'を持つ。 (nf_same_as_valueより)正規形は値であったから、 ある n1、n2について、t1' = tm_const n1 かつ t2' = tm_const n2 である。t1とt2についての ⇒* 導出を組合せると、 tm_plus t1 t2 が幾つかのステップで tm_const (plus n1 n2) に簡約されることを証明できる。
  
  t' = tm_const (plus n1 n2) が値であることは明らかなので、これは正規形である。

ビッグステップ簡約とスモールステップ簡約の同値性

小さなプログラミング言語に対して2つの異なったスタイルで操作的意味論を定義したので、 その2つの定義が本当に同じものを定義しているのかを考えるのは意味があります! 実際に定義は一致しているのですが、それを示すことはそれほど簡単にはできません。 というより、それを正確に主張することが難しいのです。 なぜなら、一方は1回で進むのが小さなステップだけですが、 もう一方は大きなまとまりで進むからです。

練習問題: ★★★ (eval__stepmany)

この証明のために合同とrscのいくつかの性質を使うのが良いでしょう。

☐

練習問題: ★★★ (eval__stepmany_inf)

eval__stepmany の証明の非形式版を記述しなさい。

☐

練習問題: ★★★ (step__eval)

☐

全部まとめることで、vがtの正規形であるのは、tがvに評価されるのと同値である、 とはっきりと言うことができます。

さらなる練習問題

練習問題: ★★★★ (combined_properties)

ここまでに算術式と条件式を別々に考えてきました。 この練習問題ではこの2つがどのように相互作用するかを調べます。

前には、plus式とif式について、以下のことを別々に証明しました...

• ステップ関係が部分関数であること(つまり、決定性を持つこと)。
  
  
• すべての項が値であるか、1ステップ進むことができるかを主張する強進行補題。

結合した言語について、これらの性質を証明、または反証しなさい。

☐

スモールステップ Imp

より本気の例として、Impの操作的意味論のスモールステップ版を示します。 定義はより大きくなりますが、基本的な考え方は上述のものとまったく同じです。

実際にはブール値の定義にかかずらってはいなかったことに注意します。 ⇒b の定義にはブール値の定義は必要ありません(なぜでしょう？)。 言語がちょっと大きかったら必要になったかもしれませんが。

コマンドの意味論は興味深い部分です。 うまくやるために2つの小さなトリックを使います:

• SKIP を「コマンド値」("command value")として使います。 つまり、正規形に逹したコマンドです。
  
  
  • 代入コマンドはSKIPに簡約されます(その際に状態を更新します)。
    
    
  • コマンド合成は、左側の部分コマンドがSKIPに簡約されるのを待って、 それを捨ててしまいます。そして続けて右側の部分コマンドの簡約をします。
    
    
• WHILEコマンドの簡約は、条件文とそれに続く同じWHILEコマンドになります。
  
  (求められる効果を得るために他にもいろいろな方法はありますが、 いずれも、 もとのWHILEコマンドをどこかに保存して、 ループ本体の1コピーを評価することには変わりありません。)

並列実行 Imp

最後に、この定義スタイルの力を示すために、Imp に平行動作のコマンドを拡張しましょう。 このコマンドは2つのサブコマンドを平行実行し、両者が終了した時点で終了します。 スケジューリングの予測不能性を反映して、 サブコマンドのアクションは任意の順序でインターリーブします。 しかし、同じメモリをシェアし、同じ変数を読み書きすることでコミュニケーションできます。

この言語のいろいろな興味深い性質の中でも格別なものは、次のプログラムが、 変数Xにどのような値を入れても停止するという事実です...

特に、Xを0にしても停止できます:

Xを2にしても停止します:

より一般に...

練習問題: ★★★, optional

練習問題: ★★★, optional

... 上のループはXがどんな値をとっても抜け出せます。