• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Combinatorial and computational structures of approximations of spaces

Research Project

Project/Area Number 15K00015
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Theory of informatics
Research InstitutionKyoto 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)
  • 2022 Annual Research Report   Final Research Report ( PDF )
  • 2021 Research-status Report
  • 2020 Research-status Report
  • 2019 Research-status Report
  • 2018 Research-status Report
  • 2017 Research-status Report
  • 2016 Research-status Report
  • 2015 Research-status Report
  • Research Products

    (47 results)

All 2023 2022 2021 2020 2019 2018 2017 2016 2015 Other

All Int'l Joint Research (12 results) Journal Article (7 results) (of which Int'l Joint Research: 5 results,  Peer Reviewed: 7 results,  Open Access: 1 results,  Acknowledgement Compliant: 1 results) Presentation (28 results) (of which Int'l Joint Research: 19 results,  Invited: 3 results)

  • [Int'l Joint Research] Swansea University(英国)

    • Related Report
      2022 Annual Research Report
  • [Int'l Joint Research] Swansea 大学(英国)

    • Related Report
      2021 Research-status Report
  • [Int'l Joint Research] Swansea University(英国)

    • Related Report
      2020 Research-status Report
  • [Int'l Joint Research] Swansea 大学(英国)

    • Related Report
      2019 Research-status Report
  • [Int'l Joint Research] Swansea 大学(英国)

    • Related Report
      2018 Research-status Report
  • [Int'l Joint Research] Swansea 大学(英国)

    • Related Report
      2018 Research-status Report
  • [Int'l Joint Research] Swansea University(英国)

    • Related Report
      2017 Research-status Report
  • [Int'l Joint Research] Swansea University(英国)

    • Related Report
      2017 Research-status Report
  • [Int'l Joint Research] Swansea University(英国)

    • Related Report
      2016 Research-status Report
  • [Int'l Joint Research] Universite Libre de Bruxelles(ベルギー)

    • Related Report
      2016 Research-status Report
  • [Int'l Joint Research] ミュンヘン大学/ジーゲン大学(ドイツ)

    • Related Report
      2015 Research-status Report
  • [Int'l Joint Research] スウォンジー大学/ケンブリッジ大学(英国)

    • Related Report
      2015 Research-status Report
  • [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

      10.1142/9789811245220_0009

    • ISBN
      9789811245213, 9789811245220
    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Extracting total Amb programs from proofs2022

    • Author(s)
      Berger Ulrich、Tsuiki Hideki
    • Journal Title

      Programming Languages and Systems (Proc. ESOP 2022, LNCS 13240)

      Volume: - Pages: 85-113

    • DOI

      10.1007/978-3-030-99336-8_4

    • ISBN
      9783030993351, 9783030993368
    • Related Report
      2021 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Intuitionistic fixed point logic2021

    • Author(s)
      Berger Ulrich、Tsuiki Hideki
    • Journal Title

      Annals of Pure and Applied Logic

      Volume: 172 Issue: 3 Pages: 1-56

    • DOI

      10.1016/j.apal.2020.102903

    • Related Report
      2020 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Prawf: An interactive proof system for program extraction2020

    • Author(s)
      Ulrich Berger, Olga Petrovska and Hideki Tsuiki
    • Journal Title

      proceedings of CIE 2020, Lecture Notes in Computer Science

      Volume: -

    • Related Report
      2019 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] On the Complexity of Lattice Puzzles.2019

    • Author(s)
      Yasuaki Kobayashi, Koki Suetsugu, Hideki Tsuiki, Ryuhei Uehara
    • Journal Title

      Proceedings of 30th International Symposium on Algorithms and Computation, {ISAAC}

      Volume: -

    • Related Report
      2019 Research-status Report
    • Peer Reviewed
  • [Journal Article] Obtaining the H and T Honeycomb from a Cross-Section of the 16-cell Honeycomb2017

    • Author(s)
      Hideki Tsuiki
    • Journal Title

      Proceedings, bridges 2017

      Volume: - Pages: 147-152

    • Related Report
      2017 Research-status Report
    • Peer Reviewed
  • [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
      2015 Research-status Report
    • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
  • [Presentation] Induction and coindution for computing exact overlaps of fractals2022

    • Author(s)
      Hideki Tsuiki
    • Organizer
      CCC2022 Workshop (Continuity, Computability, Constructivity -- From Logic to Algorithms)
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Some steps toward program extraction in a type-theoretical interpretation of IFP2022

    • Author(s)
      Ulrich Berger, Sewon Park, Holger Thies and Hideki Tsuiki
    • Organizer
      CCC2022 Workshop (Continuity, Computability, Constructivity -- From Logic to Algorithms)
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Induction / coinduction and projections of fractals2022

    • Author(s)
      Hideki Tsuiki
    • Organizer
      Proof and Computation 2022
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Extracting total Amb programs from proofs2022

    • Author(s)
      Ulrich Berger, Hideki Tsuiki
    • Organizer
      31st European Symposium on Programming
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] Extracting total Amb programs from proofs2022

    • Author(s)
      Ulrich Berger, Hideki Tsuiki
    • Organizer
      第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
    • Related Report
      2021 Research-status Report
  • [Presentation] IFP style proofs in the Coq proof assistant2021

    • Author(s)
      Sewon Park, Holger Thies and Hideki Tsuiki
    • Organizer
      CCC 2021 Continuity, Computability, Constructivity From Logic to Algorithms
    • Related Report
      2021 Research-status Report
  • [Presentation] シェルピンスキー四面体および関連したフラクタル の 2 次元射影について2021

    • Author(s)
      立木 秀樹
    • Organizer
      RIMS Symposium Recent Developments in Dynamical Systems and their Application
    • Related Report
      2021 Research-status Report
  • [Presentation] Intuitionistic Fixed Point Logic2021

    • Author(s)
      立木 秀樹, ウーリッヒ ベルガー
    • Organizer
      PPL 2021: 第23回プログラミングおよびプログラミング言語ワークショップ
    • Related Report
      2020 Research-status Report
  • [Presentation] Prawf: An Interactive Proof System for Program Extraction2020

    • Author(s)
      Ulrich Berger, Olga Petrovska, Hideki Tsuiki
    • Organizer
      Conference on Computability in Europe (CiE 2020)
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] Combining partial maps into a correct total map through program extraction2020

    • Author(s)
      Hideki Tsuiki
    • Organizer
      CCC 2020: Continuity, Computability, Constructivity --- From Logic to Algorithms
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] Partial program extractions in IFP2019

    • Author(s)
      Hideki Tsuiki
    • Organizer
      Mathematical Logic and Constructivity: The Scope and Limits of Neutral Constructivism
    • Related Report
      2019 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] On the Complexity of Lattice Puzzles2019

    • Author(s)
      Yasuaki Kobayashi, Koki Suetsugu, Hideki Tsuiki, Ryuhei Uehara
    • Organizer
      ISAAC 2019
    • Related Report
      2019 Research-status Report
    • Int'l Joint Research
  • [Presentation] 非構成的対象を扱った証明からのプログラム抽出2019

    • Author(s)
      立木秀樹
    • Organizer
      代数・論理・幾何と情報科学――理論から実世界への展開
    • Related Report
      2019 Research-status Report
  • [Presentation] IFPと、その並列プログラム抽出への拡張2019

    • Author(s)
      立木 秀樹
    • Organizer
      The 15th Theorem Proving and Provers meeting (TPP 2019)
    • Related Report
      2019 Research-status Report
  • [Presentation] Infinite Adequacy Theorem through Coinductive Definitions2019

    • Author(s)
      Hideki Tsuiki
    • Organizer
      Third Workshop on Mathematical Logic and its Applications
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research
  • [Presentation] T^ω-representations of compact sets through dyadic subbases2018

    • Author(s)
      Hideki Tsuiki and Arno Pauly
    • Organizer
      Workshop Domains '2018
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research
  • [Presentation] Gray code and extractions of concurrent executions of partial programs2018

    • Author(s)
      Hideki Tsuiki
    • Organizer
      Workshop: Constructive Mathematics
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research
  • [Presentation] Adequacy for infinite data2018

    • Author(s)
      Hideki Tsuiki and Ulrich Berger
    • Organizer
      CCC 2018
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research
  • [Presentation] イマジナリーキューブ・タイリングと16-cell タイリングの切断面2017

    • Author(s)
      立木 秀樹
    • Organizer
      Workshop「数論とエルゴード理論」
    • Place of Presentation
      金沢大学サテライト・プラザ(石川県・金沢市)
    • Year and Date
      2017-02-11
    • Related Report
      2016 Research-status Report
  • [Presentation] Concurrent program extraction2017

    • Author(s)
      Ulrich Berger and Hideki Tsuiki
    • Organizer
      Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2017)
    • Related Report
      2017 Research-status Report
    • Int'l Joint Research
  • [Presentation] Computable dyadic subbases2017

    • Author(s)
      Arno Pauly and Hideki Tsuiki
    • Organizer
      Second Workshop on Mathematical Logic and its Applications
    • Related Report
      2017 Research-status Report
    • Int'l Joint Research
  • [Presentation] Obtaining the H and T Honeycomb from a Cross-Section of the 16-cell Honeycomb2017

    • Author(s)
      Hideki Tsuiki
    • Organizer
      Bridges 2017
    • Related Report
      2017 Research-status Report
    • Int'l Joint Research
  • [Presentation] Gray/pre-Gray code and program extraction based on pre-Gray code2016

    • Author(s)
      Hideki Tsuiki
    • Organizer
      BIRS Workshop 「Interval Analysis and Constructive Mathematics」
    • Place of Presentation
      Oaxaca, メキシコ
    • Year and Date
      2016-11-13
    • Related Report
      2016 Research-status Report
  • [Presentation] T^omega-representations of compact sets2016

    • Author(s)
      Arno Pauly, Hideki Tsuiki
    • Organizer
      Thirteenth International Conference on Computability and Complexity in Analysis
    • Place of Presentation
      Faro, ポルトガル
    • Year and Date
      2016-06-15
    • Related Report
      2016 Research-status Report
    • Int'l Joint Research
  • [Presentation] full-folding map が生成するコードの再帰性について2016

    • Author(s)
      立木 秀樹
    • Organizer
      数論とエルゴート理論
    • Place of Presentation
      金沢大学サテライト・プラザ(石川県)
    • Year and Date
      2016-02-06
    • Related Report
      2015 Research-status Report
  • [Presentation] Domains with recursive structures representing a space2015

    • Author(s)
      Hideki Tsuiki
    • Organizer
      1st Pan Pacific International Conference on Topology and Applications (PPICTA)
    • Place of Presentation
      Hangzhou(中国)
    • Year and Date
      2015-11-25
    • Related Report
      2015 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] Computing with Compact Sets - the Gray Code Case2015

    • Author(s)
      Dieter Spreen, Hideki Tsuiki
    • Organizer
      Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2015)
    • Place of Presentation
      Kochel (ドイツ連邦共和国)
    • Year and Date
      2015-09-14
    • Related Report
      2015 Research-status Report
    • Int'l Joint Research
  • [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
      2015 Research-status Report
    • Int'l Joint Research

URL: 

Published: 2015-04-16   Modified: 2024-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi