Combinatorial and computational structures of approximations of spaces

2022 Fiscal Year Final Research Report

• 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
• Keywords: プログラム抽出 / 非決定性 / 実数計算 / 並列計算 / 実現可能性解釈

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.

Free Research Field

理論計算機科学

Academic Significance and Societal Importance of the Research Achievements

実数のグレイコード表現は，不定元を利用することにより離散的な構造を介さずに一意的に実数を表現したものであり，その上の計算には，非全域性や並列計算による非決定性といった実数計算の特徴的な性質が表れている。IFP / CFPは，非全域性や並列計算による非決定性について，実現可能性解釈を介して論理的に考察することを可能にしたものであり，実現可能性解釈の適用範囲を広げるとともに，並列計算の理解を深めている。