Notion of space based on distributive lattices and its computational content

基于分布格的空间概念及其计算内容

• 批准号: 20K14352
• 负责人: 河井 達治
• 金额: $ 2.75万
• 依托单位: Kochi University (2022)Japan Advanced Institute of Science and Technology (2020-2021)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Early-Career Scientists
• 财政年份: 2020
• 资助国家: 日本
• 起止时间: 2020-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20K14352/
• 关键词: 構成的数学; 位相空間論; point-freeトポロジー; コンパクト空間; プログラム抽出; 不動点定理; 実現可能解釈; 測度論; pointfreeトポロジー; 分配束; point-free位相

本研究は，1. 分配束に基づく新たな位相空間の概念を提案し，2.この概念に基づく命題の証明からアルゴリズムを抽出することを通して，point-free 位相空間論に内在する構成的意味を解明することを目的としている．前年度までに，符号付きビット表現(三本木)のなす順序空間による実数位相の特徴付け，その高次元の拡張概念として重心細分に基づくユークリッド空間のpoint-free位相表現が得られている．本年度は，これまでに得られていたコンパクト空間の分配束による表現を，局所コンパクト空間に拡張した．具体的には，局所コンパクト空間が最大値を必ずしも持たない分配束と羃等関係の組として表現できることを示した．さらに，この分配束による表現を，entailment systemの概念に基づく論理システムとして特徴付けた．これらの表現は，コンパクト空間の分配束による表現や連続束(continuous lattice)のentailment systemによる表現の自然な一般化である．これら一連の研究成果は論文としてまとめられており，現在，学術雑誌に投稿中（査読中）である．また，上記で得られた局所コンパクト空間の表現と既存のコンパクト空間の束表現を用いて，局所コンパクト空間の一点コンパクト化を定義し，このコンパクト化の概念が既存の位相空間論における一点コンパクト化と同値であることを示した．このコンパクト化は，局所コンパクト空間のentailment systemによる論理システムに一つのモデルを強制的に挿入する，という自然な考えに基づくものであり，一点コンパクト化の構成に新たな視点を加えるものである．

This study is based on 1. The concept of phase space is proposed based on the theory of distributive bundle. 2. The concept of phase space is proposed based on the theory of point-free phase space. In the previous year, the symbol expression (Sampongi) of the sequence space, the characteristic expression of the numerical phase, the concept of expansion of the high dimension, and the point-free phase expression of the basic space were obtained. This year, the company has obtained the distribution of space and performance. The specific relationship between the maximum value of the space and the distribution of the bundle is shown in the table. In addition, the distribution of bundle performance, the concept of tailment system, the basic logic system and the characteristics of the system. The expression of this expression is a generalization of the expression of the distribution of spatial bundles and the expression of continuous lattice entailment systems. The research results of this paper are now published in academic journals. In the above note, the expression of the space and the bundle expression of the existing space are defined. The concept of the space and the bundle expression of the existing space are defined. The logic of the entry system of the spatial structure of the system is the logic of the entry system.

项目成果

Factorizing the Top-Loc adjunction through positive topologies

通过正拓扑分解 Top-Loc 附加

• DOI: 10.1007/s00153-021-00768-5
• 发表时间: 2021
• 期刊: Archive for Mathematical Logic
• 影响因子: 0.3
• 作者: Francesco Ciraulo;Tatsuji Kawai;and Samuele Maschio
• 通讯作者: and Samuele Maschio

Spread representation of point-free real numbers

无点实数的展开表示

• 发表时间: 2022
• 作者: Inui Takahisa;Wakasugi Yuta;梶原直人;Tatsuji Kawai
• 通讯作者: Tatsuji Kawai

From intuitionistic mathematics to point-free topology

从直觉数学到无点拓扑

• DOI: 10.1142/9789811236488_0003
• 发表时间: 2021
• 期刊: Proof and Computation II: From Proof Theory and Univalent Mathematics to Program Extraction and Verification
• 作者: Yoshikazu Giga;Fumihiko Onoue;Keisuke Takasao;梶原直人;Tatsuji Kawai
• 通讯作者: Tatsuji Kawai

Predcative theory of stably locally compact locales

稳定局部紧凑场所的预测理论

• 发表时间: 2023
• 作者: Umeda Akihiro;Wakasugi Yuta;Yoshikawa Shuji;Mitsuo Higaki;Keisuke Takasao;Kato Tomoya;梶原直人;Tatsuji Kawai
• 通讯作者: Tatsuji Kawai

Decidable fan theorem and uniform continuity theorem with continuous moduli

可判定扇形定理和具有连续模的一致连续性定理

• 发表时间: 2021
• 期刊: Mathematical Logic Quarterly
• 影响因子: 0.3
• 作者: Fujiwara Kazumasa;Vladimir Georgiev;Kato Tomoya;Makoto Fujiwara and Tatsuji Kawai
• 通讯作者: Makoto Fujiwara and Tatsuji Kawai