ここまで見てきた評価器（例えばaexp用、bexp用、コマンド用、などなど）は「ビッグステップスタイル」で記述されてきました。 つまり、与えられた式がどのように最終的な値になるか（またはコマンドと記憶状態の組がどのように最終記憶状態になるか）を「すべて大きな1ステップ」として決定しました。 このスタイルは単純で多くの目的のために自然な方法です。 実際、この手法を広めた Gilles Kahn は、これを「自然意味論(natural semantics)」と呼びました。 しかし、これではうまくいかないときもあります。 特に、この方法は、並列プログラミング言語について言及する際には自然ではありません。 並列プログラミング言語の場合、プログラムの「意味」、つまりプログラムがどのように振る舞うかの本質は、入力状態が出力状態にどのように写像されるかだけではなく、途中で通過する状態も含みます。 なぜなら、中間状態は並列実行される他のコードからも観測されるからです。 ビッグステップスタイルのもう1つの欠点は、より技術的なことですが、ある種のアプリケーションには致命的です。 変数が数値だけでなく数値のリストにも束縛されうるImpの変種を考えましょう。 構文的には、この言語では2 + nilのような変な式を書くことができます。 そして、意味論上では、この式がどのように動くのかについて言及する必要があります。 一つの動き方としては、リストを適当な数値として扱うことで、全ての算術式を数値に評価するものがあります。 例えば数値を期待する箇所ではリストを常に0として扱う、といった扱い方があります。 ただ、この方法は少し奇抜な方法です。 より自然な方法としては、2+nilのような式の動き方を「未定義(undefined)」としてしまうことです。 つまりどのような結果にも評価されないということです。 これは簡単に実現できます。 aevalとbevalを、Fixpoint ではなく帰納的(Inductive)命題として定義するだけです。 すると、全関数ではなく部分関数にすることができます。 しかしながら、この方法で Imp を定義することには深刻な欠陥があります。 この言語では、コマンドが初期状態を終了状態に写像するのに失敗した際に、「まったく異なる」2種類の原因があり得ます。 1つは評価が無限ループに陥ることによるもの、もう1つは、どこかの地点でプログラムが、数値をリストに加えるなどの意味のない操作をしようとして、どの評価規則も適用できなくなることによるものです。 この2つの結果、つまり「停止しないこと」と「間違った設定によって行き詰まること」をごちゃ混ぜにしないでください。 特に、1つ目は「許容」したい（無限ループの可能性を許すことは、プログラミングに while のような一般的ループ構造を使う便利さの代償です）一方で、2つ目（これはただの間違いです）は「禁止」したいのです。 これは例えば言語に何らかの「型チェック(typechecking)」を追加することで実現できます。 実のところ、これはこのコースの残りの部分の主要なトピックです。 まずは、停止しないことと、間違いによる「行き詰まり状態」を区別することができる別の意味提示方法が必要です。 このように、いろいろな理由で、プログラムの振る舞いを定義し推論するよりきめの細かい方法が欲しいことが度々あります。 これがこの章のトピックです。 目標は、与えられたプログラムに対して計算の「アトミックなステップ」がどのように行われるかを定める「スモールステップ」の関係によって、「ビッグステップ」のeval関係を置き換えることです。

おもちゃの言語

無駄な議論を省くため、定数と足し算だけの極端に単純な言語に戻りましょう。 （可読性のために、定数と足し算を表すコンストラクタにCとPという一文字の名前を用います。） この章の終わりには、同じテクニックをImp言語全体に適用する方法がわかるでしょう。

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

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

                               ---------                               (E_Const) 
                               C n ==> n 
 
                               t1 ==> n1 
                               t2 ==> n2 
                           -------------------                         (E_Plus) 
                           P t1 t2 ==> n1 + n2 

そして、次が対応する「スモールステップ」版です。

                     -------------------------------        (ST_PlusConstConst) 
                     P (C n1) (C n2) --> C (n1 + n2) 
 
                              t1 --> t1' 
                         --------------------                        (ST_Plus1) 
                         P t1 t2 --> P t1' t2 
 
                              t2 --> t2' 
                      ----------------------------                   (ST_Plus2) 
                      P (C n1) t2 --> P (C n1) t2' 

注目すること:

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

Let's pause and check a couple of examples of reasoning with the step relation...

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

練習問題: ★, standard (test_step_2)

和の右側のステップを進められるのは、左側が終了したときだけです： もしt2が1ステップでt2'になるならば、 P (C n) t2 は1ステップで P (C n) t2' になります。 以上を踏まえて次の証明を完成させなさい：

☐

Relations

We will be working with several different single-step relations, so it is helpful to generalize a bit and state a few definitions and theorems about relations in general. (The optional chapter Rel.v develops some of these ideas in a bit more detail; it may be useful if the treatment here is too dense.) A binary relation on a set X is a family of propositions parameterized by two elements of X -- i.e., a proposition about pairs of elements of X.

Our main examples of such relations in this chapter will be the single-step reduction relation, -->, and its multi-step variant, -->* (defined below), but there are many other examples -- e.g., the "equals," "less than," "less than or equal to," and "is the square of" relations on numbers, and the "prefix of" relation on lists and strings.

関係 --> の性質の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 が P t1 t2 の形で（ST_PlusConstConstより）t1とt2が両者とも定数であり、「かつ」t1またはt2が P _ の形でなければならないためである。
• 同様に、一方が ST_Plus1 で他方が ST_Plus2 であることもあり得ない。 なぜなら、そのためには、x は P t1 t2 の形で、 t1 が P t11 t12 の形であると同時に C n の形でもなければならないからである。 ☐

Formally:

There is some annoying repetition in this proof. Each use of inversion Hy2 results in three subcases, only one of which is relevant (the one that matches the current case in the induction on Hy1). The other two subcases need to be dismissed by finding the contradiction among the hypotheses and doing inversion on it. The following custom tactic, called solve_by_inverts, can be helpful in such cases. It will solve the goal if it can be solved by inverting some hypothesis; otherwise, it fails.

The details of how this works are not important for now, but it illustrates the power of Coq's Ltac language for programmatically defining special-purpose tactics. It looks through the current proof state for a hypothesis H (the first match) of type Prop (the second match) such that performing inversion on H (followed by a recursive invocation of the same tactic, if its argument n is greater than one) completely solves the current goal. If no such hypothesis exists, it fails. We will usually want to call solve_by_inverts with argument 1 (especially as larger arguments can lead to very slow proof checking), so we define solve_by_invert as a shorthand for this case.

Let's see how a proof of the previous theorem can be simplified using this tactic...

値

次に、1ステップ簡約を再定義して、「値」であることを明示するようにしましょう。

関係 --> が抽象機械(abstract machine)の定義と考えると便利です:

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

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

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

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

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

                     -------------------------------        (ST_PlusConstConst) 
                     P (C n1) (C n2) --> C (n1 + n2) 
 
                              t1 --> t1' 
                         --------------------                        (ST_Plus1) 
                         P t1 t2 --> P t1' t2 
 
                               value v1 
                              t2 --> t2' 
                         --------------------                        (ST_Plus2) 
                         P v1 t2 --> P v1 t2' 

再び、変数名が重要な情報を担っています: 慣習として、v1は値のみを変域とし、一方t1とt2は任意の項を変域とします。 （この慣習により、明示的にvalue仮定を用いることは冗長となります。 この時点では非形式的なルールとCoqの記述の対応をわかりやすくするために仮定を取っておきますが、後に可読性を優先して除去します。） Here are the formal rules:

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

この変更のサニティチェックのため、決定性を再検証しましょう。 非形式的には以下の証明になります。 「証明スケッチ」: もしxが1ステップでy1にもy2にも進むならば、 y1とy2が等しいことを示さなければならない。 step x y1 と step x y2 の導出の最後の規則を考える。

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

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

☐

強進行と正規形

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

「定理(強進行)」(Strong Progress): t が項であるならば、 tは値であるか、そうでなければある項t'が存在して t --> t' となる。

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

• t = C n とする。すると、t は値である。
• t = P t1 t2 と仮定する。ここで（帰納仮定から） t1は値であるか、1ステップであるt1'になり、また、t2は値であるか、 1ステップであるt2'になる。 ここで必要なのは、P 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ステップ簡約関係に限るものではありません。 このコースで後に、別の関係の議論において同じ用語法を用います。

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

なぜこれが興味深いのでしょう？ なぜならvalue(値)は構文的概念です。つまり項の形を見ることで定義されます。 一方normal_form（正規形）は意味論的なものです。 つまり項がどのようにステップを進むかによって定義されます。 この2つの概念が一致することは自明ではないのです!

実際、正規形と値の概念が一致「しない」定義を誤って書くことが簡単に起こりえます。

練習問題: ★★★, standard, optional (value_not_same_as_normal_form1)

例えば、value(値)の定義を間違えていて、簡約が完了していない項を含んでいるかもしれません。 （この課題や以下のCoqの記述を見なかったとしても、そのような項を思いつくようにしておいてください。）

☐

練習問題: ★★, standard, optional (value_not_same_as_normal_form2)

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

☐

練習問題: ★★★, standard, optional (value_not_same_as_normal_form3)

最後に、valueとstepの定義が、ある項について、値でもなく、 step関係で1ステップ進むこともできないようになっているかもしれません。 そのような項は「行き詰まった」(stuck)と言うべきでしょう。この場合の 原因は意味論の定義の誤りにありますが、正しい定義をしているが行き詰まる項が存在する、 という状況も現れます。

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

☐

さらなる練習問題

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

練習問題: ★, standard (smallstep_bools)

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

☐

練習問題: ★★★, standard, optional (progress_bool)

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

☐

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

☐

練習問題: ★★ (smallstep_bool_shortcut)

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

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

☐

練習問題: ★★★, standard, optional (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ステップ簡約を何回か（0回も含みます）行うことでt'に到達できるとき、 tとt'を関係づけるものです。
• 次に項tの結果("result")を、 tがマルチステップ簡約で到達できる正規形tとして定義します。

Since we'll want to reuse the idea of multi-step reduction many times, let's take a little extra trouble and define it generically. Given a relation R (which will be --> for present purposes), we define a relation multi R, called the multi-step closure of R as follows.

(In the Rel chapter of Logical Foundations and the Coq standard library, this relation is called clos_refl_trans_1n. We give it a shorter name here for the sake of readability.) The effect of this definition is that multi R relates two elements x and y if

• x = y, or
• R x y, or
• there is some nonempty sequence z1, z2, ..., zn such that
  R x z1 R z1 z2 ... R zn y.

Thus, if R describes a single-step of computation, then z1 ... zn is the sequence of intermediate steps of computation between x and y. We write -->* for the multi step relation on terms.

The relation multi R has several crucial properties. First, it is obviously reflexive (that is, forall x, multi R x x). In the case of the -->* (i.e., multi step) relation, the intuition is that a term can execute to itself by taking zero steps of execution. Second, it contains R -- that is, single-step executions are a particular case of multi-step executions. (It is this fact that justifies the word "closure" in the term "multi-step closure of R.")

Third, multi R is transitive.

In particular, for the multi step relation on terms, if t1 -->* t2 and t2 -->* t3, then t1 -->* t3.

Examples

Here's a specific instance of the multi step relation:

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

練習問題: ★, standard, optional (test_multistep_2)

☐

練習問題: ★, standard, optional (test_multistep_3)

☐

練習問題: ★★, standard (test_multistep_4)

☐

正規形再び

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

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

練習問題: ★★★, standard, optional (normal_forms_unique)

☐

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

stepが正規化性を持つことを証明するため、二つの補題を必要とします。 一つは、tがt'に何ステップかで簡約されるならば、 tが P ノードの左側の子ノードとして現れるときには、 t内で同じ簡約ステップ列が可能である、ということ、 そしてまた同様のことが、 tが(左側の子ノードが値である)P の右側の子ノードとして現れるときにも言える、ということです。

練習問題: ★★, standard (multistep_congr_2)

☐

これらの補題を使えば、後は単純な帰納法で証明できます。 「定理」: step 関数は正規化性を持つ。つまり、 任意のtに対して、あるt'があって、tからステップを進めるとt'に到達し、 かつt'は正規形である、が成立する。 「証明スケッチ」:項についての帰納法を使う。考える対象は2つの場合である:

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

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

小さなプログラミング言語に対して2つの異なった方法（ビッグステップとスモールステップ）で操作的意味論を定義したので、 その2つの定義が本当に同じものを定義しているのかを考えるのは意味があります! 実際に定義は一致しているのですが、それを示すにはもう少し準備が必要です。 詳細は練習問題として残しています。　

練習問題: ★★★, standard (eval__multistep)

The key ideas in the proof can be seen in the following picture: P t1 t2 --> (by ST_Plus1) P t1' t2 --> (by ST_Plus1) P t1'' t2 --> (by ST_Plus1) ... P (C n1) t2 --> (by ST_Plus2) P (C n1) t2' --> (by ST_Plus2) P (C n1) t2'' --> (by ST_Plus2) ... P (C n1) (C n2) --> (by ST_PlusConstConst) C (n1 + n2) That is, the multistep reduction of a term of the form P t1 t2 proceeds in three phases:

• First, we use ST_Plus1 some number of times to reduce t1 to a normal form, which must (by nf_same_as_value) be a term of the form C n1 for some n1.
• Next, we use ST_Plus2 some number of times to reduce t2 to a normal form, which must again be a term of the form C n2 for some n2.
• Finally, we use ST_PlusConstConst one time to reduce P (C n1) (C n2) to C (n1 + n2).

To formalize this intuition, you'll need to use the congruence lemmas from above (you might want to review them now, so that you'll be able to recognize when they are useful), plus some basic properties of -->*: that it is reflexive, transitive, and includes -->.

☐

練習問題: ★★★, advanced (eval__multistep_inf)

eval__multistep の非形式的証明を詳細に記述しなさい。

☐ For the other direction, we need one lemma, which establishes a relation between single-step reduction and big-step evaluation.

練習問題: ★★★, standard (step__eval)

☐ The fact that small-step reduction implies big-step evaluation is now straightforward to prove, once it is stated correctly. The proof proceeds by induction on the multi-step reduction sequence that is buried in the hypothesis normal_form_of t t'. Make sure you understand the statement before you start to work on the proof.

練習問題: ★★★, standard (multistep__eval)

☐

さらなる練習問題

練習問題: ★★★, standard, optional (interp_tm)

大ステップ評価を関数 evalF としても定義しました。 既存の意味論とこの関数が等価であることを示しなさい。 （ヒント：既に eval と multistep が等価であることを示しました。 よってどちらを使っても論理的には何も問題ないはずです。 とはいえ、一方がより簡単に示せます！）

☐

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

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

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

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

結合した言語について、これら二つの性質を形式的に証明、または反証しなさい。 （つまり、定理として性質が成り立つ、または成り立たない、と明言した上でそれを示すのです。）

☐

スモールステップ Imp

ここではより本気の例として、Impの操作的意味論のスモールステップ版を示します。 The small-step reduction relations for arithmetic and boolean expressions are straightforward extensions of the tiny language we've been working up to now. To make them easier to read, we introduce the symbolic notations -->a and -->b for the arithmetic and boolean step relations.

ここでは、わざわざブール値の定義をする必要がありません。 なぜならば、以下の -->b の定義にはブール値の定義が必要ないからです(なぜでしょう？)。 言語がもうちょっと大きかったら必要になったかもしれません(なぜでしょう？)。

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

• SKIP を「コマンド値」("command value")として使います。 つまり、正規形に逹したコマンドです。
  • 代入コマンドはSKIPに簡約されます(その際に状態を更新します)。
  • コマンド合成は、左側の部分コマンドがSKIPに簡約されるのを待って、 それを捨ててしまいます。そして続けて右側の部分コマンドの簡約をします。
• WHILEコマンドの簡約は、条件文とそれに続く同じWHILEコマンドになります。

(後者の効果を得るには他にもいろいろな方法がありますが、 いずれも、もとのWHILEコマンドをどこかに保存して、ループ本体の1コピーを簡約することには変わりありません。)

並行 Imp

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

この言語で特に興味深い性質は、次のプログラムが変数Xに任意の値を入れた状態で停止させられるというものです。

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

Xを2にして停止できます: