Mercurial > hg > Papers > 2020 > soto-midterm
annotate tex/future.tex @ 8:27a6616b6683
fix
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Mon, 14 Sep 2020 19:58:10 +0900 |
parents | |
children | a8bc8c6b48bd |
rev | line source |
---|---|
8 | 1 \section{今後の課題} |
2 今後の課題として、以下が挙げられる。 | |
3 赤黒木の基本操作として insert や delete が挙げられる。 | |
4 通常は、再代入などを用いて実装を行うと思われるが、agda が変数への代入を許していないため、 | |
5 操作後の赤黒木を再構成するように実装を行う必要がある。 | |
6 その際にどこの状態の検証を行うかが課題になっている。 | |
7 | |
8 先行研究にて、 | |
9 個々の Code Gear の条件を書いてそれを接続することは agda で実装されている。 | |
10 しかし、接続された条件が健全であるか証明されていない。 | |
11 | |
12 今後はこの接続された条件の健全性の証明からしていく。 |