| 研究課題/領域番号 |
15K00015
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
立木 秀樹 京都大学, 人間・環境学研究科(研究院), 教授 (10211377)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2020-03-31
|
| キーワード | グレイコード / プログラム抽出 / full-folding map / 不定元 / 余代数 |
|---|
| 研究実績の概要 |
実数の表現である Gray-code を相互再帰的に定義された余代数として表現する方法を考案し、その実数の表現を用いて、形式体系で行われた代数的、および、余代数的な関数の定義から実数計算を行うプログラムを抽出する研究を行った。抽出されたプログラムは、符号付き２進表現とグレイコードの間の変換、平均をとる操作、グレイコードの有限の接頭辞から正規形への変換、Gray code からModified Gray Expansion への変換を行うものである。これらの演算の形式化をMinlog というプログラム抽出の機能を持つ証明支援系において行い、実際にプログラムの抽出を行った。
位相空間上の写像が再帰的なプログラムとして表現できるためには、そのコードが（相互）再帰的な構造を持つ必要がある。Full-folding map が生成するコードのもつ相互再帰的な構造は、記号力学系における Sofic shift と対応している。２次元の円盤と同相な位相空間上の Full-folding map が生成するコードが再帰的な構造を持つことと力学系の性質、特に、critical point の軌道の有限性との関係について調べた。
グレイコードに基づいた実数空間のコンパクト部分集合の表現、および、不定元（⊥）を含む無限列を用いた空間のコンパクト集合の表現を考案した。カントール集合の⊥入り文字列表現に対しては、⊥の個数と集合の濃度が一致するような表現が得られた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
プログラム抽出を専門とする研究者と共同研究を行い、グレイコード上の計算の定式化およびそれに基づくプログラムの抽出に関する成果を得て共著論文にまとめることができた。また、⊥入り文字列を用いたコンパクト集合の表現に関して、今後の研究の基礎となる共同研究を始めることが出来た。
|
| 今後の研究の推進方策 |
すでに始めている海外の研究者との共同研究を発展させていきたい。
|
| 次年度使用額が生じた理由 |
海外との共同研究が、日程調整がうまくできず、思ったようにできなかった。
|
| 次年度使用額の使用計画 |
研究発表のための海外出張を行う予定である。また、共同研究者を招聘する予定をたてている。
|
