2015 Fiscal Year Research-status Report
関数型の視点からの効率的可逆シミュレーションおよび可逆プログラミング方法論の拡張
Project/Area Number |
25730049
|
Research Institution | Nanzan University |
Principal Investigator |
横山 哲郎 南山大学, 理工学部, 准教授 (80456631)
|
Project Period (FY) |
2013-04-01 – 2017-03-31
|
Keywords | 可逆計算 / 可逆プログラミング言語 / 可逆チューリング機械 / 可逆シミュレーション / 流れ図 / 並び替えアルゴリズム / Janus / 構造化定理 |
Outline of Annual Research Achievements |
本研究では、可逆プログラミング言語の設計、および可逆プログラミング方法論の確立を目的としている。本年度は、この2点についてそれぞれ成果を得ることができた。 可逆プログラミング言語の設計では、構造化・非構造化可逆流れ図の理論を整備した。どちらの流れ図も可逆チューリング機械(RTM: reversible Turing machine)と同等の表現力があることを示し、流れ図を素直に反映した言語を設計し形式化し、プログラム逆変換器や翻訳器を設計した。実際に、ダイクストラのpermutation encodingやRTMシミュレーションを実現することができた。可逆流れ図における考え方は命令型可逆プログラミング言語の多くで共通であり今後の応用が期待される。 可逆プログラミング方法論では、基本的なアルゴリズムとして知られている並び替えに焦点を当てて、計算資源(実行時間・メモリ使用量)を効率的に使用する方法について研究を進めた。可逆シミュレーションは、漸近的計算量が悪化せずメモリ使用量が関数gでおさえられることをfaithfulと、faithfulなシミュレーションの中でgが(漸近的に)最適なものをhygienicと名付けた。これらの尺度で基本的な並び替えアルゴリズム(挿入整列法、バブルソート、選択整列法、クイックソート、マージソート)を効率的に実装する方法を報告することができた。可逆シミュレーションをすることで増えてしまったデータ(ゴミ)の表現形式は、効率的に互いに変換することができた。 これらの研究では、動的にメモリを確保する機構を備えたプログラミング言語や計算モデルを考えてこなかった。こうした機構をもつ可逆な命令型プログラミング言語や計算モデルの研究は今後の課題である。
|
Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画において掲げていたもののうち、効率的な可逆シミュレーション方法、他の分野の言語との比較、実用的な応用、および可逆プログラミング言語の処理系の実現についてはいくつかの成果が得られている。実際、予定通りに効率的可逆シミュレーションの例として可逆並び替えアルゴリズムにおけるケーススタディを継続して、これらの導出法の共通点からエッセンスを抽出して概念を整備して、他のアルゴリズム設計でも利用できることが期待される考え方をまとめることができた。並び替えアルゴリズムは基礎的なアルゴリズムであり応用範囲が広いので、その可逆版も広く応用されることが期待される。可逆シミュレーションでは、可逆自己解釈の効率化が不完全である。直接実行から漸近的な計算量が増えないことが理想であるが、その実現可能性と構築法についてさらに研究を進める必要がある。他の分野の言語との比較においては、通底する考え方をまとめることで将来に可逆プログラミング言語の設計をするときに参考になることが期待される内容をまとめることができた。ただし、関数型可逆プログラミング言語については、これまでに発表した内容を踏まえて実装およびソースコードの公開を行っている。動的にメモリを確保する機構を備えたプログラミング言語としても可逆関数型言語は興味深いが、さらに理論の整備が必要であり、また有効な応用例を示すところまでには至れていない。動的にメモリを確保する機構を備えたプログラミング言語における自己解釈系が効率的に実現できるかについても示せていない。チューリング機械の設計では万能性を失わずに状態やシンボルの数を減らすことが多くの研究者によってなされている。可逆プログラミング言語においても可逆万能性を失わずにどれだけ言語を簡単化できるかについても今後の課題である。
|
Strategy for Future Research Activity |
物理的な可逆性を論理的可逆性に持ち上げられるようにするために、プログラミング言語・アルゴリズムのレベルで理論を整備していきたい。これまで得られた成果を発展させていきたいが、その方向には、厳密な形式化、効率化、応用範囲の拡大などが考えられる。これらの中から進むべき方向を考えるのではなく、見込みのあるサブテーマについてこれまでの成果を発展させていきたい。 まずは、動的にメモリを確保する機構を備えたプログラミング言語の研究を進めたい。関数型可逆言語の設計はいろいろと困難な点があるので、S式をもつ単純な可逆命令型言語を導入したい。その上で直接実行から漸近的な計算量が増えないような可逆自己解釈器の実現を目指す。こうした線形時間可逆自己解釈系をもちいることで、たとえば、Levinの万能検索(universal search)の可逆版の実現が近づくのではないかと考えている。また、可逆計算理論に対して可逆プログラミング言語理論を応用できる可能性がある。たとえば、読み込みのみ可能なメモリを仮定した可逆プログラミング言語によって決まる計算モデルで計算複雑度にどのような影響があるのかは興味深い。 可逆プログラミング言語の厳密な形式化という方向では、可逆性の形式的な証明を与えることが考えられる。上記のような単純な言語を用いることでmeta-reasoningがやりやすくなることが期待される。 得られた成果をオープンソースとして公開していく。これまでもJanusやPISAといった言語の解釈系の公開は行ってきたが、新しく開発するプログラミング言語についてもオンラインインタプリタやGitHubなどでのソースコードの公開を行っていきたい。このことによってわれわれの研究成果を他の研究者・技術者に容易に応用できるようにする。
|
Causes of Carryover |
研究発表のための費用や学術雑誌掲載料として準備していたものの、年度末までには使用できなかったので、次年度に繰り越して有効に使用する。
|
Expenditure Plan for Carryover Budget |
昨年度末までに行えなかった研究発表のための費用もしくは学術雑誌掲載料として充当する。
|
Research Products
(4 results)