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の構造に関する帰納法を用いたほうが簡潔だなぁ。