Skip to content

Latest commit

 

History

History
88 lines (56 loc) · 5.76 KB

DESIGN.md

File metadata and controls

88 lines (56 loc) · 5.76 KB
Raw

Design Doc

(The English version of this document: docs/DESIGN.md)

Objective

Jikka は競技プログラミングの問題を解くことそのものを自動化する。

Goals

  • 形式的な形で与えられた競技プログラミングの問題の解法を自動で生成する
  • 競技プログラミングにおける実装パートのうちで機械的に処理できる部分を機械的に処理する

Non-Goals

  • 自然言語で与えられた競技プログラミングの問題の解法を自動で生成すること
    • GPT-3 や GitHub Copilot に任せておけばよい

Background

競技プログラミングの問題の中には、機械的に解けるであろう問題が存在する。 全体が機械的に解けるということはない場合であっても、部分的になら機械的に解けるであろう問題は多い。 たとえば個々の式変形それ自体は自明な式変形を丁寧に行っていくことで解けるような問題である。これを自動化したい。

Overview

Jikka は競技プログラミングの問題を自動で解くソルバである。 「競技プログラミングの問題を自動で解く」といっても様々な種類のものが考えられるが、Jikka は特にこれを「最適化を伴うトランスパイラ」の形に落とし込んで実現する。 つまり Jikka はその概観としてはただのトランスパイラである。 Python のとても制限されたサブセットとして書かれたソースコードを受けとり、GHC の Core に似た内部言語の上で最適化を行い、最終的に C++ のソースコードを出力する。

さらに、実際のコンテスト中により実用的に利用しやすくするために「最適化を行う書き換え機能を提供する IDE プラグイン」としても利用できるようにする。 たとえばコード片を右クリックしてメニューから「この O(N²) のループを O(N) に書き換える」を選べばそのように書き換えてくれる。 Language Server Protocol を用いて実装され、言語は Python および C++ の両方に対応する。

Detailed Design

トランスパイラとして実装すること

Jikka はトランスパイラとして実装される。 これは開発も利用も簡単であるためである。 競技プログラミングの問題のソルバというは目標は壮大かつ曖昧すぎて、最初から完璧なものを作るのは不可能である。 であるので、まずは確実に実装可能ですでによく理解されているもの、つまりトランスパイラとしての実装から始めていくべきである。

IDE プラグインとして実装すること

Jikka は IDE プラグインとしても利用できる。 これは利用をより簡単で実用的にするためである。 大きなファイルを大きなファイルに変換するようなトランスパイラでは、どのような最適化が行われたのかが分かりにくい。 一方で小さなコード片を小さなコード片に書き換える IDE の機能であれば、どのような最適化が行われたのかが分かりやすく、ユーザにとってより制御しやすい。

入力言語には主に Python を用いる

以下の 2 点を理由として、入力言語には Python のサブセットを用いる。

  1. 利用しやすい: 学習しやすく、書きやすい。Python は広く普及していてかつそこそこ高級な言語である
  2. 開発しやすい: 言語機能を制限すればコンパイラで扱いやすい。本物の Python との差分は未定義動作という形で吸収すればよい

言語機能は大きく制限し、静的型付け言語とする。 副作用はある種の糖衣構文としてのみ残し、意味論的には存在しない。

入力言語に独自の新しいプログラミング言語を用いることはしない

以下の 2 点を理由として、入力言語に独自言語を用いることは避ける。 それぞれ Python を用いる理由の裏となっている。

  1. 利用しにくい: 独自言語であると、ユーザはその言語を新規に覚える必要がある。たいていのユーザにとって新しい言語を覚えることはかなりの負担である
  2. 開発しにくい: 独自言語であると、開発者はその言語のドキュメントを丁寧に書く必要がある。仕様が明確であることや解説が豊富にあることはプログラミング言語の重要な機能性のひとつである

出力言語には主に C++ を用いる

理由は以下の 2 点である。

  1. 利用しやすい: 競プロという用途において柔軟な利用が可能になる
  2. 開発しやすい: 定数倍最適化を心配する必要がない

Metrics Considerations

適切な仮定の下で「AtCoder 上でのレート」という形で性能評価が可能である。 また「AtCoder Beginner Contest などの問題のうち何割が解ける」などの形での評価も可能だろう。

Testing Plan

競技プログラミングにおいては効率良く実行できる安定した end-to-end テストが簡単に書けるため、これを利用するのがよいだろう。 つまり、俗に「verify する」と呼ばれる、実際の競技プログラミングの問題に対して利用して AC を確認するという形式のテストである。

また、これを行うための専用のオンラインジャッジも用意されている: https://judge.kimiyuki.net/