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

Notion of space based on distributive lattices and its computational content

Research Project

Project/Area Number 20K14352
Research Category

Grant-in-Aid for Early-Career Scientists

Allocation TypeMulti-year Fund
Review Section Basic Section 12030:Basic mathematics-related
Research InstitutionKochi University (2022-2023)
Japan Advanced Institute of Science and Technology (2020-2021)

Principal Investigator

河井 達治  高知大学, 教育研究部自然科学系理工学部門, 講師 (00824343)

Project Period (FY) 2020-04-01 – 2025-03-31
Project Status Granted (Fiscal Year 2023)
Budget Amount *help
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2022: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2021: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Keywords構成的数学 / 位相空間論 / point-freeトポロジー / コンパクト空間 / 不動点定理 / 一点コンパクト化 / プログラム抽出 / 実現可能解釈 / 測度論 / pointfreeトポロジー / 分配束 / point-free位相
Outline of Research at the Start

構成的数学の主眼は,構成的証明とプログラムの対応を通して,数学に内在するアルゴリズム的側面を解明することにある.しかし,構成的位相空間論の主要なアプローチであるpoint-free位相の構成的意味の解明は全く進んでいない.本研究では,申請者の直近の研究に基づく分配束による位相構造を拡張することにより,厳密な構成的立場から,広範囲の空間を表現できるようなpoint-free位相の概念を提案する.また,この位相概念を用いて,構成的解析学の主要な部分を位相的観点から再構築する.さらに,証明からのプログラムの抽出を通して,point-free位相空間論の存在証明に内在するアルゴリズムを明らかにする.

Outline of Annual Research Achievements

本研究は,1.分配束に基づく新たな位相空間の概念を提案し,2.この概念に基づく命題の証明からアルゴリズムを抽出することを通して,point-free位相空間論に内在する構成的意味を解明することを目的としている.前年度までに,コンパクト空間の分配束による表現を,局所コンパクト空間に拡張した.ところが,昨年度に得られた局所コンパクト空間の特徴付けに対する証明に専門家から誤りが指摘され,今年度は,その証明の修正に取り組んだ.その結果,前年度にまでに得られた結果を完全に保持する形で,新たな証明を構成することができた.この結果は,9月に行われた国際学会CCC2023で発表した(現在,証明を修正した論文を準備中である).なお,専門家の指摘では,コンパクト空間の結果を自然に拡張する前年度の結果は成立しないのではないかとのことであった.しかし,本年度に与えた新たな証明により,昨年度までの結果が保持されたことは,コンパクト空間において成立する事実のさらなる拡張の可能性を示唆するものであると考える.一方,本年度は,上記の証明の修正に想定外の時間がかかり,本来行う予定であった,1.局所コンパクト空間の一点コンパクト化の単純な定式化やその具体例の構成,2.一般ユークリッド空間のpoint-free位相の定式化と,それに基づく種々の不動点定理のpoint-free位相のレベルでの形式化,については研究の新たな進展が得られていない.これらの課題については,来年度に取り組む予定である.

Current Status of Research Progress
Current Status of Research Progress

4: Progress in research has been delayed.

Reason

本年度は,前年度までに得られていた主結果の証明に誤りが指摘され,その修正に時間を取られてしまった.その結果,今年度に行う予定であった研究の進展が遅れている.幸い,上記の証明の修正は上手くいき,これまでの結果は保持されることを確認した.また,証明の修正の過程で,これまで気付かなかった新たな知見が得られたことも有用であった.今後は,これらの新たな知見を活かし,今年度に行う予定であった一点コンパクト化の定式化と証明,不動点定理のpoint-freeトポロジーにおける形式化とアルゴリズムの抽出に取り組む予定である.

Strategy for Future Research Activity

まず,局所コンパクト空間の一点コンパクト化のpoint-freeトポロジーにおける単純な証明を与え,その有用性を裏付けるための具体例を作成する.そして,一点コンパクト化に関する一連の研究成果を論文としてまとめる.また,順序関係から自然に誘導されると考えられるユークリッド空間の単体表現を用いることにより,一般のユークリッド空間のpoint-free位相表現を定式化する.そして,種々の不動点定理をpoint-free位相のレベルで形式化し,その証明を与える.一方,プログラム抽出のケーススタディとして,上記の一般ユークリッド空間の位相表現を構成的数学に基づく形式体系で実装し,不動点定理の証明の実装からのプログラム抽出を試みる.

Report

(4 results)
  • 2023 Research-status Report
  • 2022 Research-status Report
  • 2021 Research-status Report
  • 2020 Research-status Report
  • Research Products

    (11 results)

All 2023 2022 2021

All Journal Article (5 results) (of which Int'l Joint Research: 2 results,  Peer Reviewed: 5 results,  Open Access: 2 results) Presentation (5 results) (of which Int'l Joint Research: 4 results,  Invited: 3 results) Book (1 results)

  • [Journal Article] Reflexive combinatory algebras2022

    • Author(s)
      Gijzen Marlou M、Ishihara Hajime、Kawai Tatsuji
    • Journal Title

      Journal of Logic and Computation

      Volume: - Issue: 5 Pages: 937-960

    • DOI

      10.1093/logcom/exac049

    • Related Report
      2022 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Predicative theories of continuous lattices2021

    • Author(s)
      Tatsuji Kawai
    • Journal Title

      Logical Methods in Computer Science

      Volume: 17 Pages: 1-38

    • Related Report
      2021 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] Factorizing the Top-Loc adjunction through positive topologies2021

    • Author(s)
      Francesco Ciraulo, Tatsuji Kawai, and Samuele Maschio
    • Journal Title

      Archive for Mathematical Logic

      Volume: 60 Issue: 7-8 Pages: 967-979

    • DOI

      10.1007/s00153-021-00768-5

    • Related Report
      2021 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] From intuitionistic mathematics to point-free topology2021

    • Author(s)
      Tatsuji Kawai
    • Journal Title

      Proof and Computation II: From Proof Theory and Univalent Mathematics to Program Extraction and Verification

      Volume: - Pages: 55-98

    • DOI

      10.1142/9789811236488_0003

    • ISBN
      9789811236471, 9789811236488
    • Related Report
      2021 Research-status Report
    • Peer Reviewed
  • [Journal Article] Decidable fan theorem and uniform continuity theorem with continuous moduli2021

    • Author(s)
      Makoto Fujiwara and Tatsuji Kawai
    • Journal Title

      Mathematical Logic Quarterly

      Volume: -

    • Related Report
      2020 Research-status Report
    • Peer Reviewed
  • [Presentation] WLK implies CTM2023

    • Author(s)
      Tatsuji Kawai
    • Organizer
      Constructive Mathematics: Foundations and Practice, CM:FP
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] Predicative presentations of stably locally compact locales2023

    • Author(s)
      Tatsuji Kawai
    • Organizer
      CCC 2023 Continuity, Computability, Constructivity From Logic to Algorithms
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Predcative theory of stably locally compact locales2023

    • Author(s)
      Tatsuji Kawai
    • Organizer
      AVM 2023, Arbeitstagung Verona-Munchen
    • Related Report
      2022 Research-status Report
    • Int'l Joint Research
  • [Presentation] Real numbers from a point-free perspective2022

    • Author(s)
      河井達治
    • Organizer
      日本数学会2022年度秋季総合分科会
    • Related Report
      2022 Research-status Report
    • Invited
  • [Presentation] Spread representation of point-free real numbers2022

    • Author(s)
      Tatsuji Kawai
    • Organizer
      CCC2022: Continuity, Computability, Constructivity. From Logic to Algorithms
    • Related Report
      2022 Research-status Report
    • Int'l Joint Research / Invited
  • [Book] Handbook of Constructive Mathematics (15章 Bishop Metric Spaces in Formal Topolog, 分筆)2023

    • Author(s)
      Tatsuji Kawai (Editor, Bridges D, Ishihara H, Rathjen M, Schwichtenberg H)
    • Total Pages
      842
    • Publisher
      Cambridge University Press
    • ISBN
      9781009039888
    • Related Report
      2023 Research-status Report

URL: 

Published: 2020-04-28   Modified: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi