【MoL】25 Validity Again

この章は calculus の手法に関することなので、後日やることにする。
次の章が遂に 'substitution' なので、そっちへ急ごう。プログラム検証論で一番もやもやしていたのが、このあたりなので。

このあたりはプログラム検証論に関わらずもやもやしていて、

• assignment
  
• substitution
  
• unification/instatiation
  
• term rewriting
  
• variable bindings
  

が、どういう相互関係であるかを精確に捉えられていない。ばらばらにしか理解していない。

こつこつ。