2024-01-01から1年間の記事一覧
TaPL24章のネタです。まずStatementがcoqで正しく書けているか怪しいですが… Theorem exists_forall_second: forall T: Prop -> Prop, ((exists X, T X) <-> (forall Y: Prop, (forall X, T X -> Y) -> Y)). intros. split. - intros. destruct H. now apply…
D - Halftree意外とこの解き方している人が少ないように見えたので。例えば入力が7 3の場合は (0,1)(1,2)(2,3) と辺を張れば0~6の線グラフが得られることが分かると思います。 9 3の場合は頂点7, 8が残ってしまいますが、(7,5)と辺を張ることで、線グラフ+α…
修士を修了 特に問題なく、スムーズに卒業できたし、得られた結果も個人的には満足できるものでした。国際会議(といっても査読がすごく厳しいところではない)に出したり、arXivに投稿したりして、当時の自分はそれでいっぱいいっぱいになっていたけど、今見…