証明しやすいように書くこと

レシピを書いていたとき、証明ができやすいように、書き直すということを何度もやった。

ひとつの述語をあちこちで使い回すと、曖昧になり、証明を作るのが難しくなる。それを回避するため、述語をわけて書いてみたりした。

数学で、同じ定理を証明するのにいろいろな方法があるのと、簡単には比較できないけれど、そういうことはあるかもしれない。

証明のしやすさを考えて、述語の使い方を変えるのは、プログラムのアルゴリズムを工夫するのと同じような感覚なのかなと思う。

だとすると、proverが非力でも、なんとかなる世界があるようにも思うが、そういう書き換えは、あんまり好きではない。たぶん、論理式でどこまで書けるのかに興味があるからかな。