Combinatorial and computational structures of approximations of spaces
Project/Area Number |
15K00015
|
Research Category |
Grant-in-Aid for Scientific Research (C)
|
Allocation Type | Multi-year Fund |
Section | 一般 |
Research Field |
Theory of informatics
|
Research Institution | Kyoto University |
Principal Investigator |
Tsuiki Hideki 京都大学, 人間・環境学研究科, 教授 (10211377)
|
Project Period (FY) |
2015-04-01 – 2023-03-31
|
Project Status |
Completed (Fiscal Year 2022)
|
Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2019: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2018: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2017: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2016: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2015: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
Keywords | プログラム抽出 / 非決定性 / 実数計算 / 並列計算 / 実現可能性解釈 / 余帰納法 / グレイコード / IFP / CFP / Amb / シェルピンスキー四面体 / Coq / Program Extraction / nondeterminism / totality / Fixed Point Logic / Adequacy / Gray code / Lattice Puzzle / コンパクト集合 / T^omega / 計算可能解析学 / 表現空間 / ボトム入り文字列 / コンパクト集合の表現 / タイリング / full-folding map / 不定元 / 余代数 |
Outline of Final Research Achievements |
We studied combinatorial structures of approximations of continuous spaces like real numbers and computations based on them. Specifically, we are interested in the infinite Gray-code, which is a non-redundant representation of real numbers on infinite sequences with bottoms (i.e., non-terminating elements). Together with co-researchers, we developed logical systems called IFP (Intuitionistic Fixed Point Logic) and CFP (Concurrent Fixed Point Logic). From proofs in these systems, one can extract correct nondeterministic and concurrent programs that manipulate such partial representations, using their realizability interpretations.
|
Academic Significance and Societal Importance of the Research Achievements |
実数のグレイコード表現は,不定元を利用することにより離散的な構造を介さずに一意的に実数を表現したものであり,その上の計算には,非全域性や並列計算による非決定性といった実数計算の特徴的な性質が表れている。IFP / CFPは,非全域性や並列計算による非決定性について,実現可能性解釈を介して論理的に考察することを可能にしたものであり,実現可能性解釈の適用範囲を広げるとともに,並列計算の理解を深めている。
|
Report
(9 results)
Research Products
(47 results)
-
-
-
-
-
-
-
-
-
-
-
-
-
[Journal Article] Concurrent Gaussian Elimination2023
Author(s)
Berger Ulrich、Seisenberger Monika、Spreen Dieter、Tsuiki Hideki
-
Journal Title
M. Benini, O. Beyersdorff, M. Rathjen, P. Schuster (eds), Mathematics for Computation
Volume: -
Pages: 223-250
DOI
ISBN
9789811245213, 9789811245220
Related Report
Peer Reviewed / Int'l Joint Research
-
-
-
-
-
-
[Journal Article] Logic for Gray-code computation2016
Author(s)
U. Berger, K. Miyamoto, H. Schwichtenberg and H. Tsuiki.
-
Journal Title
D. Probst and P. Schuster (eds), Concepts of Proof in Mathematics, Philosophy, and Computer Science
Volume: -
Related Report
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] Logic for Gray code computation2015
Author(s)
Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg and Hideki Tsuiki
Organizer
CCA:Twelfth International Conference on Computability and Complexity in Analysis
Place of Presentation
明治大学 (東京)
Year and Date
2015-06-12
Related Report
Int'l Joint Research