情報は力ではない

UE4 とか Blender とか。

TaPL 演習3.5.14

問題

定理3.5.4が算術演算の評価関係に関しても成り立つことを示せ。
すなわち、 t→t' かつ  t→t'' ならば  t'=t'' であることを示せ。

証明

 t→t' の導出に関する帰納法を使用し、  t→t' の導出で最後に使った規則に対する場合分けにより証明する。

 (i) E-SUCCの場合

 t succ  t_1 という形であり、またある  t_1' が存在して  t_1→t_1' である。
左側の最も外側に  succ を用いている規則はE-SUCCのみである。 よって、 t→t'' の導出で最後に使った規則もE-SUCCであり、ある  t_1'' が存在して t_1→t_1'' である。 帰納法の仮定より、 t_1' = t_1'' 。 したがって、 t' = succ  t_1' = succ  t_1'' = t''

 (ii) E-PREDZEROの場合

 t pred  t_1 という形であり、 t_1 = 0 である。 左側の最も外側に  pred を用いている規則はE-PREDZERO、E-PREDSUCCとE-PREDの3つであるので  t→t'' の導出の最後に使った規則はこのうちのいずれかである。  t→t'' の導出で最後に使った規則はE-PREDではない。 E-PREDであれば、ある  t_1'' が存在して  t_1→t_1'' となるが、0は値なので、評価されないからである。 E-PREDSUCCの場合、 t_1 = succ  nv_1となるが、 t_1 = 0 であるのでE-PREDSUCCでもない。 よって、 t→t'' の導出の最後に使った規則はE-PREDZEROであり、 t' = t'' となる。

 (iii) E-PREDSUCCの場合

 t pred  t_1 という形であり、 t_1 = succ  nvである。  (ii)と同様の推論により、 t→t'' の導出の最後に使った規則はE-PREDSUCCであることがわかる。 よって、 t' = t'' となる。

 (iv) E-PREDの場合

 t pred  t1という形であり、ある  t_1' が存在して  t_1→t_1' である。 (ii)と同様の推論により、 t→t'' の導出で最後に使った規則がE-PREDであることがわかる。 このとき、ある  t_1'' が存在して、 t_1→t_1'' である。 帰納法の仮定より、 t_1' = t_1''。 よって、 t' = pred  t_1' = pred  t_1'' = t''

 (v) E-ISZEROZEROの場合

 t iszero  t_1 という形をしており、 t_1 = 0である。 左側の最も外側に iszero を用いている規則はE-ISZEROZERO、E-ISZEROSUCC、E-ISZEROがあるが  succ  nv_1 と0は異なるので、 t→t'' の導出で最後に使った規則はE-ISZEROSUCCではない。 また、E-ISZEROでもない。なぜなら、E-ISZEROであれば、ある  t_1' が存在して t_1→t_1' となるが 0は値なので評価されないからである。 よって t→t'' の導出で最後に使った規則はE-ISZEROZEROであり、 t' = t''

 (vi) E-ISZEROSUCCの場合

 t iszero  t_1 という形をしており、 t_1 = succ  nv_1 である。  (v) と同様の推論で、 t→t'' の導出で最後に使った規則がE-ISZEROSUCCであることがわかる。 よって、 t' = t''

 (vii) E-ISZEROの場合

 t iszero  t_1という形をしており、ある t_1' が存在して  t_1→t_1' である。  (v) と同様の推論により、 t→t'' の導出で最後に使った規則がE-ISZEROであることがわかる。 このとき、ある  t_1'' が存在して、 t_1→t_1'' である。 帰納法の仮定より、 t_1' = t_1''。 よって、 t' = iszero  t_1' = iszero  t_1'' = t''

以上より、 t→t' かつ  t→t'' ならば  t' = t'' である。

所感

解答に書いている通り、tの構造に関する帰納法を用いたほうが簡潔だなぁ。