HACK TO THE FUTURE 2023 予選(AtCoder Heuristic Contest 016)

HACK TO THE FUTURE 2023 予選(AtCoder Heuristic Contest 016) - AtCoder に参加しました。暫定49位でした。 解法 εが小さいときは前計算して埋め込んだグラフを使って、編集距離の最も近いものを答えとして出力する εが大きくてMが小さいときは、辺の数…

estie プログラミングコンテスト2022(AtCoder Heuristic Contest 014)

estie プログラミングコンテスト2022(AtCoder Heuristic Contest 014) に参加しました。暫定6位、最終4位でした。久しぶりに上位に入った気がする。 解法の中でやったこと 初期解 貪欲法で初期解を作る。以下の 5 通りの評価値それぞれで解を作って一番ス…

Topcoder Marathom Match 126

Topcoder Marathom Match 126 に参加しました。ひさしぶりに MM で非自明なことをした気がする。 概要 グリッド上にいくつかのブロックと穴が配置されている。ブロックには 1 から C までの数値が割り当てられている。ブロックに対して以下の操作ができる。 …

AtCoder Heuristic Contest 001

https://atcoder.jp/contests/ahc001 に参加しました。凡ミスをして暫定22位から最終77位に下がったので反省をします。 反省 こんな感じの処理を書きました。 for (int maxsize = 1000; ; ) { Rectangle rect = random_rect(maxsize); if (rect.area() > r[i…

TopProver Sprint Round 13

A. Flat CPO Definition task := forall (x y : option nat) (n : nat), x = Some n -> x = y \/ x = None -> x = y. x = y \/ x = None について場合分けするのが簡単です。x = y の場合は自明で、x = None の場合はもう一つの仮定 x = Some n と合わせると…

TopProver Sprint Round 10

A. Swap Twice Definition swap (t : nat * nat) := match t with (a, b) => (b, a) end. Definition task := forall t, swap (swap t) = t. 組を左右を入れ替える関数 swap が定義されていて、それを二回やると元に戻ることを示せという問題です。 t が必ず…

第5回 Asprova プログラミングコンテスト

https://atcoder.jp/contests/asprocon5 に参加しました。第4回同様焼き鈍しじゃないことをしたいなーと思いながら考えたんですが、結局焼き鈍しをしました。でも焼き鈍し部分にはまだだいぶ改善の余地がありそうな状態だったので(具体的にどこに改善の余地…

Dijkstra 法の納得感のある説明について考えている

以前からときどき考えています。完成はしていません。基本的には距離の短いほうから探索するだけだと思うので、それを典型的な DP っぽく書いてみます。dp[v][d] := 頂点 v までの距離がちょうど d の walk が存在するかどうかとしてみます。都合で path で…

第4回 Asprova プログラミングコンテスト

https://atcoder.jp/contests/asprocon4 に参加しました。今回の問題設定で最初に思いつく方針は第3回同様焼き鈍しなんですが、最近焼き鈍し以外の方法を試したい気持ちがあったので別の方針を考えていたらうまくいきませんでした。それで結局残り時間が少な…

ヤマト運輸プログラミングコンテスト2019

https://atcoder.jp/contests/kuronekoyamato-contest2019 に参加した。登録してないと問題文が読めないみたいですが。 問題1 クエリ数がまあまあ多いので全点対間最短距離だと思い、有向グラフを作って Warshall-Floyd をした。頂点数 2000 ぐらいにしかな…

第3回 Asprova プログラミングコンテスト

第3回 Asprova プログラミングコンテストに参加しました。1位だったようです。最後にパラメータをいじって数回提出したら900万点ぐらい上がってしまった結果なので、3位から上のスコアに本質的な差を感じられず、その点は運がよかったなあという感想になりま…

Marathon Match 107

マラソンマッチ始めてみました。問題文 問題概要 縦 H 横 W のグリッドがあります。各マスに 9 以下の非負整数が書いてあります。マスのいくつかを塗って、塗られたマスに書いてある数の合計を大きくしてください。ただし 縦 h 横 w のどの長方形も塗られた…

Asprova コンテストに参加した

年末年始は Asprova Programming Contest をやってました。なんか問題文が軽い気持ちで読むには重すぎる感じなのですが,短くまとめると いくつかの設備を備えた工場があり,そこでいろんな製品を生産しています 各製品はいくつかの工程を経て完成します 各…

二分探索

二分探索は,値の探索に使うという認識が一般的だと思いますが,実際にはもっと守備範囲が広いです。ということでなるべく一般的な形で書くとどうなるのかを整理した話を書いてみることにしました。why3 で書いて正しいことを検証してみたらけっこうすっきり…

最短距離と自由豊穣圏

距離空間は豊穣圏であるという Lawvere の論文(http://www.tac.mta.ca/tac/reprints/articles/1/tr1abs.html)がありますが,それに似た感じで重みつきグラフから自由に生成された豊穣圏を考えると hom-object が最短経路になるらしいことに気付いて面白いと…

Z/nZ の分解周りのメモ

と書いたとき中国剰余定理として知られる同型 の具体的な与え方が毎回思い出せないのでどこかに書いておきたいと思ってメモ。ついでに単数群の生成元も。 同型 は単純にそれぞれの成分に射影すればよい。逆が少しややこしくて, となる。mod q_i での逆元は…

Graphillion で半順序の個数を数えてみた話

Graphillion で遊んでみた。 やったこと 有限集合上の半順序の個数を数えてみた(cf. OEIS A001035)。これを効率的に求めるのは未解決問題らしい。ちなみに有限集合上の位相の個数を数える問題とだいたい同じ。要素数 n を固定して,Graphillion を使って [1.…

Emacs 上でカーソル位置にある文字の T-Code での入力方法を勝手に表示する

Emacs で日本語を入力するときに T-Code を少し使ってるのですが,ある文字の打ち方を知りたいときにわざわざ 55 って打つのがめんどくさいのでカーソルを合わせたら勝手に表示されるようにしたいとずっと前から定期的に思っていて,今日も思ったので40分く…

関数のオーダーの上の順序と足し算

https://twitter.com/yoshihiro503/status/920979507053412353 から始まってなんか議論になっている感じだったのを見て,ちょっと考えてみた話.要するに,関数のオーダー全体の集合は自然な順序が入って join-semilattice になる.あと足し算もできる(実は…

真空中を音が伝わる速さ

「真空中を音が伝わる速さはおよそ 340m/s である」という主張は正しいか正しくないかということを,ちょっと前に道を歩いていたらふと気になって考え始めたことがあって,そのことを今日思い出したので記録。まず大前提として,真空中を音が伝わることはな…

数学は可能な限り一般的であるべきか

ある論文を読んでいて,「集合 X の部分集合族 K が与えられたとする。このとき〜」と書いてあって,その後には K を用いた概念が定義されているのだけど,その部分を最後まで読んでも何を意図しているかよくわからなかった。もっと先を読んでみると,どうや…

Implicit argument が絡んで型検査を通らない例

型検査(推論?)がうまくいってもよさそうだけどうまくいかない話です.挙動は Coq 8.5pl2 で確認しました.他のバージョンでどうかは調べていません.Set Implicit Arguments してから,なんか依存型を定義します. Coq < Set Implicit Arguments. Coq < I…

かたい電車

15分間隔で電車が走っている路線でA駅からB駅へ向かい,その後30分間隔で電車が走っている路線に乗り換えてC駅に行くことを考える.A駅でいつもより一本(つまり15分)早い電車に乗るとどうなるか.おそらくB駅における乗り換えでいつもより15分長く待って,…

ホーア論理の代入の規則

わりとわかりにくくて混乱しやすい気がするホーア論理の代入の規則ですが,見方を少し変えるとわかりやすくなります。普通の規則。同値変形してこうする。要するに「代入後の x の値を x' とすれば A[x'/x] である」が事前条件です。Hoare triple の意味を考…

数学の本の話

数学の本はアウトラインがわかればあとは自分でよく考えるだけで本を閉じたまま詳細を構成することができる。しかし数学以外の本はそうとは限らない。例えば歴史の本は歴史の大まかな流れがわかっていても細部を自分の頭で考えても埋めることはできない,気…

Hilbert algebra の性質の証明

ちょっと気になってやってみたのをどこかにメモしたくなったので書いた。関数解析じゃなくて論理の方の Hilbert algebra です。 Hilbert algebra の公理 が Hilbert algebra とは if then 性質 で順序が入り,1 が最大元 などが成り立つ。証明は下に書くけど…

resolution の完全性についての疑問

一階述語論理の resolution の規則って, として を の MGU としたときに と書けて(resolution に を使うのはあまり普通ではないかもしれないけど),これだけで反駁完全なのだと思っていました。しかしどうもそうではないようだという気がしてきて,どうやっ…

ダウンロードしてみた本リスト

先日 Springer でいろいろな本が無料ダウンロードできるようになっていた。今はもうできなくなったらしい。どういうことだったのかはよく分からない。twitter を見ても,よく分からないと言っている人がたくさんいる。何冊か落としたのでメモ。 Marker, Mode…

contraction がいらないシーケント計算

「論理と計算のしくみ」を読んでいたら,シーケント計算の推論規則を ∧右,∨左,⊃左は additive ∧左,∨右 は multiplicative にすると命題論理では contraction が不要になるということを知りました。こういう組み合わせは証明論的にはだいぶ気持ち悪いよう…

Awodey 本の訳に変なとこがある

Awodey 本の邦訳について,訳の質が低いという趣旨のレビューがついています。自分で確認したわけではないのですが,このレビュアーの書いていることを信じるならば,確かにあまり丁寧に訳されてはいないようだという印象は受けます。そこに挙げられている点…