cocolog:84149980

Isabelle で過去にやった証明を再度証明している。Isabelle の simplifier をうまく働かすことができなくて、辛い。また、最近、寝ているというか横になってる時間がちょっと言えないほど長くなっている。 (JRF 4863)

JRF 2015年12月16日 (水) Tweet

Isabelle について前回言及したのは、[cocolog:84021412] だが、そこで以前、ラムダ計算のα同値に関する証明を昔やったと書いたが、その証明を基礎の部分から辿って、「再証明」していっている。

JRF2015/12/164022

以前やったのは tactic、tactical を使った証明で、それを参考に apply ... done 形式の証明にしていっている。定理の名前などが15年以上前からほとんど変わっていないのはありがたく、証明の細部を理解できないのに再証明ができてしまっている。

ただ、昔はプログラム言語 ML を使って、symmetric な証明を自動的に解くとかいったことをやっていたのだが、そういうのは(私の技術不足もあり)使えなくなっている。

JRF2015/12/163116

昔は asm_full_simp_tac で今は simp になっている simplifier は、昔はいちいち、どの理論のものを使うか指定して、一番軽そうなのを選んでやっていたのが、定理に simp の属性を付けて積み上げていく方式になっているため、重く、内部がわかりにくくなっている。

JRF2015/12/160262

その simplifier だが昔の設定に近い設定で試そうとすると、やたらと無限ループに落ち込んでしまう。simplifier に add する定理がまずいらしい。でも、原因がはっきりと掴めず、いろいろ悩んでしまって辛い。細々と declare THEOREMs [simp] や declare THEOREMs [simp del] をやって調整したりするのが普通の方法なんだろうか、そういうことも妥当かどうかわからず、やってしまうしかないのが苦しい。

JRF2015/12/161799

まだ、証明が最初のほうで simplifier とかの出番が少ないところをやってるから、昔の定理の証明の書き直し版でも通ってる面がありそうで、この先のことを考えると気がめいる。

JRF2015/12/163586

もし、大きく詰まることがあったら、諦めるのも選択肢の一つだと思っている。諦めて、できたところまでで(legacy なソースと共に)公開してお茶をにごすかもしれない。

JRF2015/12/163661

……。

Isabelle を離れて、近況も少し。

最近、ものすごく寝る時間が長い。一度起きてごはん食べて、すぐに寝て、ずっと布団の中にいるみたいなふうな日がある。横になっているだけで眠りはしていない時間も長いのだけど、それでもずっと横になっている。その時間がどれぐらいかというのは、働いている人に申し訳なくて、ちょっと言えない。前から、そうだったんだけど、最近、特に長くなってしまった。怠惰になってしまった。

JRF2015/12/162887

でも、夜中は目が冴えることがあって、朝まで PC に向かって、プログラミング…上の証明をしたりすることもあったりする。それで、朝になって寝ないとダメだと思って、朝から寝るんだけど、眠りが浅くて、またダラダラと長く寝てしまったりしている。本当に申し訳ない。…申し訳ないといいつつ、それを変えたりはしないのだけれど…。つくづく私は怠惰だ。

JRF2015/12/168015

この怠惰と Isabelle での証明との関係はほぼないはず…。前から寝過ぎだったから。が、Isabelle での証明は私の過去に触れる行為で、それが少しストレスになっているという面はあるかもしれない。証明そのものがストレスフルだというのも少しはあるかもしれない。これが終ったあと何もすることがなくなるのではないか…という不安も少しある。関係あるかは、よくわからない。

JRF2015/12/160558

あと、表現規制の強化のニュースをチラと見て、へこむ。本当は闘志を燃やさないといけないところなのに気がめいる。私がトシをとって若い人ほどアダルト分野への関心を持たなくなってる面はなきにしもあらずで、他も「高齢化」により保守的な方向に流れがちなように思う。若い人のために今ある自由ぐらいは少なくとも残さねばならないと思う。私のこの先、関心は維持しようと思わないと維持できないのかもしれない。

JRF2015/12/164101