diff --git a/.github/workflows/format-tex.yaml b/.github/workflows/format-tex.yaml
new file mode 100755
index 00000000..5de8327d
--- /dev/null
+++ b/.github/workflows/format-tex.yaml
@@ -0,0 +1,18 @@
+name: format-tex
+
+on: [push, pull_request]
+
+jobs:
+  format-tex:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: Install Dependencies
+        run: |
+          sudo apt install chktex
+
+      - name: Run chktex
+        run: |
+          chktex --nowarn={1,2,8,11,12,13,36,39} docs/*.tex
diff --git a/README.md b/README.md
index 57754179..df1d73a9 100644
--- a/README.md
+++ b/README.md
@@ -67,9 +67,7 @@ For users:
 For developpers:
 
 - [CONTRIBUTING.md](https://github.com/kmyk/Jikka/blob/master/CONTRIBUTING.md)
-- My blog article [競技プログラミングの問題を自動で解きたい - うさぎ小屋](https://kimiyuki.net/blog/2020/12/09/automated-solvers-of-competitive-programming/) (Japanese)
-  - On what it means to automatically solve problems of competitive programming / 競技プログラミングの問題を自動で解くとはどういうことなのかについて
-- [docs/how-it-works.pdf](https://github.com/kmyk/Jikka/blob/master/docs/how-it-works.pdf) (Japanese)
+- [docs/how-it-works.pdf](https://github.com/kmyk/Jikka/blob/master/docs/how-it-works.pdf) / [docs/how-it-works.ja.pdf](https://github.com/kmyk/Jikka/blob/master/docs/how-it-works.ja.pdf)
   - How it works and related theories / 動作原理や関連する理論
 - [docs/DESIGN.md](https://github.com/kmyk/Jikka/blob/master/docs/DESIGN.md)
   - The policy of designs / 実装方針
@@ -80,6 +78,11 @@ For developpers:
 - [Haddock](https://hackage.haskell.org/package/Jikka)
   - [Haddock (master)](https://kmyk.github.io/Jikka/haddock)
 
+Blog articles:
+
+- [競技プログラミングの問題を自動で解きたい - うさぎ小屋](https://kimiyuki.net/blog/2020/12/09/automated-solvers-of-competitive-programming/) (Japanese)
+- [Jikka, a transpiler/solver for competitive programming - Codeforces](https://codeforces.com/blog/entry/94648)
+
 ## Examples
 
 ### `examples/fib.py` (`v5.0.5.0`)
diff --git a/docs/how-it-works.ja.pdf b/docs/how-it-works.ja.pdf
new file mode 100644
index 00000000..42bd1889
Binary files /dev/null and b/docs/how-it-works.ja.pdf differ
diff --git a/docs/how-it-works.ja.tex b/docs/how-it-works.ja.tex
new file mode 100644
index 00000000..ee2dee87
--- /dev/null
+++ b/docs/how-it-works.ja.tex
@@ -0,0 +1,564 @@
+\documentclass{ltjsarticle}
+
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{amsthm}
+\usepackage{braket}
+\usepackage{colortbl}
+\usepackage{ebproof}
+\usepackage{enumitem}
+\usepackage{here}
+\usepackage{latexsym}
+\usepackage{lscape}
+\usepackage[linguistics]{forest}
+\usepackage{mathtools}
+\usepackage[pdfencoding=auto]{hyperref}
+\usepackage{tikz}
+
+% \usepackage{bibentry}
+% \nobibliography*
+
+\newtheorem{problem*}{問題}[section]
+\newenvironment{problem}{\begin{problem*}\renewcommand{\qedsymbol}{\(\diamond\)}\pushQED{\qed}}{\popQED\end{problem*}}
+\newtheorem{definition*}{定義}[section]
+\newenvironment{definition}{\begin{definition*}\renewcommand{\qedsymbol}{\(\diamond\)}\pushQED{\qed}}{\popQED\end{definition*}}
+
+
+\title{競技プログラミングの問題を自動的に解きたい}
+\author{Kimiyuki Onaka}
+\date{\today}
+
+\begin{document}
+\maketitle
+
+\setcounter{section}{-1}
+\section{概要}
+
+この PDF では「競技プログラミングの問題を自動的に解けるか？」という問いについて考える。
+あるいは「競技プログラミングのソルバを作ることはできるか？」と言い換えてもよいだろう。
+
+$1$ 章ではこのまだ曖昧な問いをより具体的な問いへと整理する。
+競技プログラミングの問題を自動的に解くソルバにも様々な種類のものがあることを説明し、今回我々が作成を目指すソルバがそれらの中のどの種類のものかを明確にする。
+我々が作成を目指すのは「形式的に表現された問題を受け取り、それに対する解答を出力する」という種類のものであり、その中でも特に「形式的に表現された問題」として「愚直解のソースコード」を用いるものである。
+そのようなソルバはつまり「漸近的計算量のレベルの最適化を伴うトランスパイラ」である。
+よって「競技プログラミングのソルバを作ることはできるか？」という問いは「漸近的計算量のレベルの最適化を伴うトランスパイラは作れるか？」という具体的な問いとなる。
+また、より実用的には、完全なソースコードでなく小さなコード片を入力とする「漸近的計算量のレベルの最適化を行う IDE プラグイン」としても利用できると扱いやすいであろう。
+
+$2$ 章では具体化された問いに対する暫定の答えを与える。
+つまり、最適化を伴うトランスパイラとしての競技プログラミングのソルバの実装方針を説明し、またそのような方針で実装されたソルバでいくらかの問題が解けることを見る。
+実装方針は機械的な式木の書き換えが中心となる。
+たとえば、愚直に何度も区間和を取っている部分を検出すればそれを累積和で置き換えたり、愚直な 2 重ループで畳み込みをしている部分を検出すればそれを FFT を用いた畳み込みで置き換えたりする。
+このような書き換えは ``rewrite rule'' と呼ばれる規則として表現され、よってソルバの中心部分は「rewrite rules からなる集合」として実装される。
+
+\section{競技プログラミングの問題を自動的に解くとはどのようなことか}
+
+\subsection{そもそもなぜ競技プログラミングの問題を自動で解きたいのか}
+
+まず先に、「競技プログラミングの問題を自動的に解けるか？」という問いの意義について述べておこう。
+なぜ競技プログラミングの問題を自動で解きたいのだろうか？
+これは主には以下の 3 種類であろう。
+
+\begin{enumerate}[label=(\arabic{enumi}.)]
+    \item 競技プログラミングでの実用: 「コンテスト中の作業を自動化してレートに繋げたい」「ソルバの実行ログが学習用途に使えるかもしれない」など
+    \item 工学的な興味: 「どの程度の問題までなら自動で解けてしまうのか知りたい」など
+    \item 哲学的な動機: 「問題が手動でなら解けても自動では解けないなら、本当に解けたとは言えないかもしれない」「人間がどのようにして問題を解いているのかについて理解を深めたい」
+\end{enumerate}
+
+(1.) 競技プログラミングでの実用は分かりやすい。
+簡単な問題や難しい問題の部分問題を手動でなく自動で高速に解いてしまえるなら、難しい問題の難しい部分に時間を使うことができてコンテストで有利である。
+もし自分では解けない難しい問題がソルバによって解けるならなおさらである。
+レートに影響がなくとも、簡単な問題を自動化してしまえるなら便利で楽であろう。
+
+また、教育や学習用途でソルバを使うことができるかもしれない。
+ソルバが問題を解く過程を詳細に分かりやすく出力すれば、初心者はそれを読んで問題の解き方を学ぶことができるだろう。
+
+(2.) の工学的な興味も分かりやすい。
+単純に、どの程度の問題までなら自動で解けてしまうのか (そしてどのような問題は自動では解きにくいか) を知れれば面白い。
+
+(3.) は哲学的な動機である。
+我々は競技プログラミングの問題を手動で解くことができる。
+それはいったいなぜだろうか？
+問題を解く方法を具体的なアルゴリズムとして説明できるだろうか？
+それができないのに「競技プログラミングの問題を解くことができる」と言い切ってしまってよいのだろうか？
+
+たとえば、普通に競技プログラミングをしている人が「ある問題が頭の中では解けました。しかし実装方法については検討も付きません」と発言しているとしよう。
+ある程度競技プログラミングをやったことのある人であれば、そのような発言に対しては「解けたつもりになっているのが間違いで、そんな状況のことを解けたとは言わない」と思うだろう。
+つまり、みな「問題が解けたならば実装できるはずだ」と信じているのである。
+これと似た別の状況を考えてみよう。
+「ある問題が解けて実装もできた。しかしなぜ私にこれが解けたのかはよく分からない」という状況である。
+このような状況もやはり「その問題に対する理解が足りていない」とみなされることが多いだろう。
+理解が足りていないままであれば、もしその問題の類題が出題されたときそれを解けないかもしれない。
+「問題の解法を正しく理解できたなら、その解法に至る道筋を説明できるはずだ」と信じている人は多いはずである。
+これらの観察からは次のことが疑われる。
+つまり「競技プログラミングを十分に理解しているならば、そのソルバも実装できるはずである」。
+ソルバを実装しようとしてみることは競技プログラミングへの理解に貢献するだろう。
+
+これはさらには、より一般の人間の思考についての問い、つまり「考えるとはどのようなことか」を考えることにも繋がってくる。
+たとえば、機械的な規則の適用をくり返すことで実装されたソルバがもし人間に匹敵するような成功を収めたとすれば、そこから人間の思考も結局は規則の機械的な適用を素早く行っているだけではないかと疑うことができる。
+あるいは逆にそのようなソルバがまったく失敗してしまうなら、人間の思考には機械的な規則の適用としては捉えきれない暗黙的な部分があることが疑われる。
+
+
+\subsection{競技プログラミングの問題を人間はどのように解いているのか}
+
+「競技プログラミングの問題を解く」と言っても、その範囲は意外に広い。まずこれを整理するところから初めよう。
+競プロの問題のページが開かれた直後の状態 (たとえば \url{https://atcoder.jp/contests/abc184/tasks/abc184_c} というリンクをクリックした直後のような状態) から初めて、緑色の「AC」という表示を確認するまでの過程において、具体的にはどのようなステップがあるだろうか？
+もちろんこの過程には様々なものが含まれており (例: 「問題文中に埋め込まれている図を解釈する」「問題ページをスクロールする」「青い ``提出'' と書かれたボタンをクリックする」など) いくらでも細かく説明できてしまう。
+しかし、重要でないものを無視して抽象的な形で整理すると、通常の過程は次の 3 ステップにモデル化できるだろう。
+
+\begin{description}
+    \item[(1.) 読解] 自然言語で与えられた問題を解釈し、数学的な問題として整理する
+    \item[(2.) 考察] 数学的な問題に対し、数学的な解法を考案する
+    \item[(3.) 実装] 数学的な解法を、計算機上の具体的な実装として記述する
+\end{description}
+
+順番に見ていこう。
+(1.) は (人間にとっては) 自明なのであまりかえりみられることのないステップである。
+このステップでは、日本語や英語で書かれた問題を読み、数式などで表現された問題として整理し理解する。
+たとえば「熊の Limak が人間の高橋くんに合いに AtCoder 王国を訪れている。
+AtCoder 王国は $1$ から $N$ までの番号の付いた島と、それらの間にかかる $M$ 本の橋からなる。
+今 Limak は $s$ 番目の島にいて、高橋くんは $t$ 番目の島にいる。
+そして……」のような問題文を読んで理解し、不要な情報を捨象して「$N$ 頂点無向グラフ $G = (V, E)$ と $s, t \in V$ が与えられる。……」のような問題であることを確認する。
+
+(2.) は競技プログラミングにおいて最も難しくかつ面白いとされるステップである。
+このステップでは、(1.) で理解した問題に対し、実行時間などの制限を満たす解法を考案する。
+たとえば、考察の結論として「まず重み付きグラフ $G = (V, E, w)$ とすべての頂点 $x \in V$ に対し $s-x$ 最短路を $s$ からの Dijkstra 法で求める。
+次に重み付きグラフ $G' = (V, E, w')$ とすべての頂点 $x \in V$ に対し $t-x$ 最短路を $t$ からの Dijkstra 法で求め、そして……」などのアルゴリズムが得られる。
+
+(3.) はジャッジサーバによる自動採点のために必要なステップである。
+このステップでは、(2.) で得たがまだ頭の中にある抽象的なアルゴリズムを、計算機上の具体的なコードへ翻訳する。
+たとえば「$s-t$ 最短路を Dijkstra 法で求めればよい」というときには、C++ なら
+\verb|priority_queue<pair<int64_t, int>> que; que.emplace(0, s); while (not que.empty()) …|
+のようなコードが書かれるだろう。
+
+そして、今回の話題は (2.) の「考察」のステップである。
+このステップは競技プログラミングという行為において中心となるステップであり、「問題を解く」と言うときも主にこのステップに注目している。
+つまり「競技プログラミングの問題を自動で解きたい」とは「考察を自動で行いたい」ということである。
+
+
+
+\subsection{競技プログラミングのソルバは形式化を人間に任せるとよいだろう}
+
+競技プログラミングの問題を解くことを「読解」「考察」「実装」という 3 ステップに分けた上で主に「考察」を行いたいのだと言っても、残りのふたつのステップは容易に切り離せるものではない。
+問題は何らかの形で入力されねばならないし、解法は何らかの形で出力されねばならない。
+「読解」「実装」という残りのステップについても扱える必要がある。
+
+機械にとって最も面倒なのは「読解」だろう。
+自然言語の理解という高度な処理が必要になる。
+競技プログラミングの問題文を以降のステップに支障がでないように読み取るには、表面的に単語を追うだけではおそらく足りず、文章全体の意図を正しく把握する必要があるだろう。
+競技プログラミングの問題文以外は理解できなくてよいのだとしても、これはかなり困難である。
+そしてこの「読解」は今回やりたいことではない。
+ソルバの一部として取り扱うのは諦めて、人間 (あるいは GitHub Copilot のような言語モデル) に任せてしまうべきだろう。
+
+「実装」もそのままの形では機械では扱えない。
+「数学的な解法を、計算機上の具体的な実装として記述する」と言うときの「数学的な解法」などは、(通常の人間による競技プログラミングにおいては) 人間の頭の中のみ存在するものだからである。
+人間の頭の中にしかないものは機械には扱えない。
+「数学的な解法」でなくて「数学的な問題」の場合も同様である。
+
+一方で、機械で扱える形に形式化したものが入力であれば「実装」も機械に可能である。
+このことはコンパイラを思い出せば分かる。
+F\# や Haskell のような高級言語のソースコードを仮想機械の中間言語や実際の機械語に変換する操作はまさに「実装」であろう。
+
+よって、ソルバを用いて競技プログラミングの問題を解くとすると、その過程は以下のような 4 ステップに整理されるだろう。この形であれば可能性はある。
+
+\begin{description}
+    \item[(1.) 読解] (人間が) 自然言語で与えられた問題を解釈し、数学的な問題として整理する
+    \item[(2.) 翻訳] (人間が) 数学的な問題を、機械上に形式化された問題として入力する
+    \item[(3.) 考察'] (ソルバが) 記述された形式化された問題に対し、機械的に解法を計算する
+    \item[(4.) 実装'] (ソルバが) 計算された解法を、具体的な実装として出力する
+\end{description}
+
+(1.) と (2.) は合わせて「形式化」をしている。
+これらのステップはどちらも人間にとっては簡単である。
+「読解」のステップが簡単であるのは認めてよいだろう。
+「翻訳」のステップも人間にとっては簡単だとしてよい。
+ただ読んだままを書けばよいためである。
+まったく理解できない難しい数式であってもそれを LaTeX で打ち込むだけならそれほど難しくないことがたいていだろうが、これと同じようなものである。
+
+競技プログラミングのソルバが (1.) と (2.) のステップによる「形式化」を人間に任せてしまったとして、そのような条件で残りのステップだけを処理した場合も「競技プログラミングの問題を自動で解けた」と言ってよいだろうか？
+これは「自動で解けた」と言ってしまってよいだろう。
+なぜなら、「形式化」は (機械にとっては難しいとはいえ) 人間にとってはたいてい簡単であるし、通常は重要視されるステップではないからである。
+困難でも重要でもないステップを省略しても、困難で重要な (3.) の「考察'」のステップをうまく扱うのなら「問題を自動で解く」と言ってよいだろう。
+様々なことを自動でしてくれるソフトウェアであってもデータの打ち込みは人間の担当であることは多く、今回もそうだったというだけである。
+
+
+\subsection{競技プログラミングのソルバはトランスパイラの形で実装するのがよいだろう}
+
+ソルバの入力は「形式化された問題」だろうと言ったが、では「形式化された問題」というのは具体的に何にするとよいだろうか？
+$(\text{入力となる変数}, \text{出力となる変数}, \text{それらが満たすべき制約})$ という $3$ つ組だろうか？
+計算可能な関数のグラフだと考えるべきだろうか？
+これはおそらく何でもよい。
+問題を表現できてさえいれば、入力フォーマットの選択によって問題が解けたり解けなかったりするといったことはほぼないだろう。
+好きなものを使えばよい。
+
+しかしソルバへの入力形式はソルバ自体の実装のしやすさを大きく左右する。
+どのような入力にするのがもっとも楽だろうか？
+何度かプロトタイプを実装した経験から、私は「実行可能なプログラム」を「形式化された問題」として使うのがよいと考えている。
+「実行可能なプログラム」をソルバの入力とすれば、競技プログラミングの過程は以下の 3 ステップに具体化される。
+
+\begin{description}
+    \item[(1.) 読解] (人間が) 自然言語で与えられた問題を解釈し、数学的な問題として整理する
+    \item[(2.) 実装''] (人間が) 数学的な問題を、計算機上にその愚直解として実装する
+    \item[(3.) 考察''] (ソルバが) 記述された実装に対し、計算量的な最適化を行う
+\end{description}
+
+このとき (3.) の「考察''」のステップは、入力も出力も共にプログラミング言語である。
+入力されたプログラムと同じ計算をするより高速なプログラムを出力する。
+これは「最適化」に同じである。
+つまり「実行可能なプログラム」をソルバの入力とすれば、「競技プログラミングの問題を自動で解くソルバ」は「最適化を伴なうトランスパイラ」となる。
+
+「競技プログラミングの問題を自動で解くソルバ」を「最適化を伴なうトランスパイラ」と言い換えられた。
+これは大きな進歩である。
+「なにやらよく分からないすごそうなもの」ではなく「いつもの」を書けばよいことになった。
+「人工知能」と比べれば「コンパイラ」はたいへんに開発しやすい。
+既存の技術や資料をたくさん利用できる。
+また、入力と出力のギャップが小さいことも利点である。
+入力をそのまま出力するだけのプログラムでさえ、いまや「自明なソルバ」だと主張できる。
+
+なお、「形式化された問題」として「実行可能なプログラム」使うことは明らかなことではない。
+答えを先に聞くと自然に聞こえるかもしれない。
+しかし思い出してほしいのは、「問題」と「プログラム」はまったく異なるものだということである。
+プログラムは実行できるが、問題は実行できない。
+プログラムは漸近的計算量を持つが、問題は漸近的計算量を持たない。
+少なくとも私はいくつかのプロトタイプを作るまでこのギャップを乗り越えられなかった。
+
+なお、トランスパイラ以外の形のソルバの可能性としては、たとえば「対話的なソルバ」「過去問データベースと検索エンジンからなるソルバ」などが考えられる。
+
+
+
+\subsection{競技プログラミングのすべての問題が自動で解けるわけではない}
+
+言うまでもないことだろうが、競技プログラミングのすべての問題が自動で解けるわけではないことを注意しておく。
+期待しすぎるべきではない。
+機械的な解法と相性の良い問題は解けるだろうが、相性の悪い問題は解けない。
+少なくともしばらくの間は、再翻訳がおもしろおかしいものだった時代の機械翻訳と同程度の有用性がせいぜいのはずである。
+
+特にトランスパイラとしてのソルバについて言えば、相性の悪い問題にはたとえば以下のようなものがある。
+
+\begin{enumerate}[label=(\arabic{enumi}.)]
+    \item 愚直解の実装が難しい問題
+    \item 「直感」や「ひらめき」を必要とする問題
+    \item 問題そのものが複雑な問題
+\end{enumerate}
+
+(1.) は、たとえば幾何の問題である。
+ソルバの担当範囲以外の部分が難しい。
+そのような場合は人間が頑張るしかない。
+考察要素がある問題であってもその考察要素が「愚直に実装するとたいへんだが、うまく工夫すると実装量を減らすことができる」という形であれば、やはりソルバは無力である。
+
+(2.) は、たとえば貪欲法が想定解の問題である。
+ソルバの担当範囲が難しい。
+実装にもよるだろうが、基本的にソルバは 1 歩ずつ考察を詰めていけば解けるような問題しか解けないだろう。
+「証明はできないけどなんとなく正しそう」のような判断は機械とは相性が悪そうである。
+「突然ですが、ここで $x = f(y, g(y, z))$ とおきます。すると……」のような発見的解法も機械とは相性が悪そうである。
+手法によっては扱えるかもしれないが、少なくとも、先程の節で述べたような形の機械的解法で解くことはできない。
+
+(3.) は、たとえばゲームの問題がそうだろう。
+交互ゲームで「先手が必勝である」ことを表現しようと思うだけで、量化子の繰り返しや再帰関数のような扱いにくいものが出てきてしまう。
+きれいな式で表現できないような問題と機械の相性は悪いだろう。
+
+
+
+\subsection{ソルバの実践での利用について}
+
+競技プログラミングのソルバの、それをコンテスト中に利用するユーザから見たときの様子を検討しておこう。
+基本的には現在の\href{https://oeis.org/}{オンライン整数列大辞典} (OEIS) や \href{https://www.wolframalpha.com/}{Wolfram|Alpha} とそう変わらない立ち位置にしかならない。
+
+まず明らかに言えることは、一般にソルバは銀の弾丸にはならないということである。
+もしどんなに優秀なソルバが開発されたとしても、そのようなソルバで解けてしまう問題は出題前に弾かれるだけである。
+ソルバが利用できるとしても、それは実際の問題の部分問題に対してのみであろう。
+また、ソルバですべての問題が解けるわけではないので、ユーザは「問題が自動的に解けるのはどのような場合であるか」を大まかに判断できる必要がある。
+機械的に解けうる問題であっても入力の与え方次第では解けないことも多いので、この判断を行なえることはソルバの利用のために必要である。
+しかしそのような判断ができるには結局はユーザ自身の能力が要求される。
+
+また、「競技プログラミングの問題のソルバ」という形であれば入力は問題そのものでしかありえないのだが、コンテストでの実用を考えたときにはそれ以外の可能性も現れてくる。
+最終的な解法コードのうちでアルゴリズムに本質的に関わる部分はごく一部のみであるので、そのようなコード断片のみを入力とすることもできる。
+すると、そのようなコード断片のみを扱うものはエディタのリファクタリング支援機能の延長に位置するものになる。
+それは「IDE のプラグイン」として実現される。
+ユーザがコード断片を指定すると、その部分の漸近的計算量を落とすなどの書き換えを行ってくれるようなものである。
+入出力がソースコードの全体でなくコード断片という小さいものになれば、結果の解釈や再利用もより柔軟に行えて便利であろう。
+
+
+
+\section{最適化を行うトランスパイラはどのように実装されるか}
+
+\subsection{手作業による機械的な変形で解くことができる問題がある}\label{section:hand-solve}
+
+ソルバのことはいったん忘れて、手作業による機械的な変形で解くことができる問題を AtCoder Beginner Contest 100 の $4$ 問目 Patisserie ABC (\url{https://atcoder.jp/contests/abc100/tasks/abc100_d}) を例に見てみよう。
+これは整理すると以下のような問題である。
+そこまで難しくはないので、自分がどうこの問題を解いているのかを観察しながら一度自分で解いてみて、それから続きを読み進めてほしい。
+
+\begin{problem}[Patisserie ABC から引用]\label{patisserie-abc}
+    \begin{quotation}
+        高橋君はプロのパティシエになり, AtCoder Beginner Contest 100 を記念して, 「ABC洋菓子店」というお店を開いた.
+
+        ABC洋菓子店では, $N$ 種類のケーキを売っている.
+        各種類のケーキには「綺麗さ」「おいしさ」「人気度」の $3$ つの値を持ち, $i$ 種類目のケーキの綺麗さは $x_i$, おいしさは $y_i$, 人気度は $z_i$ である.
+        これらの値は $0$ 以下である可能性もある.
+
+        りんごさんは, ABC洋菓子店で $M$ 個のケーキを食べることにした.
+        彼は次のように, 食べるケーキの組み合わせを選ぶことにした.
+        \begin{itemize}
+            \item 同じ種類のケーキを $2$ 個以上食べない.
+            \item 上の条件を満たしつつ, (綺麗さの合計の絶対値) + (おいしさの合計の絶対値) + (人気度の合計の絶対値) が最大になるように選ぶ.
+        \end{itemize}
+        このとき, りんごさんが選ぶケーキの (綺麗さの合計の絶対値) + (おいしさの合計の絶対値) + (人気度の合計の絶対値) の最大値を求めなさい.
+    \end{quotation}
+\end{problem}
+
+形式的に書けば以下のようになる。
+
+\begin{problem}[形式化された問題\ref{patisserie-abc}]\label{patisserie-abc-formal}
+    長さ $N$ の整数列 $x = (x_0, x_1, \dots, x _ {N - 1}), \; y = (y_0, y_1, \dots, y _ {N - 1}), \; z = (z_0, z_1, \dots, z _ {N - 1})$ と自然数 $M \le N$ が与えられる。
+    集合 $X \subseteq N = \{ 0, 1, \dots, N - 1 \}$ に対し
+    \[
+        f(X) = \left|\sum_{i \in X} x_i\right| + \left|\sum_{i \in X} y_i\right| + \left|\sum_{i \in X} z_i\right|
+    \]
+    と定義する。
+    このとき $\max \Set{ f(X) | X \subseteq N \land \lvert X \rvert = M }$ を求めよ。
+\end{problem}
+
+これは機械的に解ける。
+このとき求める値 $y$ は
+\[
+    y = \max \Set{ \lvert a \rvert + b | \dots }
+\]
+の形の式で定義されている。
+$\lvert a \rvert = \max \Set{ a, -a }$ であるので、このような式は
+\[
+    y = \max \Set{ \max \Set{ a, -a } + b | \dots }
+\]
+を経由して
+\[
+    y = \max \Set{ \max \Set{ a + b | \dots }, \max \Set{ - a + b | \dots } }
+\]
+と変形できる。
+この変形を可能な限り繰り返すと、求める式は
+\[
+    y = \max \Set{
+        \begin{array}{l}
+            \max \Set{ + \sum_{i \in X} x_i + \sum_{i \in X} y_i + \sum_{i \in X} z_i | \ldots X \ldots }, \\
+            \max \Set{ + \sum_{i \in X} x_i + \sum_{i \in X} y_i - \sum_{i \in X} z_i | \ldots X \ldots }, \\
+            \max \Set{ + \sum_{i \in X} x_i - \sum_{i \in X} y_i + \sum_{i \in X} z_i | \ldots X \ldots }, \\
+            \max \Set{ + \sum_{i \in X} x_i - \sum_{i \in X} y_i - \sum_{i \in X} z_i | \ldots X \ldots }, \\
+            \max \Set{ - \sum_{i \in X} x_i + \sum_{i \in X} y_i + \sum_{i \in X} z_i | \ldots X \ldots }, \\
+            \max \Set{ - \sum_{i \in X} x_i + \sum_{i \in X} y_i - \sum_{i \in X} z_i | \ldots X \ldots }, \\
+            \max \Set{ - \sum_{i \in X} x_i - \sum_{i \in X} y_i + \sum_{i \in X} z_i | \ldots X \ldots }, \\
+            \max \Set{ - \sum_{i \in X} x_i - \sum_{i \in X} y_i - \sum_{i \in X} z_i | \ldots X \ldots }  \\
+        \end{array}
+    }
+\]
+となる。
+次に絶対値記号が取れた $\max \Set{ \pm \sum x_i \pm \sum y_i \pm \sum z_i | \ldots X \ldots }$ の形の $8$ 本の式の計算が必要である。
+$x_i' = - x_i$ とおけば $- \sum x_i = \sum x_i'$ であるなど、符号の正負は同様に扱える。つまり次の式の計算だけを考えればよい。
+\[
+    \max \Set{ \sum_{i \in X} x_i + \sum_{i \in X} y_i + \sum_{i \in X} z_i | X \subseteq N \land \lvert X \rvert = M }
+\]
+$\sum_{\phi(i)} f(i) + \sum_{\psi(i)} g(i)$ は $\phi(i) \leftrightarrow \psi(i)$ のとき $\sum_{\phi(i)} (f(i) + g(i))$ で置き換えられる。
+$w_i = x_i + y_i + z_i$ とおいて次の式の計算だけを考えればよい。
+\[
+    \max \Set{ \sum_{i \in X} w_i | X \subseteq N \land \lvert X \rvert = M }
+\]
+この形の式「$N$ 個のものから $M \le N$ 個選んだときの重み総和の最大値」は十分典型的でかつこれ以上分解できそうにないものであり、これを $O(N M)$ で解く方法は既知のものとしてよいだろう\footnote{$O(N \log N)$ や $O(N)$ でもよい。}。
+よってこれは計算できる式であり、機械的な変形により $y$ が $O(N M)$ で計算できることが分かった。
+$N, M$ の上限と計算時間制限が与えられていれば、これが時間内に計算できることも機械的に判定できる。
+よってこの問題は機械的に解けると言える。
+
+
+\subsection{このような手動での機械的な変形はプログラムによっても可能である}\label{section:machine-solve}
+
+\ref{section:hand-solve}節で見たような機械的な変形がプログラムによっても可能であることを、引き続き Patisserie ABC を例に見ていこう。
+「このようにして機械的に解ける」と主張した上の説明を分析して裏に隠されたものも明示すれば、さらにいくつかの要素に分解することができる。
+主には以下のような $3$ 段階のものとして説明できる。
+
+\begin{enumerate}[label=(\arabic{enumi}.)]
+    \item 自然言語で入力された問題を形式的な形に変形する
+    \item 適用するべき変換規則を選択し適用する
+    \item 十分に簡単な形に変形された問題を実際の実装として出力する
+\end{enumerate}
+
+順番に見ていこう。
+
+まず (1.) について。
+これはソルバによっては扱わず、ソルバの利用者に行わせるものとするのだった。
+適当な高級言語を用意し、問題をそのままその言語の上に翻訳したものを入力させることになる。
+入力されたプログラムを解釈した結果は、たとえば図\ref{input-syntax}のような構文木として理解できる。
+
+\begin{figure}[p]\label{input-syntax}
+    \begin{center}
+        \begin{forest}
+            [$\max$
+                [$\Set{\ldots | \ldots}$
+                    [$+$
+                        [$\lvert \ldots \rvert$
+                            [$\sum$
+                                [$\in$
+                                    [$i$]
+                                    [$X$]
+                                ]
+                                [$x_{\dots}$
+                                    [$i$]
+                                ]
+                            ]
+                        ]
+                        [$+$
+                            [$\lvert \ldots \rvert$
+                                [$\sum$
+                                    [$\in$
+                                        [$i$]
+                                        [$X$]
+                                    ]
+                                    [$y_{\dots}$
+                                        [$i$]
+                                    ]
+                                ]
+                            ]
+                            [$\lvert \ldots \rvert$
+                                [$\sum$
+                                    [$\in$
+                                        [$i$]
+                                        [$X$]
+                                    ]
+                                    [$z_{\dots}$
+                                        [$i$]
+                                    ]
+                                ]
+                            ]
+                        ]
+                    ]
+                    [$\land$
+                        [$\subseteq$
+                            [$X$]
+                            [$N$]
+                        ]
+                        [${=}$
+                            [$\lvert \ldots \rvert$
+                                [$X$]
+                            ]
+                            [$N$]
+                        ]
+                    ]
+                ]
+            ]
+        \end{forest}
+    \end{center}
+    \caption{形式化された問題\ref{patisserie-abc-formal}を表現する構文木の一例\footnote{これは例示であり、実際にはもうすこし \lambda 項に寄せた表現を用いる。}}
+\end{figure}
+
+次に (2.) について。
+
+問題\ref{patisserie-abc}を機械的に解く過程で出現した変形は主に以下の $5$ 種であった\footnote{$a + (b + c) = (a + b) + c$ や、$a = b$ ならば $f(a) = f(b)$ であるといった自明な等式については省略した。}。
+
+\begin{itemize}
+    \item $\lvert a \rvert = \max \Set{ a, -a }$ という等式に基づく変換
+    \item $\max \Set{ \max \Set{ a, b } + c | \dots } = \max \Set{ \max \Set{ a + c | \dots }, \max \Set{ b + c | \dots } }$ という等式に基づく変換
+    \item $- \sum_{i \in X} a_i = \sum_{i \in X} b_i$ という等式に基づく変換 (ただし $b_i = - a_i$ とおく)
+    \item $\sum_{i \in X} a_i + \sum_{i \in X} b_i = \sum_{i \in X} c_i$ という等式に基づく変換 (ただし $c_i = a_i + b_i$ とおく)
+    \item $\max \Set{ \sum_{i \in X} w_i | X \subseteq N \land \lvert X \rvert = M }$ から適切な式\footnote{たとえば列 $w' = \mathrm{reverse}(\mathrm{sort}(w))$ を計算した後に $\sum_{i < M} w'_i$ を計算するような式。} への変換
+\end{itemize}
+
+
+変換規則と構文木が与えられたとき「変換が適用できるかを判定すること」および「変換を適用した結果を得ること」はプログラムによって可能である。
+実際、このような規則は図\ref{max-max-rule}に示すような木から木への組み換えとして理解できる。
+
+\begin{figure}[p]\label{max-max-rule}
+    \begin{center}
+        \begin{forest}
+            [,phantom,s sep=20ex
+                [$\max$,name=left
+                    [$\Set{\ldots | \ldots}$
+                        [$+$
+                            [$\max$
+                                [$\Set{\ldots}$
+                                    [$a$]
+                                    [$b$]
+                                ]
+                            ]
+                            [$c$]
+                        ]
+                        [$\varphi$]
+                    ]
+                ]
+                [$\max$,name=right
+                    [$\Set{\ldots}$
+                        [$\max$
+                            [$\Set{\ldots | \ldots}$
+                                [$+$
+                                    [$a$]
+                                    [$c$]
+                                ]
+                                [$\varphi$]
+                            ]
+                        ]
+                        [$\max$
+                            [$\Set{\ldots | \ldots}$
+                                [$+$
+                                    [$a$]
+                                    [$b$]
+                                ]
+                                [$\varphi$]
+                            ]
+                        ]
+                    ]
+                ]
+            ]
+            \draw[-latex,dotted] (left) edge[out=north east,in=north west] (right);
+        \end{forest}
+    \end{center}
+    \caption{等式 $\max \Set{ \max \Set{ a, b } + c | \dots } = \max \Set{ \max \Set{ a + c | \dots }, \max \Set{ b + c | \dots } }$ に基づく変換規則の、構文木の書き換えとしての表現}
+\end{figure}
+
+ただしもちろん、これらの変換規則を人の手によって事前に組み込んでおくことが前提である。
+競技プログラミングをする上で有用な等式を変換の向きと共に列挙することとなる。
+
+変換の個々の適用が可能であることだけでは十分でない。
+考えられる変換はこれらだけではないため「適用する変換を適切に選択できること」もまた必要だからである。
+この変換の選択の部分は自明ではない。
+いまのところ式の複雑さが減少するにように貪欲に変換すればたいていの場合で上手くいくだろうが、実際にはヒューリスティックな探索を行うことになるだろう。
+
+いずれにせよ、トランスパイラの形のソルバはこのような「変換規則の集合」として表現されうる。
+たとえば実際、Haskell のコンパイラである GHC の最適化機構は ``rewrite rule'' と呼ばれる規則を用いて、上で見たのとほとんど同じように行われる。
+
+最後に (3.) について。
+そもそも操作対象である形式的な数式はそれ自体がある種のソースコードである。
+これを C++ のような高級言語に変換することは難しくない。
+
+
+
+
+
+\section{関連研究}
+
+一般のものであれば、以下のものが近いだろう。
+
+\begin{itemize}
+    \item \href{https://oeis.org/}{オンライン整数列大辞典 (OEIS)} は整数列の巨大なデータベースである。
+        入出力が共に単一の整数であるような問題では、愚直解を書いて得られた整数列で OEIS を検索することで解法が判明することがある。
+    \item \href{https://www.wolframalpha.com/}{Wolfram|Alpha} は数学関連の質問応答システムである。
+        問題を解く過程で出てきた複雑な数式を Wolfram|Alpha に渡すことで解法が得られることがある。
+    \item 新井紀子らの\href{https://21robot.org/}{ロボットは東大に入れるか}プロジェクトは
+    \item \href{https://github.com/angr/angr}{angr} は CTF などで用いられるバイナリ解析フレームワークである。
+    \item DARPA の \href{https://www.darpa.mil/program/cyber-grand-challenge}{Cyber Grand Challenge} は CTF の問題を自動で
+    \item \href{https://copilot.github.com/}{GitHub Copilot} やこれに用いられている \href{https://openai.com/blog/openai-codex/}{OpenAI Codex} のような言語モデルは、自然言語の問題文からその愚直解を生成することができる。
+        Daniel Paleka (\href{https://codeforces.com/profile/valkyrie}{valkyrie}) による\href{https://codeforces.com/blog/entry/94353}{これを実際に利用してみての分析}が Codeforces の blog にある。
+    \item \href{https://github.com/borzunov/cpmoptimize}{borzunov/cpmoptimize} は Python の関数を行列累乗を用いて書き換える decorator である。
+        \href{https://kukuruku.co/post/automatic-algorithms-optimization-via-fast-matrix-exponentiation/}{これに関してのブログ記事}や\href{https://news.ycombinator.com/item?id=17592359}{これに関しての Hacker News のスレッド}には多くの関連するプロジェクトが見つかる。
+\end{itemize}
+
+競技プログラミングでの利用を意図したものに限れば、以下のような事例がある。
+
+\begin{itemize}
+    \item 競技プログラミングの解法コードに貼り付けて利用するためのライブラリは広く開発されている。これらは最も素朴な形の「競技プログラミングの問題のソルバ」だと思うこともできるだろう。たとえば \href{https://github.com/beet-aizu/library}{beet-aizu/library} がある。
+    \item 個別の問題のソルバとしては \href{https://atcoder.jp/users/wata}{wata} による「Σ電卓」が知られている (\href{https://github.com/wata-orz/SigmaCalculator}{wata-orz/SigmaCalculator}, \href{https://wata-orz.hatenadiary.org/entry/20091223/1261582436}{Σ電卓 - てきとーな日記}) (2009 年)。
+    \item 実装には至っておらず構想のみであるが、一般の問題の解法の自動生成についての試みが \href{https://www.topcoder.com/members/cafelier/}{kinaba} によってなされている (\href{https://topcoder-g-hatena-ne-jp.jag-icpc.org/cafelier/20120204/1328332594.html}{SRM 531 Div2 250 - cafelier@SRM - TopCoder部} など) (2012 年)。
+    \item AtCoder Regular Contest のある A 問題の解法の完全自動生成が \href{https://atcoder.jp/users/mkotha}{mkotha} によって行われたことがある (\url{https://twitter.com/atcoder/status/538665089931296768}, \url{https://atcoder.jp/contests/arc030/submissions/286413}) (2014 年)。
+    \item 最適化などは含まれていないが、競技プログラミングでの利用を意図して作られた言語としては \href{https://atcoder.jp/users/LayCurse}{laycurse} による cLay がある (\href{http://rsujskf.s602.xrea.com/?cLay}{cLay概要（version 20201123-1） - ゲームにっき（仮）別館（仮）}) (207 年から)。
+    \item マラソンマッチなどでの利用を意図したプログラミング言語として \href{https://atcoder.jp/users/colun}{colun} による mmlang がある (\href{https://github.com/colun/mmlang}{colun/mmlang}) (2021 年から)。データ構造の差分の計算の自動導出機能を持つ。
+\end{itemize}
+
+一般の競技プログラミングの問題を解くソルバを目指しているものとしては、ある程度の形になっているものは見つけられていない。
+
+
+% \bibliography{how-it-works}
+% \bibliographystyle{junsrt}
+
+\end{document}
diff --git a/docs/how-it-works.pdf b/docs/how-it-works.pdf
index 7793c20f..611b5b0d 100644
Binary files a/docs/how-it-works.pdf and b/docs/how-it-works.pdf differ
diff --git a/docs/how-it-works.tex b/docs/how-it-works.tex
index 7d22b354..d0d1987e 100644
--- a/docs/how-it-works.tex
+++ b/docs/how-it-works.tex
@@ -15,54 +15,292 @@
 \usepackage[pdfencoding=auto]{hyperref}
 \usepackage{tikz}
 
-\usepackage{bibentry}
-\nobibliography*
+% \usepackage{bibentry}
+% \nobibliography*
 
-\newtheorem{problem*}{問題}[section]
+\newtheorem{problem*}{Problem}[section]
 \newenvironment{problem}{\begin{problem*}\renewcommand{\qedsymbol}{\(\diamond\)}\pushQED{\qed}}{\popQED\end{problem*}}
-\newtheorem{definition*}{定義}[section]
+\newtheorem{definition*}{Definition}[section]
 \newenvironment{definition}{\begin{definition*}\renewcommand{\qedsymbol}{\(\diamond\)}\pushQED{\qed}}{\popQED\end{definition*}}
 
 
-\title{競技プログラミングの問題は機械的に解けるか？}
+\title{Towards automatically solving problems of \\ competitive programming}
 \author{Kimiyuki Onaka}
 \date{\today}
 
 \begin{document}
 \maketitle
 
+TODO: Complete translation
+
 \setcounter{section}{-1}
-\section{概要}
+\section{Abstract}
+
+In this PDF, we consider the question, ``Can we automatically solve problems of competitive programming?''.
+In other words, ``Can we make a solver for competitive programming?''.
+
+In section $1$, we organize this still vague question into a more concrete one.
+We explain that there are various types of solvers that automatically solve problems of competitive programming, and clarify which type of solver we are aiming to develop.
+Our goal is to develop a solver that receives a formally expressed problem as input and outputs a solution to it, especially one that uses naive source code as its ``formally expressed problem''.
+Such a solver is, in other words, a transpiler with optimization about asymptotic computational complexity.
+Therefore, the question ``Can we make a solver for competitive programming?'' becomes a concrete question: ``Can we make a transpiler with optimization about asymptotic computational complexity?''
+Also, for practical use, it would be easier to use it as an IDE plugin that rewrites a code snippet to reduce its asymptotic computational complexity, instead of transpiling the entire source code.
+
+In section $2$, we give a tentative answer to this concretized question.
+We describe how to implement a solver for competitive programming as a transpiler with optimization, and observes that such a solver can solve some problems.
+The implementation strategy is mechanical rewriting of expression trees.
+For example, when the solver detects a part that is naively taking interval sums many times, the solver replaces it with cumulative sums.
+For another example, when it detects a part that is naively doing convolution with double loops, then it replaces the part with convolution using FFT.
+Such rewriting is expressed as a rule called ``rewrite rules'', and the core of such a solver is implemented as a set of rewrite rules.
+
+\section{What is automatically solving problems of competitive programming}
+
+\subsection{Why do we want to solve problems automatically?}
+
+First of all, let's discuss the significance of the question, ``Can you automatically solve problems of competitive programming?''.
+Why do we want to automatically solve problems of competition programming?
+There are three main reasons for this.
+
+\begin{enumerate}[label=(\arabic{enumi}.)]
+    \item Practical use in competition programming: ``We want to automate works during a contest to get a better rating'', ``The execution log of a solver may be used for learning purposes'', etc.
+    \item Engineering interest: ``We want to know how many problems can be solved automatically.''
+    \item Philosophical motivation: ``If a problem can be solved manually but not automatically, the problem may not really be solved'', ``We want to understand how humans solve problems''.
+\end{enumerate}
+
+(1.) 競技プログラミングでの実用は分かりやすい。
+簡単な問題や難しい問題の部分問題を手動でなく自動で高速に解いてしまえるなら、難しい問題の難しい部分に時間を使うことができてコンテストで有利である。
+もし自分では解けない難しい問題がソルバによって解けるならなおさらである。
+レートに影響がなくとも、簡単な問題を自動化してしまえるなら便利で楽であろう。
+
+また、教育や学習用途でソルバを使うことができるかもしれない。
+ソルバが問題を解く過程を詳細に分かりやすく出力すれば、初心者はそれを読んで問題の解き方を学ぶことができるだろう。
+
+(2.) の工学的な興味も分かりやすい。
+単純に、どの程度の問題までなら自動で解けてしまうのか (そしてどのような問題は自動では解きにくいか) を知れれば面白い。
+
+(3.) は哲学的な動機である。
+我々は競技プログラミングの問題を手動で解くことができる。
+それはいったいなぜだろうか？
+問題を解く方法を具体的なアルゴリズムとして説明できるだろうか？
+それができないのに「競技プログラミングの問題を解くことができる」と言い切ってしまってよいのだろうか？
+
+たとえば、普通に競技プログラミングをしている人が「ある問題が頭の中では解けました。しかし実装方法については検討も付きません」と発言しているとしよう。
+ある程度競技プログラミングをやったことのある人であれば、そのような発言に対しては「解けたつもりになっているのが間違いで、そんな状況のことを解けたとは言わない」と思うだろう。
+つまり、みな「問題が解けたならば実装できるはずだ」と信じているのである。
+これと似た別の状況を考えてみよう。
+「ある問題が解けて実装もできた。しかしなぜ私にこれが解けたのかはよく分からない」という状況である。
+このような状況もやはり「その問題に対する理解が足りていない」とみなされることが多いだろう。
+理解が足りていないままであれば、もしその問題の類題が出題されたときそれを解けないかもしれない。
+「問題の解法を正しく理解できたなら、その解法に至る道筋を説明できるはずだ」と信じている人は多いはずである。
+これらの観察からは次のことが疑われる。
+つまり「競技プログラミングを十分に理解しているならば、そのソルバも実装できるはずである」。
+ソルバを実装しようとしてみることは競技プログラミングへの理解に貢献するだろう。
+
+これはさらには、より一般の人間の思考についての問い、つまり「考えるとはどのようなことか」を考えることにも繋がってくる。
+たとえば、機械的な規則の適用をくり返すことで実装されたソルバがもし人間に匹敵するような成功を収めたとすれば、そこから人間の思考も結局は規則の機械的な適用を素早く行っているだけではないかと疑うことができる。
+あるいは逆にそのようなソルバがまったく失敗してしまうなら、人間の思考には機械的な規則の適用としては捉えきれない暗黙的な部分があることが疑われる。
+
+
+\subsection{How do humans solve problems of competitive programming?}
+
+There are many things during solving competitive programming problems.
+Let's start by sorting this out.
+What steps are there in the process of solving a problem from the moment the problem page is opened (e.g., right after clicking on the link \url{https://atcoder.jp/contests/abc184/tasks/abc184_c}) to the moment you see the green ``AC'' mark?
+Of course, this process can include too many things (e.g., interpreting the diagram embedded in the question, scrolling through the question page, clicking the blue ``submit'' button, etc.) and can be described in many details.
+However, if we ignore the inessential ones and organize them in an abstract form, the usual process can be modeled into three steps:
+
+\begin{description}
+    \item[(1.) Interpretation] Read a problem given in natural language and organize it as a mathematical problem.
+    \item[(2.) Consideration] Find a mathematical solution to the mathematical problem.
+    \item[(3.) Implementation] Write the mathematical solution as a concrete implementation on a computer.
+\end{description}
+
+順番に見ていこう。
+(1.) は (人間にとっては) 自明なのであまりかえりみられることのないステップである。
+このステップでは、日本語や英語で書かれた問題を読み、数式などで表現された問題として整理し理解する。
+たとえば「熊の Limak が人間の高橋くんに合いに AtCoder 王国を訪れている。
+AtCoder 王国は $1$ から $N$ までの番号の付いた島と、それらの間にかかる $M$ 本の橋からなる。
+今 Limak は $s$ 番目の島にいて、高橋くんは $t$ 番目の島にいる。
+そして……」のような問題文を読んで理解し、不要な情報を捨象して「$N$ 頂点無向グラフ $G = (V, E)$ と $s, t \in V$ が与えられる。……」のような問題であることを確認する。
+
+(2.) は競技プログラミングにおいて最も難しくかつ面白いとされるステップである。
+このステップでは、(1.) で理解した問題に対し、実行時間などの制限を満たす解法を考案する。
+たとえば、考察の結論として「まず重み付きグラフ $G = (V, E, w)$ とすべての頂点 $x \in V$ に対し $s-x$ 最短路を $s$ からの Dijkstra 法で求める。
+次に重み付きグラフ $G' = (V, E, w')$ とすべての頂点 $x \in V$ に対し $t-x$ 最短路を $t$ からの Dijkstra 法で求め、そして……」などのアルゴリズムが得られる。
+
+(3.) はジャッジサーバによる自動採点のために必要なステップである。
+このステップでは、(2.) で得たがまだ頭の中にある抽象的なアルゴリズムを、計算機上の具体的なコードへ翻訳する。
+たとえば「$s-t$ 最短路を Dijkstra 法で求めればよい」というときには、C++ なら
+\verb|priority_queue<pair<int64_t, int>> que; que.emplace(0, s); while (not que.empty()) …|
+のようなコードが書かれるだろう。
+
+そして、今回の話題は (2.) の「考察」のステップである。
+このステップは競技プログラミングという行為において中心となるステップであり、「問題を解く」と言うときも主にこのステップに注目している。
+つまり「競技プログラミングの問題を自動で解きたい」とは「考察を自動で行いたい」ということである。
+
+The topic of this article is (2.), the ``Consideration'' step.
+This step is the central step in the act of competitive programming, and when we say ``solving a problem'', we are mainly focusing on this step.
+In other words, ``We want to automatically solve problems of competition programming'' means ``We want to do the `Consideration' step automatically''.
+
+
+
+
+\subsection{Solvers for competitive programming should leave the formalization to humans.}
+
+Even if we divide the process of solving a problem of competitive programming into the three steps of ``Interpretation'', ``Consideration'', and ``Implementation'', and say that we mainly want to do the ``Consideration'', the remaining two steps are not easily separated.
+The problem has to be input in some form, and the solution has to be output in some form.
+We need to be able to handle the remaining steps of ``Interpretation'' and ``Implementation''.
+
+機械にとって最も面倒なのは「読解」だろう。
+自然言語の理解という高度な処理が必要になる。
+競技プログラミングの問題文を以降のステップに支障がでないように読み取るには、表面的に単語を追うだけではおそらく足りず、文章全体の意図を正しく把握する必要があるだろう。
+競技プログラミングの問題文以外は理解できなくてよいのだとしても、これはかなり困難である。
+そしてこの「読解」は今回やりたいことではない。
+ソルバの一部として取り扱うのは諦めて、人間 (あるいは GitHub Copilot のような言語モデル) に任せてしまうべきだろう。
+
+「実装」もそのままの形では機械では扱えない。
+「数学的な解法を、計算機上の具体的な実装として記述する」と言うときの「数学的な解法」などは、(通常の人間による競技プログラミングにおいては) 人間の頭の中のみ存在するものだからである。
+人間の頭の中にしかないものは機械には扱えない。
+「数学的な解法」でなくて「数学的な問題」の場合も同様である。
+
+一方で、機械で扱える形に形式化したものが入力であれば「実装」も機械に可能である。
+このことはコンパイラを思い出せば分かる。
+F\# や Haskell のような高級言語のソースコードを仮想機械の中間言語や実際の機械語に変換する操作はまさに「実装」であろう。
+
+Therefore, when we were to use a solver to solve a problem of competitive programming, the process could be organized into four steps as follows:
+
+\begin{description}
+    \item[(1.) Interpretation] (A human) reads a problem given in natural language and organizes it as a mathematical problem.
+    \item[(2.) Translation] (A human) inputs the mathematical problem as a formalized problem on a computer.
+    \item[(3.) Consideration'] (A solver) computes a solution mechanically to the translated formalized solution.
+    \item[(4.) Implementation'] (A solver) outputs the computed solution as an concrete implementation.
+\end{description}
+
+(1.) and (2.) together do the ``Formalization'' process.
+Both of these steps are easy for humans.
+Admittedly, the ``Interpretation'' step is easy.
+The step of ``Translation'' is also easy for humans.
+We can just write what we read.
+This is similar to the fact that it is usually not so difficult to type a difficult mathematical expression in LaTeX, even if you don't understand it at all.
+
+競技プログラミングのソルバが (1.) と (2.) のステップによる「形式化」を人間に任せてしまったとして、そのような条件で残りのステップだけを処理した場合も「競技プログラミングの問題を自動で解けた」と言ってよいだろうか？
+これは「自動で解けた」と言ってしまってよいだろう。
+なぜなら、「形式化」は (機械にとっては難しいとはいえ) 人間にとってはたいてい簡単であるし、通常は重要視されるステップではないからである。
+困難でも重要でもないステップを省略しても、困難で重要な (3.) の「考察'」のステップをうまく扱うのなら「問題を自動で解く」と言ってよいだろう。
+様々なことを自動でしてくれるソフトウェアであってもデータの打ち込みは人間の担当であることは多く、今回もそうだったというだけである。
+
+
+\subsection{We should implement a solver for competitive programming in the form of a transpiler.}
+
+I said that the input to the solver should be a ``formalized problem'', but what exactly should be the ``formalized problem''?
+Is it a $3$-tuple of $(\text{variables as input}, \text{variables as output}, \text{constraints to be satisfied})$?
+Or is it a graph of a computable function?
+It could be anything.
+As long as it can represent the problem, it is unlikely that the choice of input format will make the problem solvable or unsolvable.
+You can use whatever you like.
+
+However, the input format to a solver greatly affects the ease of implementation of the solver itself.
+What kind of input is easiest to use?
+From my experience of implementing several prototypes, I think it is better to use an executable program as a formalized problem.
+If ``executable programs'' are the input to the solver, the process of competitive programming can be reduced to the following three steps:
+
+\begin{description}
+    \item[(1.) Interpretation] (A human) reads a problem given in natural language and organizes it as a mathematical problem.
+    \item[(2.) Implementation''] (A human) writes a naive solution to the mathematical problem.
+    \item[(3.) Consideration''] (A solver) optimizes the given implementation in its computational complexity.
+\end{description}
+
+In this case, the ``Consideration'' '' step in (3.) uses a programming language as both input and output.
+The output is a faster program that does the same calculation as the input program.
+This is the same to ``optimization''.
+In other words, if we use a ``executable program'' as the input of a solver, the ``solver that automatically solves the problem of competitive programming'' becomes a ``transpiler with optimization''.
+
+The notion of ``a solver that automatically solves problems of competitive programming'' has been explicated as the concept of ``a transpiler with optimization''.
+This is a big step forward.
+We can now write the ``usual one'' instead of ``some mysterious and amazing thing''.
+Compared to something like artificial intelligence, compilers are much easier to develop.
+We can use a lot of existing technologies and materials.
+Another advantage is that the gap between input and output is small.
+Even a program that simply outputs its input can now be claimed to be the ``trivial solver''.
+
+Note that it is not obvious to use an ``executable program'' as a ``formalized problem''.
+It may sound natural to hear the answer first.
+But remember, a ``problem'' and a ``program'' are two very different things.
+You can run a program, but you cannot run a problem.
+A program has an asymptotic computational complexity, but a problem does not have an asymptotic computational complexity.
+At least I couldn't get over this gap until I had made a few prototypes.
+
+Other than transpilers, other types of solvers are possible, such as interactive solvers, or solvers consisting of a database of past problems and a search engine.
+
+
 
-この PDF では、競技プログラミングの問題を機械的に解くことについて議論する。
+\subsection{Not all problems of competition programming can be solved automatically.}
 
-まず $3$ 章までで競技プログラミングの問題を機械的に解くことについての概要を見る。
-$1$ 章でいくつかの問題が解かれる過程を分析し、機械によって競技プログラミングの問題を解くことは有望であることを確認する。
-問題の形式化を取り扱わないことにすれば、 AtCoder 水色程度の能力のプログラムができうるだろうというのが結論である。
-$2$ 章では、機械的に解くことが難しいだろう問題の例を見る。
-問題自体に再帰が含まれるような複雑な問題 (たとえばゲームに関する問題) などでは困難が大きいことを見る。
-また、問題の形式化そのものが問われている問題 (たとえば幾何問題) は今回の手法の範囲外であることも確認する。
-$3$ 章では、自動で問題を解くプログラムを作ることの意義を説明する。
-ここまでは一般の競技プログラマーに向けての文章である。
+It probably goes without saying, but I should warn you that not all problems of competitive programming can be solved automatically.
+You shouldn't expect too much.
+Problems that are suitable for mechanical methods will be solved, but problems that are not suitable for mechanical methods will not be solved.
+At least for a while, a solver will be nothing more than a toy software.
 
-$4$ 章では競技プログラミングの問題を解くプログラムの実装のための背景の理論を説明する。
-これはそのようなプログラムの開発者に向けての文章である。
+Especially for solvers as transpilers, problems that are not suitable for them include the following:
 
-\section{いくつかの問題はプログラムによって解ける}
+\begin{enumerate}[label=(\arabic{enumi}.)]
+    \item Problems difficult to implement naive solutions
+    \item Problems that require ``intuition'' or ``inspiration''
+    \item problems that are intrinsically complicated
+\end{enumerate}
+
+(1.) は、たとえば幾何の問題である。
+ソルバの担当範囲以外の部分が難しい。
+そのような場合は人間が頑張るしかない。
+考察要素がある問題であってもその考察要素が「愚直に実装するとたいへんだが、うまく工夫すると実装量を減らすことができる」という形であれば、やはりソルバは無力である。
+
+(2.) は、たとえば貪欲法が想定解の問題である。
+ソルバの担当範囲が難しい。
+実装にもよるだろうが、基本的にソルバは 1 歩ずつ考察を詰めていけば解けるような問題しか解けないだろう。
+「証明はできないけどなんとなく正しそう」のような判断は機械とは相性が悪そうである。
+「突然ですが、ここで $x = f(y, g(y, z))$ とおきます。すると……」のような発見的解法も機械とは相性が悪そうである。
+手法によっては扱えるかもしれないが、少なくとも、先程の節で述べたような形の機械的解法で解くことはできない。
+
+(3.) は、たとえばゲームの問題がそうだろう。
+交互ゲームで「先手が必勝である」ことを表現しようと思うだけで、量化子の繰り返しや再帰関数のような扱いにくいものが出てきてしまう。
+きれいな式で表現できないような問題と機械の相性は悪いだろう。
+
+
+
+\subsection{About use of a solver in practice}
+
+Let's consider what a solver for competitive programming looks like from view of the users who use it during contests.
+Basically, it will only be in a position not so different from the current \href{https://oeis.org/}{The On-Line Encyclopedia of Integer Sequences} (OEIS) and \href{https://www.wolframalpha.com/}{Wolfram|Alpha}.
 
-\subsection{手作業による機械的な変形で解くことができる問題がある}
+まず明らかに言えることは、一般にソルバは銀の弾丸にはならないということである。
+もしどんなに優秀なソルバが開発されたとしても、そのようなソルバで解けてしまう問題は出題前に弾かれるだけである。
+ソルバが利用できるとしても、それは実際の問題の部分問題に対してのみであろう。
+また、ソルバですべての問題が解けるわけではないので、ユーザは「問題が自動的に解けるのはどのような場合であるか」を大まかに判断できる必要がある。
+機械的に解けうる問題であっても入力の与え方次第では解けないことも多いので、この判断を行なえることはソルバの利用のために必要である。
+しかしそのような判断ができるには結局はユーザ自身の能力が要求される。
 
-AtCoder Beginner Contest 100 の $4$ 問目 Patisserie ABC (\url{https://atcoder.jp/contests/abc100/tasks/abc100_d}) を例に見てみよう。
+Also, the input can only be a problem itself when we think a ``solver for competition programming problems'', but other possibilities appear when considering practical use in contests.
+Since only a small portion of the final solution code is intrinsically related to its algorithm, we can use such code fragments as input.
+Then, something that deals only with such code fragments will be an extension of refactoring support functions of editors.
+It can be realized as a ``plugin to an IDE''.
+When the user specifies a code fragment, the plugin will rewrite it by reducing the asymptotic computational complexity of that fragment.
+If the input/output is not the whole source code but small code fragments, it will be convenient to interpret and reuse the results more flexibly.
+
+
+\section{How is a transpiler with optimization implemented?}
+
+\subsection{Some problems can be solved by mechanical transformation by hand.}\label{section:hand-solve}
+
+ソルバのことはいったん忘れて、手作業による機械的な変形で解くことができる問題を AtCoder Beginner Contest 100 の $4$ 問目 Patisserie ABC (\url{https://atcoder.jp/contests/abc100/tasks/abc100_d}) を例に見てみよう。
 これは整理すると以下のような問題である。
 そこまで難しくはないので、自分がどうこの問題を解いているのかを観察しながら一度自分で解いてみて、それから続きを読み進めてほしい。
 
-\begin{problem}[Patisserie ABC から引用]
-    \label{patisserie-abc}
+\begin{problem}[Patisserie ABC から引用]\label{patisserie-abc}
     \begin{quotation}
         高橋君はプロのパティシエになり, AtCoder Beginner Contest 100 を記念して, 「ABC洋菓子店」というお店を開いた.
 
         ABC洋菓子店では, $N$ 種類のケーキを売っている.
-        各種類のケーキには「綺麗さ」「おいしさ」「人気度」の $3$ つの値を持ち, $i$ 種類目のケーキの綺麗さは $x_i$ , おいしさは $y_i$ , 人気度は $z_i$ である.
+        各種類のケーキには「綺麗さ」「おいしさ」「人気度」の $3$ つの値を持ち, $i$ 種類目のケーキの綺麗さは $x_i$, おいしさは $y_i$, 人気度は $z_i$ である.
         これらの値は $0$ 以下である可能性もある.
 
         りんごさんは, ABC洋菓子店で $M$ 個のケーキを食べることにした.
@@ -77,8 +315,7 @@ \subsection{手作業による機械的な変形で解くことができる問
 
 形式的に書けば以下のようになる。
 
-\begin{problem}[形式化された問題\ref{patisserie-abc}]
-    \label{patisserie-abc-formal}
+\begin{problem}[形式化された問題\ref{patisserie-abc}]\label{patisserie-abc-formal}
     長さ $N$ の整数列 $x = (x_0, x_1, \dots, x _ {N - 1}), \; y = (y_0, y_1, \dots, y _ {N - 1}), \; z = (z_0, z_1, \dots, z _ {N - 1})$ と自然数 $M \le N$ が与えられる。
     集合 $X \subseteq N = \{ 0, 1, \dots, N - 1 \}$ に対し
     \[
@@ -129,14 +366,15 @@ \subsection{手作業による機械的な変形で解くことができる問
 \[
     \max \Set{ \sum_{i \in X} w_i | X \subseteq N \land \lvert X \rvert = M }
 \]
-この形の式「$N$ 個のものから $M \le N$ 個選んだときの重み総和の最大値」は十分典型的でかつこれ以上分解できそうにないものであり、これを $O(N M)$ で解くための変形の残りの部分はすべて埋め込んでおいてよいだろう \footnote{$O(N \log N)$ や $O(N)$ でもよい。}。
+この形の式「$N$ 個のものから $M \le N$ 個選んだときの重み総和の最大値」は十分典型的でかつこれ以上分解できそうにないものであり、これを $O(N M)$ で解く方法は既知のものとしてよいだろう\footnote{$O(N \log N)$ や $O(N)$ でもよい。}。
 よってこれは計算できる式であり、機械的な変形により $y$ が $O(N M)$ で計算できることが分かった。
 $N, M$ の上限と計算時間制限が与えられていれば、これが時間内に計算できることも機械的に判定できる。
 よってこの問題は機械的に解けると言える。
 
-\subsection{このような手動での機械的な変形は、プログラムによっても可能である}
 
-引き続き Patisserie ABC を例に見ていこう。
+\subsection{Such manual mechanical transformation can also be done by programs.}\label{section:machine-solve}
+
+\ref{section:hand-solve}節で見たような機械的な変形がプログラムによっても可能であることを、引き続き Patisserie ABC を例に見ていこう。
 「このようにして機械的に解ける」と主張した上の説明を分析して裏に隠されたものも明示すれば、さらにいくつかの要素に分解することができる。
 主には以下のような $3$ 段階のものとして説明できる。
 
@@ -148,18 +386,15 @@ \subsection{このような手動での機械的な変形は、プログラム
 
 順番に見ていこう。
 
-\subsubsection{プログラムは形式的な入力のみを受け付けることとする}
-
 まず (1.) について。
-これはプログラムによっては扱わず、プログラムの利用者に行わせるものとする。
-Haskell や ML 系言語 \footnote{F\# や Standard ML など。} に似た文法のできるだけ高級な言語を用意し、問題をそのままこの言語の上に翻訳したものを入力させることになる。
+これはソルバによっては扱わず、ソルバの利用者に行わせるものとするのだった。
+適当な高級言語を用意し、問題をそのままその言語の上に翻訳したものを入力させることになる。
 入力されたプログラムを解釈した結果は、たとえば図\ref{input-syntax}のような構文木として理解できる。
 
-\begin{figure}[p]
-    \label{input-syntax}
+\begin{figure}[p]\label{input-syntax}
     \begin{center}
         \begin{forest}
-            [$\mathrm{max}$
+            [$\max$
                 [$\Set{\ldots | \ldots}$
                     [$+$
                         [$\lvert \ldots \rvert$
@@ -214,32 +449,26 @@ \subsubsection{プログラムは形式的な入力のみを受け付けるこ
             ]
         \end{forest}
     \end{center}
-    \caption{形式化された問題\ref{patisserie-abc-formal}を表現する構文木の一例 \footnote{これは例示であり、実際にはもうすこし \lambda 項に寄せた表現を用いる。}}
+    \caption{形式化された問題\ref{patisserie-abc-formal}を表現する構文木の一例\footnote{これは例示であり、実際にはもうすこし \lambda 項に寄せた表現を用いる。}}
 \end{figure}
 
-我々は汎用人工知能を作りたいのでも自然言語処理をしたいのでもない。
-もしいま無理にこれを行おうとしても、たいへんな苦労の後に実用に耐えない精度のものができあがるだけだろう。
-
-\subsubsection{変換規則は人間が列挙し、どのような順序で適用するかは機械に探索させる}
-
 次に (2.) について。
 
-問題\ref{patisserie-abc}を機械的に解く過程で出現した変形は主に以下の $5$ 種であった \footnote{$a + (b + c) = (a + b) + c$ や、$a = b$ ならば $f(a) = f(b)$ であるといった自明な等式については省略した。}。
+問題\ref{patisserie-abc}を機械的に解く過程で出現した変形は主に以下の $5$ 種であった\footnote{$a + (b + c) = (a + b) + c$ や、$a = b$ ならば $f(a) = f(b)$ であるといった自明な等式については省略した。}。
 
 \begin{itemize}
     \item $\lvert a \rvert = \max \Set{ a, -a }$ という等式に基づく変換
     \item $\max \Set{ \max \Set{ a, b } + c | \dots } = \max \Set{ \max \Set{ a + c | \dots }, \max \Set{ b + c | \dots } }$ という等式に基づく変換
     \item $- \sum_{i \in X} a_i = \sum_{i \in X} b_i$ という等式に基づく変換 (ただし $b_i = - a_i$ とおく)
     \item $\sum_{i \in X} a_i + \sum_{i \in X} b_i = \sum_{i \in X} c_i$ という等式に基づく変換 (ただし $c_i = a_i + b_i$ とおく)
-    \item $\max \Set{ \sum_{i \in X} w_i | X \subseteq N \land \lvert X \rvert = M }$ から適切な式 \footnote{たとえば列 $w' = \mathrm{reverse}(\mathrm{sort}(w))$ を計算した後に $\sum_{i < M} w'_i$ を計算するような式。} への変換
+    \item $\max \Set{ \sum_{i \in X} w_i | X \subseteq N \land \lvert X \rvert = M }$ から適切な式\footnote{たとえば列 $w' = \mathrm{reverse}(\mathrm{sort}(w))$ を計算した後に $\sum_{i < M} w'_i$ を計算するような式。} への変換
 \end{itemize}
 
 
 変換規則と構文木が与えられたとき「変換が適用できるかを判定すること」および「変換を適用した結果を得ること」はプログラムによって可能である。
 実際、このような規則は図\ref{max-max-rule}に示すような木から木への組み換えとして理解できる。
 
-\begin{figure}[p]
-    \label{max-max-rule}
+\begin{figure}[p]\label{max-max-rule}
     \begin{center}
         \begin{forest}
             [,phantom,s sep=20ex
@@ -287,499 +516,57 @@ \subsubsection{変換規則は人間が列挙し、どのような順序で適
 \end{figure}
 
 ただしもちろん、これらの変換規則を人の手によって事前に組み込んでおくことが前提である。
-「$\dots = \dots$ という等式に基づく変換」と表記したことから明らかであるように、「競技プログラミングをする上で有用な等式」を「変換の向きと共に」列挙することとなる。
-これらの変換規則を自動で獲得することは、個々の問題を解くよりはるかに難しい課題であるので行わない。
+競技プログラミングをする上で有用な等式を変換の向きと共に列挙することとなる。
 
 変換の個々の適用が可能であることだけでは十分でない。
 考えられる変換はこれらだけではないため「適用する変換を適切に選択できること」もまた必要だからである。
 この変換の選択の部分は自明ではない。
-いまのところ式の複雑さが減少するにように貪欲に変換すればたいていの場合で上手くいくだろうと予想しているが、もしそれが偽ならヒューリスティックな探索を行うことになるだろう。
+いまのところ式の複雑さが減少するにように貪欲に変換すればたいていの場合で上手くいくだろうが、実際にはヒューリスティックな探索を行うことになるだろう。
 
-\subsubsection{変形結果の式をソースコードとして出力することは難しくない}
+いずれにせよ、トランスパイラの形のソルバはこのような「変換規則の集合」として表現されうる。
+たとえば実際、Haskell のコンパイラである GHC の最適化機構は ``rewrite rule'' と呼ばれる規則を用いて、上で見たのとほとんど同じように行われる。
 
 最後に (3.) について。
 そもそも操作対象である形式的な数式はそれ自体がある種のソースコードである。
 これを C++ のような高級言語に変換することは難しくない。
 
 
-\subsection{そのようにして解ける問題の数は少なくはない}
-
-実際に AtCoder Beginner Contest の第 $100$ 回から第 $104$ 回までの $20$ 問\footnote{問題をどこから持ってくるかによっても結果は変わるだろう。}を、その問題が機械的に解けそうであるかを判断\footnote{主観的な基準で}した結果を表\ref{table-analysis}に示す。
-ここから直ちに言えることは次の $2$ 点だろう。
-
-\begin{itemize}
-    \item 解けるか解けないかは問題との相性の面が大きい
-    \item AtCoder Beginner Contest の C, D 問題が $5$ 問に $1$ 問ぐらいは解ける
-\end{itemize}
-
-\begin{table}[p]
-    \caption{\label{table-analysis} AtCoder Beginner Contest の問題が機械的に解けそうか判断した結果の一覧}
-    \begin{center}
-        \scalebox{0.8}{
-            \begin{tabular}{|l|l|c|l|} \hline
-                コンテスト & 問題 & 機械的に解けうるか & それはなぜか \\ \hline \hline
-
-                \href{https://atcoder.jp/contests/abc100}{AtCoder Beginner Contest 100} & \href{https://atcoder.jp/contests/abc100/tasks/abc100_a}{A - Happy Birthday!} & Yes & 自明 \\ \hline
-                \href{https://atcoder.jp/contests/abc101}{AtCoder Beginner Contest 101} & \href{https://atcoder.jp/contests/abc101/tasks/abc101_a}{A - Eating Symbols Easy} & Yes & 自明 \\ \hline
-                \href{https://atcoder.jp/contests/abc102}{AtCoder Beginner Contest 102} & \href{https://atcoder.jp/contests/abc102/tasks/abc102_a}{A - Multiple of 2 and N} & Yes? & 自明ではあるが面倒 \\ \hline
-                \href{https://atcoder.jp/contests/abc103}{AtCoder Beginner Contest 103} & \href{https://atcoder.jp/contests/abc103/tasks/abc103_a}{A - Task Scheduling Problem} & Yes & 自明 \\ \hline
-                \href{https://atcoder.jp/contests/abc104}{AtCoder Beginner Contest 104} & \href{https://atcoder.jp/contests/abc104/tasks/abc104_a}{A - Rated for Me} & Yes & 自明 \\ \hline \hline
-
-                \href{https://atcoder.jp/contests/abc100}{AtCoder Beginner Contest 100} & \href{https://atcoder.jp/contests/abc100/tasks/abc100_b}{B - Ringo's Favorite Numbers} & Yes & 自明 \\ \hline
-                \href{https://atcoder.jp/contests/abc101}{AtCoder Beginner Contest 101} & \href{https://atcoder.jp/contests/abc101/tasks/abc101_b}{B - Digit Sums} & Yes & 自明 \\ \hline
-                \href{https://atcoder.jp/contests/abc102}{AtCoder Beginner Contest 102} & \href{https://atcoder.jp/contests/abc102/tasks/abc102_b}{B - Maximum Difference} & Yes & 自明 \\ \hline
-                \href{https://atcoder.jp/contests/abc103}{AtCoder Beginner Contest 103} & \href{https://atcoder.jp/contests/abc103/tasks/abc103_b}{B - String Rotation} & Yes & 自明 \\ \hline
-                \href{https://atcoder.jp/contests/abc104}{AtCoder Beginner Contest 104} & \href{https://atcoder.jp/contests/abc104/tasks/abc104_b}{B - AcCepted} & Yes & 自明 \\ \hline \hline
-
-                \href{https://atcoder.jp/contests/abc100}{AtCoder Beginner Contest 100} & \href{https://atcoder.jp/contests/abc100/tasks/abc100_c}{C - *3 or /2} & No & 機械的な手法とあまり相性が良くない \\ \hline
-                \href{https://atcoder.jp/contests/abc101}{AtCoder Beginner Contest 101} & \href{https://atcoder.jp/contests/abc101/tasks/arc099_a}{C - Minimization} & No & 機械的な手法とあまり相性が良くない \\ \hline
-                \href{https://atcoder.jp/contests/abc102}{AtCoder Beginner Contest 102} & \href{https://atcoder.jp/contests/abc102/tasks/arc100_a}{C - Linear Approximation} & Yes? & 難しいが可能なはず \\ \hline
-                \href{https://atcoder.jp/contests/abc103}{AtCoder Beginner Contest 103} & \href{https://atcoder.jp/contests/abc103/tasks/abc103_c}{C - Modulo Summation} & No & 剰余は意外と面倒。難しそう \\ \hline
-                \href{https://atcoder.jp/contests/abc104}{AtCoder Beginner Contest 104} & \href{https://atcoder.jp/contests/abc104/tasks/abc104_c}{C - All Green} & No & 貪欲を含むので難しい \\ \hline \hline
-
-                \href{https://atcoder.jp/contests/abc100}{AtCoder Beginner Contest 100} & \href{https://atcoder.jp/contests/abc100/tasks/abc100_d}{D - Patisserie ABC} & Yes & 機械的な手法が有効に働く問題である \\ \hline
-                \href{https://atcoder.jp/contests/abc101}{AtCoder Beginner Contest 101} & \href{https://atcoder.jp/contests/abc101/tasks/arc099_b}{D - Snuke Numbers} & No & 機械的な手法と明らかに相性が悪い \\ \hline
-                \href{https://atcoder.jp/contests/abc102}{AtCoder Beginner Contest 102} & \href{https://atcoder.jp/contests/abc102/tasks/arc100_b}{D - Equal Cut} & No & 単純に問題が難しい \\ \hline
-                \href{https://atcoder.jp/contests/abc103}{AtCoder Beginner Contest 103} & \href{https://atcoder.jp/contests/abc103/tasks/abc103_d}{D - Islands War} & No & 形式化の形次第だが難しそう \\ \hline
-                \href{https://atcoder.jp/contests/abc104}{AtCoder Beginner Contest 104} & \href{https://atcoder.jp/contests/abc104/tasks/abc104_d}{D - We Love ABC} & Yes? & 難しいが可能なはず \\ \hline
-            \end{tabular}
-        }
-    \end{center}
-\end{table}
-
-
-
-\section{すべての問題が解けるわけではない}
-
-形式化との相性が悪い問題がいくらか存在する。
-次のような問題を解くことは難しい。
-
-\begin{enumerate}
-    \item 形式的に証明を書くことが難しい問題
-    \item 形式化する能力が問うている問題
-\end{enumerate}
-
-\subsection{妥当性の説得は簡単であっても、証明として書き下すことが難しい解法がある}
-
-競技プログラミングにおいて、解法は必ずしも証明を伴なわない。
-たとえば貪欲法を用いた解法の証明を数学的に厳密に与えることは難しい。
-小さい入力の値を表示した結果から帰納的に解法を推測することもある。
-しかしわれわれの手法は必然的に解法に証明を伴う。
-真であることが知られている等式を用いて自明な式変形を繰り返すことを基本にしているので「証明はできないがおそらく正しいであろう解法\footnote{乱択アルゴリズムのことではない}」は基本的に\footnote{実験結果の先頭 $n$ 個を使って OEIS を引くとか、無根拠に貪欲だと決め付けるなどは可能だが、まったく有意義でない}生成できない。
-
-AtCoder Beginners Selection の $7$ 問目 Card Game for Two (\url{https://atcoder.jp/contests/abs/tasks/abc088_b}) がその例である。
-これは以下のような問題である。
-
-\begin{problem}[Card Game for Two から引用]
-    \label{card-game-for-two}
-    \begin{quotation}
-        $N$ 枚のカードがあります.
-        $i$ 枚目のカードには, $a_i$ という数が書かれています.
-        Alice と Bob は, これらのカードを使ってゲームを行います.
-        ゲームでは, Alice と Bob が交互に $1$ 枚ずつカードを取っていきます.
-        Alice が先にカードを取ります.
-        $2$ 人がすべてのカードを取ったときゲームは終了し, 取ったカードの数の合計がその人の得点になります.
-        $2$ 人とも自分の得点を最大化するように最適な戦略を取った時, Alice は Bob より何点多く取るか求めてください.
-    \end{quotation}
-\end{problem}
-
-この問題は人間にとっては簡単である。
-単純な貪欲法でよい。
-その時点で残っているカードの中から最大のものを選ぶことが誰にとっても最適である。
-つまり列 $A$ を降順にソートし ($1$ から数えて) 奇数番目の数の総和から偶数番目の数の総和を引いたものが答えである。
-計算量は $O(N \log N)$ となる。
-
-この問題を機械によって解くにはどうすべきだろうか？
-そもそも問題を機械に入力する時点ですでに自明ではない。
-単純には minimax 法のようにして、以下のように形式化できる。
-
-\begin{problem}[形式化された問題\ref{card-game-for-two}]
-    \label{card-game-for-two-formal}
-    整数の多重集合 \footnote{多重集合とは重複を許す集合のこと。それぞれの要素 $x$ からそれがいくつ含まれているか (重複度) を表す自然数 $m(x) \in \mathbb{N}$ への関数 $m : X \to \mathbb{N}$ のことだとして理解できる。} $A \in \mathbb{N}^\mathbb{Z}$ \footnote{$Y^X$ は $X$ から $Y$ への関数全体の集合 $\Set{ f | f : X \to Y }$ のことである。ただし計算不可能な関数などの面倒は考えないこととする} に対し関数 $f : \mathbb{N}^\mathbb{Z} \to \mathbb{Z}$ を
-    \[
-        f(A) = \begin{cases}
-            0 & (A = \emptyset) \\
-            \max \Set{ a - f(A \setminus \Set{ a }) | a \in A } & (A \ne \emptyset)
-        \end{cases}
-    \]
-    と定義する。
-    多重集合 $A$ が入力される。
-    値 $f(A)$ を出力せよ。
-\end{problem}
-
-このような式は複雑である。
-式の形だけを見ても (1.) 集合を引数とするような (2.) 再帰関数であって (3.) その漸化式に集合の最大値を得る操作を含むためである\footnote{展開すれば $N$ 段の $\max$ と $\min$ の交互の繰り返しになっている、つまりある種の $\Pi_N$ 文のような性質を持つと思うと難しさが分かりやすい。}。
-人間であってもこのような再帰的な式だけから「貪欲に取ればよい」という解法に至るのは手間がかかるはずである\footnote{このことから「この事態は適切な形式化ができていない証拠であり、形式言語の表現力がとぼしいことが原因である」とみることができるかもしれない。}。
-
-そしてこれに対し証明を与えるのはなお難しい。
-実際に証明を書き下してみると以下のようになる。
-機械的に解く場合は解法と同時に証明が出力されるようなものであるべきだが、これを自動で導出するのは困難だろう。
-
-\begin{proof}[問題\ref{card-game-for-two}の貪欲解の正当性の証明]
-    重複がある場合も以下の議論はほとんど同様である。
-    簡単のため、入力される重複集合に重複はないとする。
-    つまり問題は有限集合 $A \subseteq_\mathrm{fin} \mathbb{Z}$ が与えられるものとみなしてよい。
-
-    関数 $g : \Set{ A \subseteq \mathbb{Z} \mid A \text{~is finite} } \to \mathbb{Z}$ を
-    \[
-        g(A) = \begin{cases}
-            0 & (A = \emptyset) \\
-            \max A - f(A \setminus \Set{ \max A }) & (A \ne \emptyset)
-        \end{cases}
-    \] と定義する。
-    任意の $A$ に対し $f(A) = g(A)$ を示せば、貪欲解が最適であると言える。
-
-    集合 $A$ の大きさ $\lvert A \rvert \in \mathbb{N}$ に関する帰納法を用いる。
-    \begin{itemize}
-        \item $\lvert A \rvert \le 1$ のときは明らか。
-        \item $n$ 未満の場合の成立を仮定し $\lvert A \rvert = n \ge 2$ での場合を示す。
-            $a = \max A$ とする。
-            $b \in A$ であって $b - f(A \setminus \Set{ b }) \ge a - f(A \setminus \Set{ a })$ なものをとる。
-            $b = a$ を示せば $f(A) = g(A)$ であることが示せる。
-
-            帰納法の仮定から左辺は $b - f(A \setminus \Set{ b }) = b - g(A \setminus \Set{ b }) = b - a + g(A \setminus \Set{ a, b })$ である。
-            どんな $c \in A$ についても $c - f(A \setminus \Set{ c }) \le f(A)$ であることを使って、右辺は $a - f(A \setminus \Set{ a }) \ge a - b + f(A \setminus \Set{ a, b }) = a - b + g(A \setminus \Set{ a, b })$ である。
-            あわせると $b - a + g(A \setminus \Set{ a, b }) \ge a - b + g(A \setminus \Set{ a, b })$ が得られる。
-            これを整理すると $b \ge a$ が得られ、つまり $b = a$ である。
-    \end{itemize}
-\end{proof}
-
-\subsection{形式化する部分が問われている問題には役に立たない}
-
-こちらは手法の枠組みに起因する難しさである。
-「形式的に表現された式を自動で変形しアルゴリズム的な改善をする」ことは「そもそも形式化することが難しい」問題には無力である。
-
-たとえば ICPC 2019 年度国内予選の $5$ 問目 立方体表面パズル (\url{https://onlinejudge.u-aizu.ac.jp/challenges/sources/ICPC/Prelim/1636}) を見てみよう。
-問題文は長いので詳細は該当ページやその図解を直接見てほしいが、簡潔には以下のようなものである。
-
-\begin{problem}
-    \label{cube-surface-puzzle}
-    立方体表面パズルとは、次のようなパズルである:
-    \begin{itemize}
-        \item $1 \times 1 \times 1$ の大きさの単位立方体 $n^3 - (n - 2)^3$ 個で構成された $n \times n \times n$ の中空の立方体がある。
-            この立方体を $6$ 分割したもの (ピース) が与えられる。
-            これを組み立てて元の立方体を復元する遊びが立方体表面パズルである。
-    \end{itemize}
-    さて、立方体表面パズルの $6$ 個のピースが入力される。
-    ただし必ずしも立方体が復元できるものとは限らない。
-    立方体が復元できるならば復元した結果を、できないならできないと出力せよ。
-\end{problem}
-
-実際に解こうとしてみれば、この問題が「アルゴリズムを用いて計算量を落とすこと」でなくむしろ「問題文の内容を正確にプログラミング言語に翻訳すること」を問うていることが分かる。
-特に、この問題が始めて出題されたコンテストでは実行時間制限は実質 $1$ 時間程度であり、アルゴリズム的な工夫はほとんど不要であった。
-
-
-\section{自動で問題を解くプログラムは有用である}
-
-次のような用途が考えられる。
-
-\begin{enumerate}[label=(\arabic{enumi}.)]
-    \item 自分では解けない問題を解くために用いる。
-    \item 学習のために用いる。
-    \item 考察や実装の仮定で手間を省くために用いる。
-\end{enumerate}
-
-この節の議論の多くは「電卓があれば算数は不要か？」「Google などの検索エンジンが使えるのに単語を覚える必要はあるか？」のような議論と類似していることを注意しておく。
-
-\subsection{自分では解けない問題を解くために用いることは難しいだろう}
-
-まず (1.) について。
-ここまで議論してきたような方法で自動で競技プログラミングの問題を解くプログラムを、自分では解けないような問題を解くために用いることは難しいだろう。
-
-原因は次の $3$ つである。
-
-\begin{enumerate}[label=(\alph{enumi}.)]
-    \item 形式化する作業の難しさ
-    \item 機械的に解ける問題の判定の難しさ
-    \item コンテスト環境への影響
-\end{enumerate}
-
-今回の手法では問題を形式化することはユーザの役割である。
-一般に、なにか与えられたものを正確に読みとってその結果を形式的に (あるいは厳密に) 表現することは、表現される対象と表現のための手法への理解が必要である。
-そのような理解を持つ人間であれば、プログラムによって機械的に解けてしまうような問題 (つまり比較的単純な問題) の多くを手動で機械的に解くことができるはずである。
-たとえば $\max \Set{ f(X) | X \subseteq N \land \lvert X \rvert = M }$ のような表現を読み書きできるほど数学に慣れている人間であれば、$\lvert a \rvert = \max \Set{ a, -a }$ を使うような簡単な式変形にも同様に慣れているだろう。
-
-プログラムですべての問題が解けるわけではないので、ユーザは「問題が機械的に解けるのはどのような場合であるか」を大まかに判断できる必要がある。
-機械的に解けうる問題であっても入力の与え方次第では解けないことも多いので、この判断を行なえることはプログラムの利用のために必要である。
-しかしそのような判断ができるには、やはりユーザ自身の能力が要求される。
-
-コンテスト環境への影響も無視できない。
-問題を機械的に解くプログラムが十分に普及すれば、機械的には解けない問題のみが出題されるようになることは明らかである。
-
-\subsection{競技プログラミングの初心者にとっては、学習のために役に立つだろう}
-
-次に (2.) について。
-競技プログラミングの問題を解くプログラムは「競技プログラミングをする上で有用な等式や定理やデータ構造を集めたもの」であり、また、規則に従って変換を繰り返すことから「問題を解く過程をギャップの小さい変形の列として出力できる」という性質を持つ。
-これらは学習のためのリソースとして利用できるだろう。
-
-\subsection{競技プログラミングの上級者ならば、機械的には解けない問題の考察や実装の道具として用いることができる}
-
-最後に (3.) について。
-これが最も重要であり、主に意図される用途である。
-
-競技プログラミングの簡単な問題を解くプログラムがあったとしても、実際の難しい問題は人が解くしかないだろう。
-しかしそのような場合でも、難しい部分を人間が解決したあとに帰着されて残る簡単な部分は機械によって処理可能である。
-つまりわれわれは、問題のより本質的な部分にのみ注力することができるようになる。
-
-単に実装の手間を省くのみならず、考察の手段としても利用することができる。
-式を入力すればそれをアルゴリズムに改善した結果の計算量を出力してくれるシステムとしても利用できるからである。
-立てた式の計算量が瞬時に分かることは、高度なアルゴリズムの設計の効率化に寄与する。
-
-\subsection{これらの用途は総合的に、競技プログラミングの界隈のレベルの上昇に寄与する}
-
-(1.) により出題される問題の質が上昇し、(2.) と (3.) により多くの競技者の能力が上昇することが期待できる。
-これらから、機械的に問題を解くプログラムは競技プログラミングの界隈にとって有益であると言える。
-
-
-\section{この機械的な手法はどのような理論に基づくものか}
 
-\subsection{事前知識として何が必要か}
 
-今回の手法は主に数理論理学の、特に証明に関する範囲の知識に基づくものである。
-これに関する比較的平易な和書として、次の $2$ 冊をおすすめしておく。
 
-\begin{itemize}
-    \item \bibentry{ono-logic}
-    \item \bibentry{terui-computer-math}
-\end{itemize}
+\section{Related Research}
 
-実際の開発においては、型システムやコンパイラの実装についての理解も必要である。
-対象言語の設計には{\lambda}計算や集合論の知識も役に立つだろう。
-これには次の $3$ 冊を紹介しておく。
+一般のものであれば、以下のものが近いだろう。
 
 \begin{itemize}
-    \item \bibentry{tapl}
-    \item \bibentry{tiger-book}
-    \item \bibentry{kunen-foundation}
+    \item \href{https://oeis.org/}{オンライン整数列大辞典 (OEIS)} は整数列の巨大なデータベースである。
+        入出力が共に単一の整数であるような問題では、愚直解を書いて得られた整数列で OEIS を検索することで解法が判明することがある。
+    \item \href{https://www.wolframalpha.com/}{Wolfram|Alpha} は数学関連の質問応答システムである。
+        問題を解く過程で出てきた複雑な数式を Wolfram|Alpha に渡すことで解法が得られることがある。
+    \item 新井紀子らの\href{https://21robot.org/}{ロボットは東大に入れるか}プロジェクトは
+    \item \href{https://github.com/angr/angr}{angr} は CTF などで用いられるバイナリ解析フレームワークである。
+    \item DARPA の \href{https://www.darpa.mil/program/cyber-grand-challenge}{Cyber Grand Challenge} は CTF の問題を自動で
+    \item \href{https://copilot.github.com/}{GitHub Copilot} やこれに用いられている \href{https://openai.com/blog/openai-codex/}{OpenAI Codex} のような言語モデルは、自然言語の問題文からその愚直解を生成することができる。
+        Daniel Paleka (\href{https://codeforces.com/profile/valkyrie}{valkyrie}) による\href{https://codeforces.com/blog/entry/94353}{これを実際に利用してみての分析}が Codeforces の blog にある。
+    \item \href{https://github.com/borzunov/cpmoptimize}{borzunov/cpmoptimize} は Python の関数を行列累乗を用いて書き換える decorator である。
+        \href{https://kukuruku.co/post/automatic-algorithms-optimization-via-fast-matrix-exponentiation/}{これに関してのブログ記事}や\href{https://news.ycombinator.com/item?id=17592359}{これに関しての Hacker News のスレッド}には多くの関連するプロジェクトが見つかる。
 \end{itemize}
 
-アルゴリズムや競技プログラミングについての知識が、ドメイン知識として必要である。
-データ構造も数学に寄せて扱うので永続データ構造に関する知識もあるとよい。
-これには次の $2$ 冊をおすすめしておく。
+競技プログラミングでの利用を意図したものに限れば、以下のような事例がある。
 
 \begin{itemize}
-    \item \bibentry{arihon}
-    \item \bibentry{okasaki-data-structure}
+    \item 競技プログラミングの解法コードに貼り付けて利用するためのライブラリは広く開発されている。これらは最も素朴な形の「競技プログラミングの問題のソルバ」だと思うこともできるだろう。たとえば \href{https://github.com/beet-aizu/library}{beet-aizu/library} がある。
+    \item 個別の問題のソルバとしては \href{https://atcoder.jp/users/wata}{wata} による「Σ電卓」が知られている (\href{https://github.com/wata-orz/SigmaCalculator}{wata-orz/SigmaCalculator}, \href{https://wata-orz.hatenadiary.org/entry/20091223/1261582436}{Σ電卓 - てきとーな日記}) (2009 年)。
+    \item 実装には至っておらず構想のみであるが、一般の問題の解法の自動生成についての試みが \href{https://www.topcoder.com/members/cafelier/}{kinaba} によってなされている (\href{https://topcoder-g-hatena-ne-jp.jag-icpc.org/cafelier/20120204/1328332594.html}{SRM 531 Div2 250 - cafelier@SRM - TopCoder部} など) (2012 年)。
+    \item AtCoder Regular Contest のある A 問題の解法の完全自動生成が \href{https://atcoder.jp/users/mkotha}{mkotha} によって行われたことがある (\url{https://twitter.com/atcoder/status/538665089931296768}, \url{https://atcoder.jp/contests/arc030/submissions/286413}) (2014 年)。
+    \item 最適化などは含まれていないが、競技プログラミングでの利用を意図して作られた言語としては \href{https://atcoder.jp/users/LayCurse}{laycurse} による cLay がある (\href{http://rsujskf.s602.xrea.com/?cLay}{cLay概要（version 20201123-1） - ゲームにっき（仮）別館（仮）}) (207 年から)。
+    \item マラソンマッチなどでの利用を意図したプログラミング言語として \href{https://atcoder.jp/users/colun}{colun} による mmlang がある (\href{https://github.com/colun/mmlang}{colun/mmlang}) (2021 年から)。データ構造の差分の計算の自動導出機能を持つ。
 \end{itemize}
 
-一方で統計学に関連する知識は不要である。
-ここまでの議論から明らかなように、いま考えている手法は統計的手法ではない。
-ビッグデータは用いず、ディープラーニングは行わない、基本的に一切の学習を行わないシステムである。
-エキスパートシステムという名前で説明されるのが適切だろう。
-
-\subsection{推論を形式化した体系としてのシークエント計算を援用する}
-
-シークエント計算は単なる形式的な証明の体系としてのみならず、型推論や定理証明支援系のための道具としても利用されている。
-われわれの手法も、明示的にであれ暗黙的にであれシークエント計算に類似した構造を利用することになるだろう。
-これは「どのような値について計算が終わっているか」などの情報を保持することが重要であることによる。
-
-「式」や「型」がどのようなものであるかについては、事前に適切に定義をしておくとする。
-「式 $e$ は型 $T$ を持つ」という言明を $e \in T$ と書くことにする。
-
-\begin{definition}[シークエント]
-「言明の集合 $\Gamma = \Set{ e_0 \in T_0, \dots, e_{n - 1} \in T_{n - 1} }$ に含まれる式 $e_0, \dots, e_{n - 1}$ の値がすべて与えられているとき、型 $T$ を持つ式 $e$ が時間計算量 $O(f)$ で計算できる」という言明を $\Gamma \vdash e \in T \cap O(f)$ と書くこととする\footnote{言明を正確に表現できさえすれば具体的な記法は重要でないことに注意せよ。たとえば $R(\Gamma, e, T, f)$ や $\fbox{\begin{tabular}{|c|c|} \hline \Gamma & e \\ \hline T & f \\ \hline \end{tabular}}$ と書くということにしても、以下の議論にまったく影響はない}。
-このような形で書かれた言明をシークエントと呼ぶ。
-\end{definition}
-
-たとえば「自然数 $K \in \mathbb{N}$ と関数 $f \in \mathbb{Z}^\mathbb{N} $ が与えられているとき式 $\sum_{i < n} f(i)$ の値は整数であって計算量 $O(K)$ で計算できる」という言明は $K \in \mathbb{N}, f \in \mathbb{Z}^\mathbb{N}  \vdash \sum_{i < n} f(i) \in \mathbb{Z} \cap O(K)$ というシークエントで書かれる。
-あるシークエントが表現する言明が正しいとき、そのシークエントを妥当であるという。
-
-\begin{definition}[推論規則]
-「シークエント $\Gamma \vdash e \in T \cap O(f)$ が妥当であるならば、シークエント $\Gamma' \vdash e' \in T' \cap O(f')$ も妥当である」という言明を
-\begin{center}
-    \begin{prooftree}
-        \hypo{ \Gamma \vdash e \in T \cap O(f) }
-        \infer1{ \Gamma' \vdash e' \in T' \cap O(f') }
-    \end{prooftree}
-\end{center}
-と書くこととする。
-ただし条件となるシークエントは複数 ($0$ 以上の有限個) あってもよく、その場合は
-\begin{center}
-    \begin{prooftree}
-        \hypo{ \Gamma_0 \vdash e_0 \in T_0 \cap O(f_0) }
-        \hypo{ \Gamma_1 \vdash e_1 \in T_1 \cap O(f_1) }
-        \hypo{ \dots }
-        \hypo{ \Gamma_{n - 1} e_{n - 1} T_{n - 1} O(f_{n - 1}) }
-        \infer4{ \Gamma' \vdash e' \in T' \cap O(f') }
-    \end{prooftree}
-\end{center}
-のように書く。
-このような形で書かれた言明を推論規則と呼ぶ。
-\end{definition}
-
-分かりやすさのために推論規則の名前を横棒の右に書いて示すことがある。
-条件が $0$ 個の推論規則は、始式あるいは公理とも呼ばれる。
-ある推論規則が表現する言明が正しいとき、その推論規則は健全であるという。
-
-たとえば「自然数 $n \in \mathbb{N}$ と関数 $f : \mathbb{N} \to \mathbb{Z}$ が与えられているとする。このとき $- \min_{i < n} f(i)$ が $O(N)$ で計算できるならば、$\max_{i < n} - f(i)$ も $O(N)$ で計算できる」という言明は
-\begin{center}
-    \begin{prooftree}
-        \hypo{ n \in \mathbb{N}, f \in \mathbb{Z}^\mathbb{N} \vdash - \min_{i < n} f(i) \in \mathbb{Z} \cap O(N) }
-        \infer1{ n \in \mathbb{N}, f \in \mathbb{Z}^\mathbb{N} \vdash \max_{i < n} - f(i) \in \mathbb{Z} \cap O(N) }
-    \end{prooftree}
-\end{center}
-と書かれる。
-「式 $e$ が $O(f)$ で計算でき、$e$ の計算結果があれば式 $e'$ が $O(f')$ で計算できるならば、全体としては式 $e'$ は $O(f + f')$ で計算できる」という言明は
-\begin{center}
-    \begin{prooftree}
-        \hypo{ \Gamma \vdash e \in T \cap O(f) }
-        \hypo{ e \in T, \Gamma \vdash e' \in T' \cap O(f') }
-        \infer2[cut]{ \Gamma \vdash e' \in T' \cap O(f + f') }
-    \end{prooftree}
-\end{center}
-と書ける\footnote{この形の規則はカット規則と呼ばれる}。
-
-\begin{definition}[推論木]
-ある判断したいシークエントから始めて、推論規則を逆向きに使って木を組み上げることを考える。
-そのような木を推論木と呼ぶ。
-推論規則の集合を固定した上で、次のように定義される。
-
-\begin{enumerate}[label=(\arabic{enumi}.)]
-    \item シークエント $S$ は推論木である。そのような推論木の終式とはシークエント $S$ 自体である。
-    \item 未完成の推論木 $\Delta_0, \dots, \Delta_{n - 1}$ に対し、その終式 $S_0, \dots, S_{n - 1}$ を前提としシークエント $S'$ を結論とする推論規則があるならば、これらを
-        \begin{prooftree}
-            \hypo{ \vdots }
-            \infer[no rule]1{ S_0 }
-            \hypo{ \cdots }
-            \hypo{ \vdots }
-            \infer[no rule]1{ S_{n - 1} }
-            \infer3{ S' }
-        \end{prooftree}
-        と繋げて書いたものも推論木である。
-        その終式とはシークエント $S'$ である。
-\end{enumerate}
-
-\end{definition}
-
-推論木の定義の (1.) を使わず構成された推論木を完成した推論木と呼ぶ。
-推論規則が適切であれば完成した推論木の終式は妥当なシークエントであり、推論木を逆から読むと形式的な証明とみなせる。
-また、そこからプログラムを抽出することができる。
-
-\subsection{シークエント計算の利用の具体例}
-
-たとえば AtCoder Beginner Contest 134: C - Exception Handling (\url{https://atcoder.jp/contests/abc134/tasks/abc134_c}) を例に見てみよう。
-これは次のように形式化できる問題である。
-
-\begin{problem}[形式化された Exception Handling]
-    \label{exception-handling-formal}
-    自然数 $N$ と長さ $N$ の数列 $A$ が与えられる。
-    関数 $f(i) = \max \Set{ A(j) | j < n \land j \ne i }$ の値を $O(N)$ ですべて計算せよ。
-\end{problem}
-
-これは終式を $N \in \mathbb{N},~ A \in \mathbb{N}^N \vdash \lambda i. \max \Set{ A(j) | j < n \land j \ne i }  \in \mathbb{N}^N \cap O(N)$ とする完成した推論木を構築せよという問題に等しい。
-次の推論規則が用意されているとする。
-以下の推論規則はすべて健全である。
-
-\begin{itemize}
-
-    \item 「式 $e$ が $O(f)$ で計算でき、$e$ の計算結果 $a$ があれば式 $e'$ が $O(f')$ で計算できるならば、全体としては式 $e'$ は $O(f + f')$ で計算できる」
-        \begin{center}
-            \begin{prooftree}
-                \hypo{ \Gamma \vdash e \in T \cap O(f) }
-                \hypo{ e,~ \Gamma \vdash e' \in T \cap O(f') }
-                \infer2[cut]{ \Gamma \vdash e' \in T \cap O(f + f') }
-            \end{prooftree}
-        \end{center}
-
-    \item 「$\max \Set{ \max \Set{ e(j) | j < i }, \max \Set{ e(j) | i < j < n } }$ が計算できるならば  $\max \Set{ e(j) | j < n \land j \ne i }$ も計算できる」
-        \begin{center}
-            \begin{prooftree}
-                \hypo{ \Gamma \vdash \max \Set{ \max \Set{ e | j < i }, \max \Set{ e | i < j < n } } \in T \cap O(f) }
-                \infer1[split-$\max$]{ \Gamma \vdash \max \Set{ e | j < n \land j \ne i } \in T \cap O(f) }
-            \end{prooftree}
-        \end{center}
-
-    \item 「自然数 $N$ 未満の自然数 $i < N$ を使って値 $e(i) \in T$ が $O(f)$ で計算できるならば、$O(N)$ で関数 $e : N \to T$ のすべての値を計算できる」
-        \begin{center}
-            \begin{prooftree}
-                \hypo{ N \in \mathbb{N},~ i \in N, \Gamma \vdash e \in T \cap O(f) }
-                \infer1[$\to$右]{ \Gamma \vdash \lambda i. e \in T \cap O(N f) }
-            \end{prooftree}
-        \end{center}
-
-    \item 「関数 $A : N \to \mathbb{Z}$ のすべての値が計算されているとき関数 $\lambda i. \max \Set{ A(j) | j < i }$ は $O(N)$ ですべての値を計算できる」
-        \begin{center}
-            \begin{prooftree}
-                \infer0{ N \in \mathbb{N},~ A \in \mathbb{Z}^N \vdash \lambda i. \max \Set{ A(j) | j < i } \in \mathbb{Z}^N \cap O(N) }
-            \end{prooftree}
-        \end{center}
-
-    \item 「関数 $A : N \to \mathbb{Z}$ のすべての値が計算されているとき関数 $\lambda i. \max \Set{ A(j) | i < j < N }$ は $O(N)$ ですべての値を計算できる」
-        \begin{center}
-            \begin{prooftree}
-                \infer0{ N \in \mathbb{N},~ A \in \mathbb{Z}^N \vdash \lambda i. \max \Set{ A(j) | i < j < N } \in \mathbb{Z}^N \cap O(N) }
-            \end{prooftree}
-        \end{center}
-
-    \item 「$\max \Set{ l(i), r(i) }$ のような自明な式は $O(1)$ で計算できる」
-        \begin{center}
-            \begin{prooftree}
-                \infer0{ i \in N,~ l = \ldots,~ r = \ldots,~ \Gamma \vdash & \max \Set{ l(i), r(i) } \in \mathbb{Z} \cap O(1) }
-            \end{prooftree}
-        \end{center}
-
-\end{itemize}
-
-$\Gamma = \Set{ N \in \mathbb{N}, A \in \mathbb{N}^N }$ と書くことにし、これらの推論規則を使えば問題\ref{exception-handling-formal}のシークエントを終式とする完成した推論木が図\ref{proof-tree}のように書ける。
-そして、これらの推論規則がどのようにして健全であったかに基づいて、推論木からプログラムを復元できる。
-実際、たとえばカット規則「式 $e$ が $O(f)$ で計算でき、$e$ の計算結果 $a$ があれば式 $e'$ が $O(f')$ で計算できるならば、全体としては式 $e'$ は $O(f + f')$ で計算できる」はつまり「まず $e$ を計算し、それを使って $e'$ を計算する」ようなプログラムの断片を指示している。
-
-\begin{landscape}
-    \begin{figure}[p]
-        \label{proof-tree}
-        \begin{center}
-            \scalebox{0.9}{
-                \begin{prooftree}[rule margin=2ex]
-                    \infer0{ \Gamma \vdash \lambda i. \max \Set{ A(j) | j < i } \in \mathbb{N}^N \cap O(N) }
-                    \infer0{ l = \ldots,~ \Gamma \vdash \lambda i. \max \Set{ A(j) | i < j < N } \in \mathbb{N}^N \cap O(N) }
-                    \infer0{ i \in N,~ l = \ldots,~ r = \ldots,~ \Gamma \vdash & \max \Set{ l(i), r(i) } \in \mathbb{N} \cap O(1) }
-                    \infer1[$\to$右]{ l = \ldots,~ r = \max \Set{ A(j) | i < j < N },~ \Gamma \vdash & \lambda i. \max \Set{ l(i), r(i) } \in \mathbb{N}^N \cap O(N) }
-                    \infer2[cut]{ l = \max \Set{ A(j) | j < i },~ \Gamma \vdash & \lambda i. \max \Set{ l(i), \max \Set{ A(j) | i < j < n } } \in \mathbb{N}^N \cap O(N) }
-                    \infer2[cut]{ \Gamma \vdash & \lambda i. \max \Set{ \max \Set{ A(j) | j < i }, \max \Set{ A(j) | i < j < N } } \in \mathbb{N}^N \cap O(N) }
-                    \infer1[split-$\max$]{ \Gamma \vdash & \lambda i. \max \Set{ A(j) | j < N \land j \ne i } \in \mathbb{N}^N \cap O(N) }
-                \end{prooftree}
-            }
-        \end{center}
-        \caption{問題\ref{exception-handling-formal}に関する推論木}
-    \end{figure}
-\end{landscape}
-
-
-\subsection{利用可能な既存のソルバについて}
-
-個別的に解ける問題のクラスがいくつか知られている。
-
-\begin{enumerate}[label=(\arabic{enumi}.)]
-    \item データ構造によるもの
-    \item 線型計画問題
-    \item 燃やす埋める問題
-    \item 正規表現に関連するもの
-    \item 構文解析に関連するもの
-    \item Robinson 算術の式として書かれるもの
-    \item 実閉体の言語の式として書かれるもの
-    \item 数列に関連するもの
-\end{enumerate}
-
-(1.) のような、データ構造を利用できる問題はその汎用性から重要である。
-利用可能であるかどうかの判定が比較的容易であり、他のソルバと違ってユーザが陽に指定しなくても自然に利用しやすいだろう。
-segment tree や convex hull trick のような汎用的なデータ構造や wavelet matrix や van Emde Boas tree や top tree などの強力なデータ構造がすべて自動で利用されるようにしておくべきである。
-
-(2.) の線型計画問題は有名な問題クラスである。
-単体法や Karmarkar のアルゴリズムなど解ける。
-(3.) は競技プログラミングのコミュニティ内で特有の呼称であり、Project Selection Problem とも呼ばれる。
-整理すると「$x_0 \land \dots \land x_{s - 1} \to x_s \lor \dots \lor x_{s + t - 1}$ の形の命題論理式と自然数の対の集合 $\Set{ (\varphi_0, c_0), \dots, (\varphi_{n-1}, c_{n-1}) }$ が与えられる。付値 $v : \mathrm{PropVar} \to \Set{ \top, \bot }$ に対する関数 $f(v) = \sum_{v(\varphi_i) = \bot} c_i$ を最小化する付値 $v$ を求めよ」という形の問題のクラスに等しい。少なくない問題をこれに帰着させることができ、最大流アルゴリズムで解ける。
-
-(4.) の正規表現は扱いやすい対象のひとつである。
-たとえば「ある正規表現 $\gamma$ に受理されるような文字列の個数を数えよ」と等しい問題はしばしば出題され、これは syntactic monoid \cite{hopcroft} などを使えば解ける。
-(5.) はよりやさしい。構文解析については Lex や Yacc のようなツールが整備されており、これを利用することができる。
-
-(6.), (7.) は量化子除去アルゴリズムを用いて自明な形に変換可能である。
-国立情報学研究所の東ロボくんプロジェクトでも実際に用いられたそうである\cite{tourobo}。
-
-(8.) には OEIS と呼ばれるデータベース (The On-Line Encyclopedia of Integer Sequences®, \url{https://oeis.org/}) を利用することができる。
+一般の競技プログラミングの問題を解くソルバを目指しているものとしては、ある程度の形になっているものは見つけられていない。
 
 
-\bibliography{how-it-works}
-\bibliographystyle{junsrt}
+% \bibliography{how-it-works}
+% \bibliographystyle{junsrt}
 
 \end{document}
diff --git a/docs/latexmkrc b/docs/latexmkrc
new file mode 100644
index 00000000..00ba7a78
--- /dev/null
+++ b/docs/latexmkrc
@@ -0,0 +1,2 @@
+$pdf_mode = 4;  # use lualatex
+$bibtex = 'pbibtex %O %B';  # for junsrt
diff --git a/scripts/pre-commit b/scripts/pre-commit
index 0a722aae..7c112ce9 100755
--- a/scripts/pre-commit
+++ b/scripts/pre-commit
@@ -50,6 +50,14 @@ if git diff --staged --name-only | grep '\.py$'; then
         || exit 1
 fi
 
+# TeX
+if git diff --staged --name-only | grep '\.tex$'; then
+    chktex --version \
+        || { echo HINT: Please install chktex, e.g. '$ sudo apt install chktex'; exit 1; }
+    chktex --nowarn={1,2,8,11,12,13,36,39} $(git ls-files | grep '\.tex$') \
+        || exit 1
+fi
+
 # Other files
 for ext in yml yaml json md html mjs; do
     if git diff --staged --name-only | grep '\.'$ext'$'; then