kmyk-jikka · kmyk · Sep 12, 2021 · Sep 12, 2021 · Sep 12, 2021
diff --git a/README.md b/README.md
@@ -71,7 +71,7 @@ For developpers:
   - 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)
   - How it works and related theories / 動作原理や関連する理論
-- [docs/DESIGN.md](https://github.com/kmyk/Jikka/blob/master/docs/DESIGN.md) (Japanese)
+- [docs/DESIGN.md](https://github.com/kmyk/Jikka/blob/master/docs/DESIGN.md)
   - The policy of designs / 実装方針
 - [docs/internal.md](https://github.com/kmyk/Jikka/blob/master/docs/internal.md)
   - The overview of internal processes / 内部の処理の流れ

diff --git a/docs/DESIGN.ja.md b/docs/DESIGN.ja.md
@@ -0,0 +1,88 @@
+# Design Doc
+
+(このドキュメントの日本語バージョン: [docs/DESIGN.ja.md](https://github.com/kmyk/Jikka/blob/master/docs/DESIGN.ja.md))
+
+## Objective
+
+Jikka automates the very process of solving problems of competitive programming.
+
+## Goals
+
+- Automatically generating solutions to competition programming problems given in a formal form
+- Mechanically processing some implementation parts of competition programming
+  - In practical use, it aims for a position similar to [OEIS](https://oeis.org/) and [Wolfram&#x7c;Alpha](https://www.wolframalpha.com/).
+
+## Non-Goals
+
+- Automatically generating solutions to competition programming problems given in natural language
+  - Let GPT-3, GitHub Copilot, etc. do this for you.
+
+## Background
+
+There are some problems in competitive programming that can be solved mechanically.
+Even if the whole problem cannot be solved mechanically, there are many problems that can be solved partially mechanically.
+For example, there are problems that can be solved by carefully transforming the given formula, which each transformation itself is trivial.
+We want to automate this.
+
+## Overview
+
+Jikka is an automatic solver for problems of competitive programming.
+We can think many possible forms of automatic solvers, but Jikka is implemented especially as a transpiler doing optimization.
+In other words, Jikka is just a transpiler in its overview.
+It takes source code of a very restricted subset of Python as input, optimizes it in an internal language similar to GHC's Core, and finally writes source code of C++ as output.
+
+In addition, Jikka can be used as an IDE plugin that provides rewriting functions for optimization, for more practical use during real contests.
+For example, by right-clicking on a snippet of code and selecting "Rewrite this O(N²) loop to O(N)" from the menu, the code will be rewritten as such.
+It is implemented using the Language Server Protocol, and supports both Python and C++ languages.
+
+## Detailed Design
+
+### Implemented as a transpiler
+
+Jikka is implemented as a transpiler, because it is easy to develop and use.
+The goal of a solver for competitive programming problems is too ambitious and vague to create a perfect one from the beginning.
+Therefore, we should start with an easy-to-implement and already well-understood thing, i.e., a transpiler.
+
+### Implemented as IDE plugin
+
+Jikka is also available as an IDE plugin.
+This makes it easier to use in practice.
+With a transpiler that converts a large file to a large file, it is difficult to understand what kind of optimization has been done.
+On the other hand, with the IDE's function that rewrites a small snippet of code into a small snippet of code, it is easier for the user to understand and control what kind of optimization has been done.
+
+### Use Python for input
+
+We will use a subset of Python as input, due to the following two reasons:
+
+1. easy to use: easy to learn and write; Python is a widely used and reasonably expensive language.
+2. easy to develop: easy to handle with a compiler, if we limit the features. The differences from real Python can be absorbed in the form of undefined behaviors.
+
+We largely limit the language features, and makes it a statically typed language.
+Side effects are left only as some kind of syntax suger, and removed in its core semantics.
+
+### Don't use a new own language for input
+
+We avoid using a new own language as input, due to the following two reasons.
+Each of these is an inverse of the reason for using Python:
+
+1. difficult to use: A new own language requires the user to learn the language anew. For most users, learning a new language is a significant burden.
+2. difficult to develop: A new own language requires the developer to carefully write documentation for the language. Clear specifications and plenty of explanations are one of the important features of a programming language.
+
+### Use C++ for output
+
+There are two reasons:
+
+1. ease of use: flexible in the context of competitive programming
+2. easy to develop: no need to worry about constant-factor optimization
+
+## Metrics Considerations
+
+Under appropriate assumptions, it is possible to evaluate performance in terms of rating on AtCoder.
+It may also be possible to evaluate performance in terms of how many of the problems in the AtCoder Beginner Contest can be solved.
+
+## Testing Plan
+
+In competition programming, it is easy to write fast and stable end-to-end tests, so we use them.
+This is a form of testing that is commonly referred to as "verifying", in which you check the AC by using it against real problems of competition programming.
+
+There are also dedicated online judges for this purpose: <https://judge.kimiyuki.net/>
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
@@ -1,77 +1,56 @@
 # Design Doc
 
+(The English version of this document: [docs/DESIGN.md](https://github.com/kmyk/Jikka/blob/master/docs/DESIGN.md))
+
 ## Objective
 
-Jikka は、競技プログラミングの問題を解く行為そのものを自動化するツールである。
-特にこれを「最適化を伴うトランスパイラ」の形に落とし込んで実現する。
+Jikka は競技プログラミングの問題を解くことそのものを自動化する。
 
 ## Goals
 
-- 形式的な形で与えられた競技プログラミングの問題の解法を自動で生成すること。またこれによりユーザのレートを上げること
-- 競技プログラミングにおける機械的に処理できる部分を機械的に処理することによって、機械的には処理できないより本質的でおもしろい部分に人間が集中できるようにすること
+- 形式的な形で与えられた競技プログラミングの問題の解法を自動で生成する
+- 競技プログラミングにおける実装パートのうちで機械的に処理できる部分を機械的に処理する
+  - 実用的には [OEIS](https://oeis.org/) や [Wolfram&#x7c;Alpha](https://www.wolframalpha.com/) のような立ち位置を目指す
 
 ## Non-Goals
 
 - 自然言語で与えられた競技プログラミングの問題の解法を自動で生成すること
-- 競技プログラミングにおける機械的に処理できる部分を機械的に処理することによって、競技プログラミングのおもしろさを破壊すること
+  - GPT-3 や GitHub Copilot に任せておけばよい
 
 ## Background
 
 競技プログラミングの問題の中には、機械的に解けるであろう問題が存在する。
 全体が機械的に解けるということはない場合であっても、部分的になら機械的に解けるであろう問題は多い。
-たとえば、個々の式変形それ自体は自明な式変形を丁寧に行っていくことで解けるような問題である。これを自動化したい。
+たとえば個々の式変形それ自体は自明な式変形を丁寧に行っていくことで解けるような問題である。これを自動化したい。
 
 ## Overview
 
-Jikka はその概観としてはただのトランスパイラである。
+Jikka は競技プログラミングの問題を自動で解くソルバである。
+「競技プログラミングの問題を自動で解く」といっても様々な種類のものが考えられるが、Jikka は特にこれを「最適化を伴うトランスパイラ」の形に落とし込んで実現する。
+つまり Jikka はその概観としてはただのトランスパイラである。
 Python のとても制限されたサブセットとして書かれたソースコードを受けとり、GHC の Core に似た内部言語の上で最適化を行い、最終的に C++ のソースコードを出力する。
 
-## Detailed Design
-
-### 競技プログラミングの問題を解く過程は「形式化」「考察」「実装」に分けられる
-
-競技プログラミングの問題を解く過程は以下の 3 ステップに大別できる。
-
-1.  形式化: 自然言語で与えられた問題を解釈し、数学的で形式的な問題として整理する
-2.  考察: 数学的で形式的な問題に対し、数学的で抽象的な解法を考案する
-3.  実装: 数学的で抽象的な解法を、計算機における具体的な実装として記述する
-
-競技プログラミングの (すくなくとも AtCoder で出題されるような問題の) 中心であり最もおもしろくかつ難しい部分は「考察」の部分であると考えられている。
-しかしこの「考察」にも、一定の知識があれば機械的に可能であるような部分は多く含まれている。
-Jikka はそのような機械的な考察を処理する。
-
-このような「考察の自動化」について考察は [docs/how-it-works.pdf](https://github.com/kmyk/Jikka/blob/master/docs/how-it-works.pdf) により詳しい説明がある。
+さらに、実際のコンテスト中により実用的に利用しやすくするために「最適化を行う書き換え機能を提供する IDE プラグイン」としても利用できるようにする。
+たとえばコード片を右クリックしてメニューから「この O(N²) のループを O(N) に書き換える」を選べばそのように書き換えてくれる。
+Language Server Protocol を用いて実装され、言語は Python および C++ の両方に対応する。
 
-### 「考察」の自動化を実現する方法は「エキスパートシステム」「自動定理証明器」「コンパイラ」などに分けられるだろう
-
-競技プログラミングの問題を自動で (あるいは半自動で) 解くソルバを作りたいと考えたとき、仕様や設計の選択肢の方向は大きく分けて次のみっつであろう:
-
-1.  エキスパートシステム / DSL 処理系 / データベース / etc. (例: WolframAlpha, PostgreSQL, OEIS, GLPK, Z3, Akinator, ...)
-2.  自動定理証明器 / 定理証明支援系 (例: Otter, Coq, Agda, ...)
-3.  コンパイラ / トランスパイラ (例: Haskell, F#, Rust, ...)
-
-(1.) は最も直接的なものである。このような方向のソルバは「形式的に書かれた競プロの問題を入力とし、解法コードを出力する」ものだろう。
-問題を直接形式化したかなり高級な表現を受けとることになるはずである。
-たとえば [AtCoder Regular Contest 066: D - Xor Sum](https://atcoder.jp/contests/arc066/tasks/arc066_b) であれば `given N: int; assume: 1 <= N <= 10^18; count (u, v): int * int s.t. 0 <= u <= N, 0 <= v <= N, (exists (a, b): int * int. a xor b = u /\ a + b = v);` のような入力になるかもしれない。
-(1.) の方向のソルバであって (2.) や (3.) から遠いものを考えると、性質のよい問題のクラスに対する個別のソルバの集合体としてのソルバや、問題とその解法のデータベースシステムという形になるだろうと思われる。
-
-(2.) は理論的に整理したものである。このような方向のソルバは「計算可能関数のある表現を入力とし、その関数のよい計算量についての構成的証明を出力する」ものである。
-高度な考察を自動で行いたいと思うと、(2.) の方向のソルバも最終的にはこれに近づくものと予想している。
+## Detailed Design
 
-(3.) は最も現実的なものである。このような方向のソルバは「通常のプログラミング言語のソースコードを入力とし、計算量的な最適化がなされた機械語やその他の言語のソースコードを出力とする」ようなものである。
-実装においても利用においても簡単であることが利点となる。
+### トランスパイラとして実装すること
 
-また、上記の (1.), (2.), (3.) とは別に、個別の問題のクラス (線形計画問題, 制約充足問題, ...) に対するソルバがそれぞれ作られることもあるだろう。
-そのようなソルバの解ける問題の範囲はかなり限られたものとなる。
-しかし個別の問題に対するソルバは理解しやすいという点で優れている。つまり、「ある問題を解くことができるかできないか」「得られる解法はどのような性質を持つか」などが分かりやすく、扱いやすい。
+Jikka はトランスパイラとして実装される。
+これは開発も利用も簡単であるためである。
+競技プログラミングの問題のソルバというは目標は壮大かつ曖昧すぎて、最初から完璧なものを作るのは不可能である。
+であるので、まずは確実に実装可能ですでによく理解されているもの、つまりトランスパイラとしての実装から始めていくべきである。
 
-### トランスパイラとして実装される
+### IDE プラグインとして実装すること
 
-トランスパイラとして実装される
-開発と利用が簡単であるためである。
-目標が壮大すぎて最初から完璧なものを作るのは不可能であるため、まずは確実に実装可能な部分から始めていくのがよいだろう。
+Jikka は IDE プラグインとしても利用できる。
+これは利用をより簡単で実用的にするためである。
+大きなファイルを大きなファイルに変換するようなトランスパイラでは、どのような最適化が行われたのかが分かりにくい。
+一方で小さなコード片を小さなコード片に書き換える IDE の機能であれば、どのような最適化が行われたのかが分かりやすく、ユーザにとってより制御しやすい。
 
-### 入力言語には Python を用いる
+### 入力言語には主に Python を用いる
 
 以下の 2 点を理由として、入力言語には Python のサブセットを用いる。
 
@@ -89,12 +68,12 @@ Jikka はそのような機械的な考察を処理する。
 1.  利用しにくい: 独自言語であると、ユーザはその言語を新規に覚える必要がある。たいていのユーザにとって新しい言語を覚えることはかなりの負担である
 2.  開発しにくい: 独自言語であると、開発者はその言語のドキュメントを丁寧に書く必要がある。仕様が明確であることや解説が豊富にあることはプログラミング言語の重要な機能性のひとつである
 
-### 出力言語には C++ を用いる
+### 出力言語には主に C++ を用いる
 
 理由は以下の 2 点である。
 
 1.  利用しやすい: 競プロという用途において柔軟な利用が可能になる
-2.  開発しやすい: 局所的な最適化をまったく回避できる
+2.  開発しやすい: 定数倍最適化を心配する必要がない
 
 ## Metrics Considerations
 
@@ -103,14 +82,7 @@ Jikka はそのような機械的な考察を処理する。
 
 ## Testing Plan
 
-効率良く実行できる安定した end-to-end テストが簡単に書けるため、これを利用するのがよいだろう。
-つまり、俗に「verify する」と呼ばれる、実際の競技プログラミングの問題に対して利用して AC を確認するという形式のテストに類似したものが可能である。
-
-## 先行事例
-
-競技プログラミングでの利用を意図したものに限れば、以下のような先行事例がある。
+競技プログラミングにおいては効率良く実行できる安定した end-to-end テストが簡単に書けるため、これを利用するのがよいだろう。
+つまり、俗に「verify する」と呼ばれる、実際の競技プログラミングの問題に対して利用して AC を確認するという形式のテストである。
 
-- 個別の問題のソルバとしては [wata](https://atcoder.jp/users/wata) による「Σ 電卓」が知られている ([wata-orz/SigmaCalculator](https://github.com/wata-orz/SigmaCalculator), [Σ 電卓 - てきとーな日記](https://wata-orz.hatenadiary.org/entry/20091223/1261582436)) (2009 年)。
-- 実装には至っておらず構想のみであるが、一般の問題の解法の自動生成についての試みが [kinaba](https://www.topcoder.com/members/cafelier/) によってなされている ([SRM 531 Div2 250 - cafelier@SRM - TopCoder 部](https://topcoder-g-hatena-ne-jp.jag-icpc.org/cafelier/20120204/1328332594.html) など) (2012 年)。
-- AtCoder Beginner Contest のある A 問題の解法の完全自動生成が [mkotha](https://atcoder.jp/users/mkotha) によって行われたことがある (<https://twitter.com/atcoder/status/538665089931296768>, <https://atcoder.jp/contests/arc030/submissions/286413>) (2014 年)。
-- 最適化などは含まれていないが、競技プログラミングでの利用を意図して作られた言語としては [laycurse](https://atcoder.jp/users/LayCurse) による cLay がある ([cLay 概要（version 20201123-1） - ゲームにっき（仮）別館（仮）](http://rsujskf.s602.xrea.com/?cLay)) (2107 年から)。
+また、これを行うための専用のオンラインジャッジも用意されている: <https://judge.kimiyuki.net/>