累積帰納法の一般化

coq

TopProver で行われたCoqコンテストに参加して、モチベが上がったため、coqのライブラリを整備することに。 とりあえず便利なので累積帰納法を整備した。 自然数に関する累積帰納法だけだと不便なことがあるので、より一般化し、任意の型 X の f による nat …

opam install z3 が "clang: error: unsupported option '-fopenmp'" で落ちる

## 解決策ocamlc の -cc オプションで clang の代わりに gcc を指定させる. バッドノウハウだが, ocamlc と ocamlfind を wrap する.コマンドを理解してから使ってください cc=`which gcc` dir="$(dirname $(which ocamlc))" if [ ! -e $dir/ocamlc_ -a -e $…

Myアニメ・映画・ノベルゲームキュー

僕がいつか見るアニメ・映画・ノベルゲームキューです。 キューなので先頭(上)からしか取り出せません。 おすすめされるとキューの末尾に追加されます。たいていのアニメは数話で切ることになると思います。 キューに入っていても構わずおすすめしてください…

Myおすすめアニメランキング

僕(drafear)が全話視聴したアニメリストです. 個人的に良かった順に並べています. あんまりだらだらと感想書いても仕方ないので短く書いています. 一部ノベルゲームが含まれています. 特におすすめしたいものなので.あまり合わなかったアニメも載せています…

dijkstraの空間計算量(メモリ使用量)をO(V)に減らす

Priority Queue を使った実装だと時間計算量 \(O(V + ElogE)\), 空間計算量 \(O(V + E)\) になると思います。実装は重くなるのと定数が重いですが、Priority Queue の代わりに Segment Tree を使うと時間計算量 \(O(V + ElogV)\), 空間計算量 \(O(V)\) に改…

全方位木DPライブラリを作った

概要 森に対して全方位木DPを行うライブラリです。 全方位森DPの方がいいんかな。 森でないときにassertが落ちるようにするためにUnionFindを使っています。 パフォーマンスが気になるなら使わないように実装しなおすと良いかもしれません。 計算量 construc…

gdbでredirectが使えない

僕の環境 $ gdb a.out -eval-command run < nyuryoku 通常の環境 普通、gdbでredirectするには、下のようにすれば良いらしい。 $ gcc -g a.cpp -o a.out $ gdb a.out (gdb) run < nyuryokuただ、僕の環境では (gdb) run "<" "nyuryoku"と解釈されてしまいう…

JISキーボードをUSキーボードとして使う

結論 Windows Keymapする。1. お手軽な方法↓をDLして実行、気に入ったらスタートアップ(shell:startup)に登録する。www.dropbox.com2. 編集したいならAutoHotkey をインストールして以下のスクリプトを hoge.ahk などと保存して実行する。気に入ったらスター…

python3でバイナリデータを標準出力に出力する

python3でcgiを書いていて、画像データを標準出力に出力しようとしてハマったのでメモ 結論 1. sys.stdout.buffer.write を使う 2. 先に print を使っていたなら sys.stdout.buffer.write の直前に sys.stdout.flush を呼ぶ サンプルコード print("Content-T…

ECNA 2016 - D: Lost in Translation ★★☆☆☆

評価・感想 制約小さくて想定解とは異なる気もするけど、 DAGなら最小有向全域木の1ステップ目で終わるというのが面白かった。 問題 Englishで書かれた本があり、それをnヶ国語に翻訳したい。 m人の翻訳者の候補が居て、i番目の人は言語を言語(またはその逆)…

2016-2017 ACM-ICPC Pacific Northwest Regional Contest (Div. 1) - G: Maximum Islands ★★★☆☆

評価・感想 フローと塗りつぶしの2ステップがあるけどそこまで実装重くなく, 教育的良問だと思った. 二部グラフの最大安定集合は二部グラフの最小点カバーになって最小カットになって最大流になってすごく楽しい. 二部グラフの最大マッチング=最小頂点被覆 …

2016-2017 ACM-ICPC Pacific Northwest Regional Contest (Div. 1) - F: Illumination ★★★★☆

評価 2-SATに見えない良問. dfsしてしまいWA, 同値類で分解できるじゃーんと言ってUFしてWAした. 問題 n×nのグリッドのいくつかのマスに照明がある. 照明は全部でL個あり, 照明iは, に配置されている. 各照明は上下または左右に距離Rまで(合計2R+1マス)照ら…

2016-2017 ACM-ICPC Pacific Northwest Regional Contest (Div. 1) - B: Buggy Robot ★★★☆☆

評価 良問だが若干実装疲れた. 初め, dijkstraに見えなかった. 解くのにそんなに時間がかからなかったし若干実装重いB問題かーくらいの感覚だったけど, 解いてる人数少なくて驚いた. 問題 迷路と操作列が与えられる. 操作列はUDLR(上下左右)からなる文字列で…

iTerm2でタブの複製をしたい

コマンドや移動の履歴まで複製できれば最高だが, ここではカレントディレクトリだけの複製をした. 応用すれば "新しいタブでコマンド実行" などが容易にできる. it2_newtab.applescript #!/usr/bin/osascript -- Usage: oscript it2_newtab.applescript prof…

ラピゲ勉強会した

京大マイコンクラブ (KMC)で毎年新入生向けに開催されているイベント「ラピッドコーディグ祭り」に向けてゲームを作ってみた。 ラピッドコーディグ祭りはゲームを作ったことない新入生でも上回生の手厚いサポートの下で1日で1からゲームを作ることを体験して…

はてなブログのアイコンの画質悪くね?

自分の記事上だけでいいから、とりあえずアイコンの画質を上げたいと思って、外部のアイコンを読み込むよう、アイコンのURLを置換する処理をヘッダに加えた Before After 設定 -> [ブログタイトル] -> 設定 -> 検索エンジン最適化 -> headに要素を追加 に以…

やっぱりMacに無変換がほしい

Mac

F7 や Control + K は慣れないし遠くない? やっぱりWindows離れできず、 普段は英数キー 全角入力中に英数キーで無変換 として使えるように設定した。 1. 英数キーをF13にマッピング KarabinerElementsを使った GitHub - tekezo/Karabiner-Elements: The ne…

MacBook Pro開封

愛用のゲーミングノートPCのネジ穴が潰れてネジが外れ、仕方なくACアダプタの差し込みでネジの代わりをすることとなり、持ち運びが大変となったため1年と数ヶ月前に購入して部屋の奥に封印していたMacBook Proを開封しました! 届いて1年経ってようやく開封 …