TaPL 演習3.5.14
問題
定理3.5.4が算術演算の評価関係に関しても成り立つことを示せ。
すなわち、 かつ ならば であることを示せ。
証明
の導出に関する帰納法を使用し、 の導出で最後に使った規則に対する場合分けにより証明する。
E-SUCCの場合
は という形であり、またある が存在して である。
左側の最も外側に を用いている規則はE-SUCCのみである。
よって、 の導出で最後に使った規則もE-SUCCであり、ある が存在して である。
帰納法の仮定より、 。
したがって、
E-PREDZEROの場合
は という形であり、 である。 左側の最も外側に を用いている規則はE-PREDZERO、E-PREDSUCCとE-PREDの3つであるので の導出の最後に使った規則はこのうちのいずれかである。 の導出で最後に使った規則はE-PREDではない。 E-PREDであれば、ある が存在して となるが、0は値なので、評価されないからである。 E-PREDSUCCの場合、 となるが、 であるのでE-PREDSUCCでもない。 よって、 の導出の最後に使った規則はE-PREDZEROであり、 となる。
E-PREDSUCCの場合
は という形であり、 である。 と同様の推論により、 の導出の最後に使った規則はE-PREDSUCCであることがわかる。 よって、 となる。
E-PREDの場合
は という形であり、ある が存在して である。 (ii)と同様の推論により、 の導出で最後に使った規則がE-PREDであることがわかる。 このとき、ある が存在して、 である。 帰納法の仮定より、。 よって、
E-ISZEROZEROの場合
は という形をしており、である。 左側の最も外側に を用いている規則はE-ISZEROZERO、E-ISZEROSUCC、E-ISZEROがあるが と0は異なるので、 の導出で最後に使った規則はE-ISZEROSUCCではない。 また、E-ISZEROでもない。なぜなら、E-ISZEROであれば、ある が存在して となるが 0は値なので評価されないからである。 よって の導出で最後に使った規則はE-ISZEROZEROであり、
E-ISZEROSUCCの場合
は という形をしており、 である。 と同様の推論で、 の導出で最後に使った規則がE-ISZEROSUCCであることがわかる。 よって、
E-ISZEROの場合
は という形をしており、ある が存在して である。 と同様の推論により、 の導出で最後に使った規則がE-ISZEROであることがわかる。 このとき、ある が存在して、 である。 帰納法の仮定より、。 よって、
以上より、 かつ ならば である。
所感
解答に書いている通り、tの構造に関する帰納法を用いたほうが簡潔だなぁ。