2015年10月03日

たまにはどうでもいいこと

最近は一人のんびりと作業をする日々である。
これでお金がもらえるならなによりだが、まあお金はほとんど(当たり前だが家にいる間は全く)もらってない。
研究やったり、なんとなく遊んで夜中になったら唐突にCoqをいじり始めたり。
そんな生活なので、生活リズムという語が消えてしまった。

健康って何だっけなあ。

最近Coqでいじってるのはとある定性空間表現というものなのだが、記号表現なのでCoqで扱いやすい反面、図形的なものを見いだすのに記号をこねくり回す必要がある。
そのせいでコードが長くなること長くなること。
3月までいた学生が主にやっていた定式化なのだけれど、1月くらいから手伝って、今およそ17000行か18000行くらい。当てにならないけれどwcだと19000行を越えている。年度始まって書き加えたのは10000行いかないくらい?
あと数千行くらいは増えそうだなあ。いろいろ減らせそうな部分もあるけど。

とりあえず、ある程度以上の規模になって思うのは、誤りを見つけたときの編集がやはり難しいということだ。
特に証明はまずい。
さっぱりどこがどこの対応かわからない。
ある程度bulletを使って証明を木っぽく表現できるけれど、もっと気合い入れて全部木構造に出来ないものだろうか。
ただしProof Termを直接扱うのはパスで。
でかすぎて遅くなるし。
posted by chiguri at 00:52| Comment(0) | 日記