# 研究目的

- 愚直にプログラムを書くと、冗長なコードができてしまい、実行時間も掛かってしまう

- この場合、コードに対してアルゴリズムを適応すると、実行が最適化され実行時間が減り、良いコードが作成できる

- しかし、世の中にはアルゴリズムが大量にあり、これをプログラマーが全て覚え、また適応できる場面を思いつくというのは不可能

- そのため、人が愚直に書いたコードに対してアルゴリズムを使用するコードに自動適用できるようにしたい

- この場合、アルゴリズム適用前と適用後で同じコードになっていることを証明するのは難しい。

- また、普通のプログラミング言語では、関数の遷移が自由であるため、アルゴリズムの適応を行うのは難しいと考える

- ここで、当研究室で開発している Gears Agda を用いる。
    - Gears Agdaとは当研究室で開発している Continuetion based C (CbC)の概念を取り入れた記法
    - 当研究室で開発しているCbCと、のgotoを使用して関数遷移を行う言語である。
    - gotoを用いて関数遷移をすることで、プログラムが一つの処理になる

- Garas Agdaで一度実装したプログラムの入力と出力が一致したアルゴリズムを適応する
    - これによりアルゴリズムの適応前後で仕様が変わっていないことを証明する