| 研究課題/領域番号 |
14J09142
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 研究分野 |
数学基礎・応用数学
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
片岡 俊基 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| 研究期間 (年度) |
2014-04-25 – 2017-03-31
|
| 研究課題ステータス |
中途終了 (2016年度)
|
| 配分額 *注記 |
2,800千円 (直接経費: 2,800千円)
2016年度: 900千円 (直接経費: 900千円)
2015年度: 900千円 (直接経費: 900千円)
2014年度: 1,000千円 (直接経費: 1,000千円)
|
|---|
| キーワード | 超準解析 / 圏論 / トポス / ファイブレーション / 形式検証 / ハイブリッドシステム / 特徴量抽出 / 特異値分解 / Dedekind-MacNeille完備化 / 様相不動点論理 / 余代数 / 圏論的論理 / 様相論理 / データマイニング / 完備化 / コンパイラ / 相互作用の幾何 |
|---|
| 研究実績の概要 |
コンピューター制御される物理システム（ハイブリッドシステム）について，その正しさを確かめることは近年の重要な課題である。とくに本研究では，純粋なコンピュータープログラムのための検証手法を適切に拡張してハイブリッドシステムの検証手法を作ることを最終的な目標に設定していた。
本研究計画では[末永&蓮尾'11]のように超準解析を用いるアプローチを拡張するために，直観主義超準解析をよりよく研究することが必要と考えた。直観主義超準解析の先行研究について，[Moerdijk'95]に始まる研究ではトポスが主役として用いられていた一方，[Butz'04]ではトポスの場合の結果は一部でしかない。当初の研究計画ではトポスを重視していたが，それに限らない直観主義超準解析の研究を進めている。
今年度は，圏論的な超準解析（これは直観主義論理の場合を含む）について，申請者が行った研究の一部分をまとめ，圏論に関する国際会議であるCT (International Category Theory Conference) にて発表した。申請者の発表はplenary sessionで行われた。ここで発表した結果は，[Butz'04]で与えられた論理と圏モデルをファイブレーションという圏論の道具を用いて再調査し新しい特徴付けを得たというものである。
申請者がDC1採用されていた2年8ヶ月の業績をまとめると，「圏による極限的振舞いの検証」について3つの結果を得たと言える。今年度に発表した超準解析の結果は「無限小」などの超実数を論理に加えることが圏に何を加えることで達成されるのかであったことの他に，前年度までの結果として，無限に続く遷移を扱うための不動点論理に対応する圏に関する結果と，形式概念解析に対応して圏の双完備化（極限と余極限を適切に付加する）を得た結果がある。
|
| 現在までの達成度 (段落) |
28年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
28年度が最終年度であるため、記入しない。
|
