課題についてのアドバイス

• Coqによる証明問題は、そこまでに文中で行ってきた証明となるべく同じようにできるようにしています。 課題に取り組む前に、そこまでの証明を自分でも（手とCoqの両方で）やってみなさい。 そして、細部まで理解していることを確認しなさい。そうすることは、多くの時間を節約することになるでしょう。
• 問題にする Coq の証明はそれなりに複雑なため、怪しそうなところをランダムに探ってみたり、直感に任せたりといった方法で解くことはまず無理です。 なぜその性質が真で、どう進めば証明になるかを最初に考える必要があります。 そのための一番良い方法は、形式的な証明を始める前に、紙の上に非形式的な証明をスケッチでも良いので書いてみることです。 そうすることで、定理が成立することを直観的に確信できます。
• 作業を減らすために自動化を使いましょう。 この章に出てくる証明は、すべての場合を明示的に書き出すととても長くなります。

振る舞い同値性

これまでの章で、簡単なプログラム変換の正しさを調べました。 optimize_0plus関数です。 対象としたプログラミング言語は、算術式の言語の最初のバージョンでした。 それには変数もなく、そのためプログラム変換が正しいとはどういうことを意味するかを定義することはとても簡単でした。 つまり、変換の結果得られるプログラムが常に、それを評価すると元のプログラムと同じ数値になるということでした。 Imp言語全体、特に代入について、プログラム変換の正しさを語るためには、変数の役割、および状態について考えなければなりません。

定義

変数が入っているaexpとbexpについては、どう定義すれば良いかは明らかです。 2つのaexpまたはbexpが振る舞い同値である(behaviorally equivalent)とは、すべての状態で2つの評価結果が同じになることです。

Here are some simple examples of equivalences of arithmetic and boolean expressions.

コマンドについては、状況はもうちょっと微妙です。 簡単に「2つのコマンドが振る舞い同値であるとは、両者を同じ状態から開始すれば同じ状態で終わることである」と言うわけには行きません。 コマンドによっては、特定の状態から開始したときに停止しないためどのような状態にもならないことがあるからです！ すると次のように言う必要があります。 2つのコマンドが振る舞い同値であるとは、任意の与えられた状態から両者をスタートすると、(1)両者ともに発散するか、(2)両者ともに停止して同じ状態になることです。 これを簡潔に表現すると、「1つ目が停止して特定の状態になるならば2つ目も同じになり、逆もまた成り立つ」となります。

簡単な例

コマンドの同値性の例として、 SKIPにからんだ自明な変換から見てみましょう:

練習問題: ★★ (skip_right)

コマンドの後ろにSkipをつけても元のコマンドと等価なプログラムになることを示しなさい。

☐

同様にして、TESTコマンドを最適化します:

もちろん、ガードがtrueそのままである条件文を書こうとするプログラマなんていないでしょう。 興味深いのは、ガードが真と「同値である」場合です。 「定理」:もしbがBTrueと同値ならば、TEST b THEN c1 ELSE c2 FIはc1と同値である。 「証明」:

• (->) すべてのstとst'に対して、もしst =[ TEST b THEN c1 ELSE c2 FI ]=> st'ならばst =[ c1 ]=> st'となることを示す。
  [st =[ TEST b THEN c1 ELSE c2 FI ]=> st']を示すのに使うことができた可能性のある規則、つまり[E_IfTrue]と[E_IfFalse]とで、場合分けをする。 - [st =[ TEST b THEN c1 ELSE c2 FI ]=> st'] の導出の最後の規則が[E_IfTrue]であると仮定する。 このとき、[E_IfTrue]の仮定より[st =[ c1 ]=> st']となる。 これはまさに証明したいことである。 - 一方、[st =[ TEST b THEN c1 ELSE c2 FI ]=> st'] の導出の最後の規則が[E_IfFalse]と仮定する。 すると、[beval st b = false]かつ[st =[ c2 ]=> st']となる。 [b]が[BTrue]と同値であったことから、すべての[st]について、[beval st b = beval st BTrue]が成立する。 ここで[beval st BTrue = true]であるため、これは特に[beval st b = true]を意味する。 しかしこれは矛盾である。 なぜなら、[E_IfFalse]から[beval st b = false]でなければならないからである。 従って、最後の規則は[E_IfFalse]ではあり得ない。 - ([<-]) すべての[st]と[st']について、もし[st =[ c1 ]=> st']ならば[st =[ TEST b THEN c1 ELSE c2 FI ]=> st']となることを示す。 [b]が[BTrue]と同値であることから、[beval st b] = [beval st BTrue] = [true]となる。 仮定[st =[ c1 ]=> st']より[E_IfTrue]が適用でき、[st =[ TEST b THEN c1 ELSE c2 FI ]=> st']となる。 [] 以下がこの証明の形式化版です:

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

☐

Exercise: 3 stars, standard (swap_if_branches)

Show that we can swap the branches of an IF if we also negate its guard.

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

ガード部の否定を取ることで、条件文の中身を入れ替えることができることを示しなさい。

☐

WHILEループについては、同様の2つ定理があります。 ガードがBFalseと同値であるループはSKIPと同値である、というものと、ガードがBTrueと同値であるループはWHILE BTrue DO SKIP END（あるいは他の任意の停止しないプログラム）と同値である、というものです。 1つ目のものは簡単です。

練習問題: ★★, advanced, optional (WHILE_false_informal)

WHILE_falseの非形式的証明を記述しなさい。 ☐

2つ目の事実を証明するためには、ガードがBTrueと同値であるwhileループが停止しないことを言う補題が1つ必要です:

「補題」:bがBTrueと同値のとき、st =[ WHILE b DO c END ]=> st'となることはない。 「証明」:st =[ WHILE b DO c END ]=> st'と仮定する。 st =[ WHILE b DO c END ]=> st'の導出についての帰納法によって、この仮定から矛盾が導かれることを示す。 考える必要のある場合分けは E_WhileFalse と E_WhileTrue であり、それ以外はコマンドが矛盾する。

• st =[ WHILE b DO c END ]=> st' が規則E_WhileFalseから証明されると仮定する。 すると仮定からbeval st b = false となる。 しかしこれは、bがBTrueと同値という仮定と矛盾する。
• st =[ WHILE b DO c END ]=> st' が規則E_WhileTrueを使って証明されると仮定する。 このとき、以下のことがわかる。
  1. beval st b = trueが成り立つ。 2. ある状態 st0 があり、st =[ c ]=> st0 と st0 =[ WHILE b DO c END ]=> st' が成り立つ。 3. 帰納法の仮定から、st0 =[ WHILE b DO c END ]=> st' は矛盾を導く。
  この2と3から矛盾が導かれる。 ☐

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

補題WHILE_true_nontermが意味するものを日本語で書きなさい。 ☐

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

以下の定理を示しなさい。 ヒント：ここでWHILE_true_nontermを使いなさい。

☐ A more interesting fact about WHILE commands is that any number of copies of the body can be "unrolled" without changing meaning. Loop unrolling is a common transformation in real compilers.

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

☐ Proving program properties involving assignments is one place where the fact that program states are treated extensionally (e.g., x !-> m x ; m and m are equal maps) comes in handy.

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

☐

Exercise: 2 stars, standard (equiv_classes)

Given the following programs, group together those that are equivalent in Imp. Your answer should be given as a list of lists, where each sub-list represents a group of equivalent programs. For example, if you think programs (a) through (h) are all equivalent to each other, but not to (i), your answer should look like this: [prog_a;prog_b;prog_c;prog_d;prog_e;prog_f;prog_g;prog_h] ; [prog_i] Write down your answer below in the definition of equiv_classes.

☐

振る舞い同値の性質

ここからは、プログラムの同値性に関する性質を調べていきましょう。

振る舞い同値は同値関係である

最初に、aexp、bexp、comの同値が、本当に「同値関係」であること、つまり、反射性、対称性、推移性を持つことを検証します。 証明は簡単です。

振る舞い同値は合同関係である

少しわかりにくいですが、振る舞い同値は、合同関係(congruence)でもあります。 つまり、2つのサブプログラムが同値ならば、それを含むプログラム全体も同値です:

              aequiv a1 a1' 
      ----------------------------- 
      cequiv (x ::= a1) (x ::= a1') 
 
              cequiv c1 c1' 
              cequiv c2 c2' 
         -------------------------- 
         cequiv (c1;;c2) (c1';;c2') 

他のコマンドも同様です。

（注意して欲しいのですが、ここで推論規則の記法を使っていますが、これは定義の一部ではありません。 単に正しい含意を読みやすい形で書き出しただけです。 この含意は以下で証明します。）

合同性がなぜ重要なのか、次の節で具体的な例(fold_constants_com_soundの証明)によって見ます。 ただ、メインのアイデアは、大きなプログラムの小さな部分を同値の小さな部分で置き換えると、大きなプログラム全体が元のものと同値になることを、変化していない部分についての明示的な証明「なしに」わかるということです。 つまり、大きなプログラムの小さな変更についての証明の負担が、プログラムではなく変更に比例するということです。

ループの合同性は帰納法が必要になるので、さらに少しおもしろいものになります。 「定理」:WHILEについての同値は合同関係である。 すなわち、もしb1がb1'と同値であり、c1がc1'と同値ならば、WHILE b1 DO c1 ENDはWHILE b1' DO c1' ENDと同値である。 「証明」:b1がb1'と同値、c1がc1'と同値であるとする。 すべてのstとst'について、証明すべきことは、st =[ WHILE b1 DO c1 END ]=> st'の必要十分条件はst =[ WHILE b1' DO c1' END ]=> st'であることである。 必要条件と十分条件の両方向を別々に証明する。

• (->) st =[ WHILE b1 DO c1 END ]=> st'ならば st =[ WHILE b1' DO c1' END ]=> st'であることを、st =[ WHILE b1 DO c1 END ]=> st'の導出についての帰納法で示す。 自明でないのは、導出の最後の規則がE_WhileFalseまたはE_WhileTrueのときだけである。
  • E_WhileFalse: この場合、規則の形からbeval st b1 = falseかつst = st'となる。 しかしb1とb1'が同値であることからbeval st b1' = falseになる。 さらにE_WhileFalseを適用すると証明すべきst =[ WHILE b1' DO c1' END ]=> st'が得られる。
  • E_WhileTrue: 規則の形からbeval st b1 = trueおよび、ある状態st'0について帰納法の仮定st'0 =[ WHILE b1' DO c1' END ]=> st'のもとで、 st =[ c1 ]=> st'0かつst'0 =[ WHILE b1 DO c1 END ]=> st'となる。
    c1とc1'が同値であることから、st =[ c1' ]=> st'0となる。 さらにb1とb1'が同値であることから、beval st b1' = trueとなる。 E_WhileTrueを適用すると、証明すべきst =[ WHILE b1' DO c1' END ]=> st'が得られる。
• (<-) 同様である。 ☐

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

☐

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

☐

同値である2つのプログラムとその同値の証明の例です...

Exercise: 3 stars, advanced, optional (not_congr)

We've shown that the cequiv relation is both an equivalence and a congruence on commands. Can you think of a relation on commands that is an equivalence but not a congruence?

プログラム変換

プログラム変換(program transformation)とは、プログラムを入力とし、出力としてそのプログラムの何らかの変形を生成する関数です。 定数畳み込みのようなコンパイラの最適化は標準的な例ですが、それ以外のものもたくさんあります。

プログラム変換が健全(sound)とは、その変換が元のプログラムの振る舞いを保存することです。

定数畳み込み変換

式が定数(constant)であるとは、その式が変数参照を含まないことです。 定数畳み込みは、定数式をその値に置換する最適化です。

定数畳み込みのこのバージョンは簡単な足し算等を消去していないことに注意します。 複雑になるのを避けるため、1つの最適化に焦点を絞っています。 式の単純化の他の方法を組込むことはそれほど難しいことではありません。 定義と証明が長くなるだけです。

（BEqとBLeの場合に）fold_constants_aexpをbexpに持ち上げることができるだけでなく、定数「ブール」式をみつけてその場で置換することもできます。

コマンド内の定数を畳み込みするために、含まれるすべての式に対応する畳み込み関数を適用します。

定数畳み込みの健全性

上でやったことが正しいことを示さなければなりません。

以下が算術式に対する証明です:

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

ここに、ブール式の定数畳み込みに関する健全性の議論のBEqの場合の非形式的証明を示します。 これを丁寧に読みその後の形式的証明と比較しなさい。 次に、形式的証明のBLe部分を（もし可能ならばBEqの場合を見ないで）記述しなさい。 「定理」:ブール式に対する定数畳み込み関数fold_constants_bexpは健全である。 「証明」:すべてのブール式bについてbがfold_constants_bexp bと同値であることを示す。 bについての帰納法を行う。 bがBEq a1 a2という形の場合を示す。 この場合、
       beval st (BEq a1 a2)
     = beval st (fold_constants_bexp (BEq a1 a2))

を示せば良い。これには2種類の場合がある:

• 最初に、あるn1とn2について、fold_constants_aexp a1 = ANum n1かつfold_constants_aexp a2 = ANum n2と仮定する。
  この場合、
             fold_constants_bexp (BEq a1 a2)
           = if n1 =? n2 then BTrue else BFalse
  かつ
             beval st (BEq a1 a2)
           = (aeval st a1) =? (aeval st a2)
  となる。 算術式についての定数畳み込みの健全性（補題fold_constants_aexp_sound）より、
             aeval st a1
           = aeval st (fold_constants_aexp a1)
           = aeval st (ANum n1)
           = n1
  かつ
             aeval st a2
           = aeval st (fold_constants_aexp a2)
           = aeval st (ANum n2)
           = n2
  である。 従って、
             beval st (BEq a1 a2)
           = (aeval a1) =? (aeval a2)
           = n1 =? n2
  となる。 また、（n1 = n2とn1 <> n2の場合をそれぞれ考えると）
             beval st (if n1 =? n2 then BTrue else BFalse)
           = if n1 =? n2 then beval st BTrue else beval st BFalse
           = if n1 =? n2 then true else false
           = n1 =? n2
  となることは明らかである。 ゆえに
             beval st (BEq a1 a2)
           = n1 =? n2
           = beval st (if n1 =? n2 then BTrue else BFalse)
  となる。 これは求められる性質である。
• それ以外の場合、fold_constants_aexp a1とfold_constants_aexp a2のどちらかは定数ではない。この場合、
             beval st (BEq a1 a2)
           = beval st (BEq (fold_constants_aexp a1)
                           (fold_constants_aexp a2))
  を示せば良い。 bevalの定義から、これは
             (aeval st a1) =? (aeval st a2)
           = (aeval st (fold_constants_aexp a1)) =?
                     (aeval st (fold_constants_aexp a2))
  を示すことと同じである。 算術式についての定数畳み込みの健全性（補題fold_constants_aexp_sound）より、
           aeval st a1 = aeval st (fold_constants_aexp a1)
           aeval st a2 = aeval st (fold_constants_aexp a2)
  となり、この場合も成立する。 ☐

(Doing induction when there are a lot of constructors makes specifying variable names a chore, but Coq doesn't always choose nice variable names. We can rename entries in the context with the rename tactic: rename a into a1 will change a to a1 in the current goal and context.)

☐

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

次の証明のWHILEの場合を完成させなさい。

☐

(0 + n)の消去の健全性、再び

練習問題: ★★★★, advanced, optional (optimize_0plus)

「論理の基礎」のImpの章のoptimize_0plusの定義をふり返ります。
    Fixpoint optimize_0plus (e:aexp) : aexp :=
      match e with
      | ANum n =>
          ANum n
      | APlus (ANum 0) e2 =>
          optimize_0plus e2
      | APlus e1 e2 =>
          APlus (optimize_0plus e1) (optimize_0plus e2)
      | AMinus e1 e2 =>
          AMinus (optimize_0plus e1) (optimize_0plus e2)
      | AMult e1 e2 =>
          AMult (optimize_0plus e1) (optimize_0plus e2)
      end.

この関数は、aexpの上で定義されていて、状態を扱わないことに注意します。 変数を扱えるようにした、この関数の新しいバージョンを記述しなさい。 加えて、bexpおよびコマンドに対しても、同様のものを記述しなさい:
     optimize_0plus_aexp
     optimize_0plus_bexp
     optimize_0plus_com

これらの関数の健全性を、fold_constants_*について行ったのと同様に証明しなさい。 optimize_0plus_comの証明においては、合同性補題を使いなさい（そうしなければ証明はとても長くなるでしょう!）。 次に、コマンドに対して次の処理を行う最適化関数を定義しなさい。 行うべき処理は、まず定数畳み込みを（fold_constants_comを使って）行い、次に0 + n項を（optimize_0plus_comを使って）消去することです。

• この最適化関数の出力の意味のある例を示しなさい。
• この最適化関数が健全であることを示しなさい。（この部分は「とても」簡単なはずです。）

非等価性の証明

c1がX ::= a1; Y ::= a2という形のコマンドで、c2がコマンドX ::= a1; Y ::= a2'であると仮定します。 ただしa2'は、a2の中のすべてのXをa1で置換したものとします。 例えば、c1とc2は次のようなものです。
       c1 = (X ::= 42 + 53;;
               Y ::= Y + X)
       c2 = (X ::= 42 + 53;;
               Y ::= Y + (42 + 53))

明らかに、この例の場合はc1とc2は同値です。 しかし、一般にそうだと言えるでしょうか？

この後すぐ、そうではないことを示します。 しかし、ここでちょっと立ち止まって、自分の力で反例を見つけることができるか試してみるのは意味があることです。

次が、式aの中の変数xを別の算術式uで置換する関数の形式的定義です。

そして次が、興味対象の性質です。 上記コマンドc1とc2が常に同値であることを主張するものです。

残念ながら、この性質は、常には成立「しません」。 つまり、すべてのx1, x2, a1, a2について、次が成立するわけではない、ということです。
      cequiv (x1 ::= a1;; x2 ::= a2)
             (x1 ::= a1;; x2 ::= subst_aexp x1 a1 a2)

仮にすべてのx1, x2, a1, a2について
      cequiv (x1 ::= a1;; x2 ::= a2)
             (x1 ::= a1;; x2 ::= subst_aexp x1 a1 a2)

が成立するとしましょう。 ここで、次のプログラムを考えます。
      X ::= X + 1;; Y ::= X

次のことに注意しましょう。
      empty_st =[ X ::= X + 1;; Y ::= X ]=> st1

ここで st1 = (Y !-> 1 ; X !-> 1) です。 仮定より、次が言えます。
      cequiv (X ::= X + 1;;
              Y ::= X)
             (X ::= X + 1;;
              Y ::= X + 1)

すると、cequivの定義より、次が言えます。
      empty_st =[ X ::= X + 1;; Y ::= X + 1 ]=> st1

しかし次のことも言えます。
      empty_st =[ X ::= X + 1;; Y ::= X + 1 ]=> st2

ただし st2 = (Y !-> 2 ; X !-> 1) です。 st1 <> st2であるはずなので、これはcevalが決定性を持つことに矛盾します! ☐

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

上で成立すると考えていた同値は、完全に意味がないものではありません。 それは実際、ほとんど正しいのです。それを直すためには、最初の代入の右辺に変数Xが現れる場合を排除すれば良いのです。

var_not_used_in_aexpを使って、subst_equiv_propertyの正しいバージョンを形式化し、証明しなさい。

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

無限ループがSKIPと同値でないことを示しなさい。

☐

Extended Exercise: Nondeterministic Imp

As we have seen (in theorem ceval_deterministic in the Imp chapter), Imp's evaluation relation is deterministic. However, non-determinism is an important part of the definition of many real programming languages. For example, in many imperative languages (such as C and its relatives), the order in which function arguments are evaluated is unspecified. The program fragment x = 0;; f(++x, x) might call f with arguments (1, 0) or (1, 1), depending how the compiler chooses to order things. This can be a little confusing for programmers, but it gives the compiler writer useful freedom. In this exercise, we will extend Imp with a simple nondeterministic command and study how this change affects program equivalence. The new command has the syntax HAVOC X, where X is an identifier. The effect of executing HAVOC X is to assign an arbitrary number to the variable X, nondeterministically. For example, after executing the program: HAVOC Y;; Z ::= Y * 2 the value of Y can be any number, while the value of Z is twice that of Y (so Z is always even). Note that we are not saying anything about the probabilities of the outcomes -- just that there are (infinitely) many different outcomes that can possibly happen after executing this nondeterministic code. In a sense, a variable on which we do HAVOC roughly corresponds to an uninitialized variable in a low-level language like C. After the HAVOC, the variable holds a fixed but arbitrary number. Most sources of nondeterminism in language definitions are there precisely because programmers don't care which choice is made (and so it is good to leave it open to the compiler to choose whichever will run faster). We call this new language Himp (``Imp extended with HAVOC'').

To formalize Himp, we first add a clause to the definition of commands.

Exercise: 2 stars, standard (himp_ceval)

Now, we must extend the operational semantics. We have provided a template for the ceval relation below, specifying the big-step semantics. What rule(s) must be added to the definition of ceval to formalize the behavior of the HAVOC command?

As a sanity check, the following claims should be provable for your definition:

☐ Finally, we repeat the definition of command equivalence from above:

Let's apply this definition to prove some nondeterministic programs equivalent / inequivalent.

Exercise: 3 stars, standard (havoc_swap)

Are the following two programs equivalent?

If you think they are equivalent, prove it. If you think they are not, prove that.

☐

Exercise: 4 stars, standard, optional (havoc_copy)

Are the following two programs equivalent?

If you think they are equivalent, then prove it. If you think they are not, then prove that. (Hint: You may find the assert tactic useful.)

☐ The definition of program equivalence we are using here has some subtle consequences on programs that may loop forever. What cequiv says is that the set of possible terminating outcomes of two equivalent programs is the same. However, in a language with nondeterminism, like Himp, some programs always terminate, some programs always diverge, and some programs can nondeterministically terminate in some runs and diverge in others. The final part of the following exercise illustrates this phenomenon.

Exercise: 4 stars, advanced (p1_p2_term)

Consider the following commands:

Intuitively, p1 and p2 have the same termination behavior: either they loop forever, or they terminate in the same state they started in. We can capture the termination behavior of p1 and p2 individually with these lemmas:

☐

Exercise: 4 stars, advanced (p1_p2_equiv)

Use these two lemmas to prove that p1 and p2 are actually equivalent.

☐

Exercise: 4 stars, advanced (p3_p4_inequiv)

Prove that the following programs are not equivalent. (Hint: What should the value of Z be when p3 terminates? What about p4?)

☐

Exercise: 5 stars, advanced, optional (p5_p6_equiv)

Prove that the following commands are equivalent. (Hint: As mentioned above, our definition of cequiv for Himp only takes into account the sets of possible terminating configurations: two programs are equivalent if and only if the set of possible terminating states is the same for both programs when given a same starting state st. If p5 terminates, what should the final state be? Conversely, is it always possible to make p5 terminate?)

☐

さらなる練習問題

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

この練習問題は、Impの章のoptionalの練習問題 add_for_loop を拡張したものです。 もとの add_for_loop は、コマンド言語に C言語のスタイルの forループを追加しなさい、というものでした。 ここでは次のことを証明しなさい:
      for (c1 ; b ; c2) {
          c3
      }

は
       c1 ;
       WHILE b DO
         c3 ;
         c2
       END

と同値である。