System FをRocq (Coq)で示そうとして結局断念した話。

支援証明系辛すぎます…引退です…自然言語による証明のありがたさが良く沁みました。

TaPLを読み進めていて、せっかくなら支援証明系も触ってみようということで、各章の主定理をRocq(Coq)で順番に示していこうとしたのですが、 23章のSystem Fで詰まって断念しました。以下に理由を書きます。

代入の扱いが大変すぎる

支援証明系でキッチリ証明しようとすると、α変換を正しく扱うのが難しいです。人間ならλ式の変数くらい"適当"に変えればよいで伝わりますが、機械にはどう取るかを指定しなければなりません。 なのでDe-Bruijn列で証明しようとしたのですが、これもまた大変で、シフトに関する補題を大量に証明しないと行けなくなります。人間だとお気持ちで伝わるところが、機械だと全く通じないので、 丁寧な不等式の設定+場合分けで示さないといけないのが非常に煩雑です。

そもそも正しい定義/命題を書くことが難しい

TaPLだと自由変数の扱いがあまり具体的に書いておらず、そこを正しく命題に書き表すのが難しいです。また型変数の束縛も本の注釈に大事なことが書かれていたりするので、見落とすとドツボにはまります。

同じ証明の繰り返しになる

項を項に代入、型を型に代入、型を項に代入するの3つの代入があるので、それぞれ命題を示さなければなりません。ここは工夫が聞くんじゃないかと思っているのですが、自分の証明方法では 煩雑になってしまいました。

あんまり完全な証明を与えるモチベーションがなくなってしまった。

書き直しを何度かして、何となく各命題が回り始めたので、「ああ正しく命題と定義を設定できてそうだな」となってからモチベーションが落ちてしまいました。証明の完成が近づくにつれて、 成り立つことがかなり自明に見えるが証明が面倒臭い命題が残っていって、やりたくない、あんまり意味がないという気持ちが強くなりました。

一応これで供養という事にします...自分は公開されているGithubで23章の進行保存定理を完全に示せているレポジトリは見たことがないので、是非チャレンジしてみてください。

github.com

二階命題論理の存在量化子を全称量化子で書き換える

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 H0 in H.
- intros. apply H. intros. now exists X. Qed.

ARC152D Halftree

D - Halftree

意外とこの解き方している人が少ないように見えたので。

例えば入力が7 3の場合は
(0,1)(1,2)(2,3)
と辺を張れば0~6の線グラフが得られることが分かると思います。
9 3の場合は頂点7, 8が残ってしまいますが、(7,5)と辺を張ることで、線グラフ+αの形で木が構成できます。
このように、できるだけ線グラフで構築して、残った頂点を適当に線グラフにつなげれば良いです。

提出

2023年の振り返りと2024年目標

修士を修了

特に問題なく、スムーズに卒業できたし、得られた結果も個人的には満足できるものでした。国際会議(といっても査読がすごく厳しいところではない)に出したり、arXivに投稿したりして、当時の自分はそれでいっぱいいっぱいになっていたけど、今見返してみると、アラがあったりして、他人に引用してもらえるようなものではなかったのかなと反省しています。

入社

某外資系ソフトウェアエンジニアになりました。一応業務内容はこなせている気がしますが、コミュニケーション能力だったり、バグを報告/修正するというエンジニアとしてのマインドはまだ足りていないと痛感しています。あと同僚の思考スピードについていけていない気がするので、知識を体系化するか、または物事の考え方について考えを改めないといけないかもなと思っています。

趣味

4-6月に圏論、6月からは型システム入門をCoqで進めていました。圏論はAlg-dさんのサイト 圏論 | 壱大整域で学びました。あんまり学部/修士時代、プログラミングの基礎論に興味がなかったのですが、いざやってみると結構面白かったです。引き続き続けていきたいと思います。

目標

仕事: "エンジニアマインド"を身に着けるにします。そうすれば自然とアウトプットが増えるんじゃないかなと願っています。後シンプルに社会人として無理のないまともな生活を送りたいです。
趣味: HaskellとRustに入門するにします。

yukicoder: No.1062 素敵なスコア

https://yukicoder.me/problems/no/1062

A\lt Bとします。
K以下の要素を黒丸、 Kよりも大きい要素を白丸で表すことにすると以下のような状況になります。


このうち操作を行った後も同じ要素になるindexは以下の黒枠で囲った部分になります。



このように P,Q両方でswapされずに同じ要素になるindexと、両方でswapされて同じ要素になるindexがあることがわかります。前者の総数は解説にあるように (X^2+Y^2+Z^2) (N-1)!となります。
後者の総数を Sとして、 Sを求めることを考えます。
各index (1 \leq i \leq X)で S_i=( P_i,Q_i両方で白丸で、操作で黒丸とswapされて P_i=Q_iとなる数列の総数)が求まれば、 S=2\sum_{i=1}^X S_iとなります。係数が2の理由ですが、○○がswapされる先は●●なので、 P_i,Q_i両方で黒丸のindexも同数だけあるからです。

S_iの状況は以下のようになります。



これを、


こうじゃ。

なので、 S_i=(後半に●●i個、前半に○●Y個と●●X-i個を好きなように並べた列に○○Z-1個を挿入した列の総数) =X!Y!Z! \times {}_{Y+X-i}C_{Y}\times {}_{N-1}C_{Z-1}となります。よって、

S=2X!Y!Z! \times {}_{N-1}C_{Z-1} \sum_{i=1}^X {}_{Y+X-i}C_{Y}=2X!Y!Z! \times {}_{N-1}C_{Z-1} \sum_{i=0}^{X-1} {}_{Y+i}C_{Y}

ですが、経路数を少し考えると

\sum_{i=0}^{X-1} {}_{Y+i}C_{Y}={}_{X+Y}C_{X-1}

であることがわかるので、 S=2X!Y!Z! \times {}_{N-1}C_{Z-1} \times {}_{X+Y}C_{X-1}=\frac{2XZ}{Y+1}(N-1)!となります。
前半パートと合わせれば答えは (X^2+Y^2+Z^2+\frac{2XZ}{Y+1})(N-1)!です。 

#include <bits/stdc++.h>
using namespace std;
typedef long long ll;
const ll mod = 998244353;

int N, A, B;

int main() {
    cin >> N >> A >> B;
    if(A > B) swap(A, B);
    ll x = A, y = B - A, z = N - B;
    ll fac = 1, nfac = 1;
    for(int i = 1; i <= N - 1; i++) {
        fac = fac * i % mod;
        if(i != y + 1) nfac = nfac * i % mod;
    }
    cout << ((x * x % mod + y * y % mod + z * z % mod) * fac 
            + 2 * x * z % mod * nfac) % mod << endl;
}

Codeforces Round #616 (Div. 1)

https://codeforces.com/contest/1290

ダメダメだったため、撤退…あとでちゃんと復習します。

A
勘違いして変な条件で考えてしまいました…詰めるのもめちゃくちゃ遅かった。例によって条件を整理しきらずに紙に頼ってしまった。

B
adhocだと思えば解けたかもしれない…

C
解説みたらライトを辺と置き換える言い換えすらもできてなかった。(ライトを頂点とした2部グラフで見てた。)
でも解けそうな気はしたが…

codeforcesの問題、ちゃんと考察にadhocな点が1つ2つあって、実装もまあまあ重い感じなんだよな。
AtCoderはadhocに振り切れればいいけど。失敗しているときはだいたい考察が足りてないときではある気がする。頭を動かしましょう。

AOJ2445: MinimumCostPath

http://judge.u-aizu.ac.jp/onlinejudge/description.jsp?id=2445

N<400の時は愚直に求めることにします。
N>=400の時は、
左下、右上の100x100領域に注目します。
(0,0)->(左下の領域)->(真ん中の領域)->(右上の領域)->(N-1,N-1)と移動していくことになりますが、
真ん中の領域では必ず右または上のみの移動になります。

これを証明するためには、任意の経路を経路長を伸ばすことなく、真ん中の領域で右または上のみ移動する経路に変換できることを示せばよいです。
左下の領域から初めて出た場所を(x,100)とします。対称性より(100,y)の時も同様です。
0<=y<100において、障害物がない行が必ず存在します。その行を通って左下の領域から出ると、右または上のみの移動で、右上の領域に入ることが出来ます。
このとき経路長は伸びません。

この事実により、左下の領域から出た座標と右上の領域に入った座標について、最短経路の本数を求めれば良くなり、これは
https://atcoder.jp/contests/dp/tasks/dp_y
です。最後に通った障害物で包除する感じです。

int dx[4] = {1, -1, 0, 0};
int dy[4] = {0, 0, 1, -1};

int N, M;
int X[110], Y[110];
int B[510][510];
ll D[510][510];

void pre(int l, int r, int x, int y) {
	int n = r - l;
	rep(i, 0, n) {
		rep(j, 0, n) {
			B[i][j] = inf;
		}
	}
	rep(i, 0, M) {
		if(l <= X[i] && X[i] < r && l <= Y[i] && Y[i] < r) {
			B[X[i] - l][Y[i] - l] = -1;
		}
	}
	memset(D, 0, sizeof(D));
	x -= l;
	y -= l;
	queue<pi> que;
	que.push(pi(x, y)); 
	B[x][y] = 0;
	D[x][y] = 1;
	while(!que.empty()) {
		pi p = que.front(); que.pop();
		rep(i, 0, 4) {
			int nx = p.fst + dx[i], ny = p.sec + dy[i];
			if(0 <= nx && nx < n && 0 <= ny && ny < n && B[nx][ny] != -1) {
				if(B[nx][ny] >= B[p.fst][p.sec] + 1) {
					ADD(D[nx][ny], D[p.fst][p.sec]);
					if(B[nx][ny] > B[p.fst][p.sec] + 1) {
						B[nx][ny] = B[p.fst][p.sec] + 1;
						que.push(pi(nx, ny));
					}
				}
			}
		}
	}
}

ll qre(int x1, int y1, int x2, int y2) {
	vector<pi> vec;
	// debug(x1, y1, x2, y2);
	rep(i, 0, M) {
		if(x1 == X[i] && y1 == Y[i]) return 0;
		if(x2 == X[i] && y2 == Y[i]) return 0;
		if(x1 <= X[i] && X[i] <= x2 && y1 <= Y[i] && Y[i] <= y2) vec.pb(pi(X[i], Y[i]));
	}
	vec.pb(pi(x1, y1));
	vector<ll> dp(sz(vec), 0);
	sort(all(vec));
	rer(i, sz(vec), 0) {
		int a = vec[i].fst, b = vec[i].sec;
		dp[i] = C(x2 - a + y2 - b, x2 - a);
		rep(j, i + 1, sz(vec)) {
			int c = vec[j].fst, d = vec[j].sec;
			ADD(dp[i], mod - dp[j] * C(c - a + d - b, d - b) % mod);
		}
	}
	return dp[0];
}

void solve() {
	int bound = 100;
	cin >> N >> M;
	C_init(2 * N);
	rep(i, 0, M) {
		cin >> X[i] >> Y[i];
		X[i]--; Y[i]--;
	}
	if(N < 400) {
		pre(0, N, 0, 0);
		cout << D[N - 1][N - 1] << "\n";
	}
	else {
		vector<pair<pi, pl>> vl, vr;
		pre(0, bound, 0, 0);
		rep(i, 0, bound) {
			if(B[i][bound - 1] != -1)
			vl.pb(make_pair(pi(i, bound), pl(B[i][bound - 1] + 1, D[i][bound - 1])));
			if(B[bound - 1][i] != -1)
			vl.pb(make_pair(pi(bound, i), pl(B[bound - 1][i] + 1, D[bound - 1][i])));
		}
		pre(N - bound, N, N - 1, N - 1);
		rep(i, 0, bound) {
			if(B[i][0] != -1)
			vr.pb(make_pair(pi(N - bound + i, N - bound - 1), pl(B[i][0] + 1, D[i][0])));
			if(B[0][i] != -1)
			vr.pb(make_pair(pi(N - bound - 1, N - bound + i), pl(B[0][i] + 1, D[0][i])));
		}
		ll md = inf;
		rep(i, 0, sz(vl)) {
			rep(j, 0, sz(vr)) {
				ll v = vl[i].sec.fst + vr[j].sec.fst + (vr[j].fst.sec - vl[i].fst.sec) + (vr[j].fst.fst - vl[i].fst.fst);
				MIN(md, v);
				// debug(v, vl[i], vr[j]);
			}
		}
		// debug(md, vl, vr);
		ll res = 0;
		rep(i, 0, sz(vl)) {
			rep(j, 0, sz(vr)) {
				if(md == vl[i].sec.fst + vr[j].sec.fst + (vr[j].fst.sec - vl[i].fst.sec) + (vr[j].fst.fst - vl[i].fst.fst)) {
					ADD(res, vl[i].sec.sec * vr[j].sec.sec % mod 
							* qre(vl[i].fst.fst, vl[i].fst.sec, vr[j].fst.fst, vr[j].fst.sec) % mod);
				}
			}
		}
		cout << res << "\n";
	}
}

2パートあるだけで実装辛くなる…