arXiv subjects

Tatsuji Kawai

Publications and source records attributed to Tatsuji Kawai.

16 recordsLinked to original sources

arXiv2026

Constructive equivalence between Brouwer's fixed-point theorem and weak König's lemma

In the context of constructive reverse mathematics, we show that Brouwer's fixed-point theorem and weak König's lemma (WKL) are equivalent. To derive WKL from Brouwer's fixed-point theorem, the construction of a continuous function on the unit square without fixed points due to Orevkov [Soviet Math. Doklady (1963), 1253--1256] is generalised to yield a uniformly continuous function on the unit square whose fixed points encode information about infinite paths of a given infinite tree.

math.LO↗

arXiv2025

Modeling Language for Scenario Development of Autonomous Driving Systems

Autonomous driving systems are typically verified based on scenarios. To represent the positions and movements of cars in these scenarios, diagrams that utilize icons are typically employed. However, the interpretation of such diagrams is typically ambiguous, which can lead to misunderstandings among users, making them unsuitable for the development of high-reliability systems. To address this issue, this study introduces a notation called the car position diagram (CPD). The CPD allows for the concise representation of numerous scenarios and is particularly suitable for scenario analysis and design. In addition, we propose a method for converting CPD-based models into propositional logic formulas and enumerating all scenarios using a SAT solver. A tool for scenario enumeration is implemented, and experiments are conducted on both typical car behaviors and international standards. The results demonstrate that the CPD enables the concise description of numerous scenarios, thereby confirming the effectiveness of our scenario analysis method.

cs.SE↗

arXiv2022

Reflexive combinatory algebras

We introduce the notion of reflexivity for combinatory algebras. Reflexivity can be thought of as an equational counterpart of the Meyer-Scott axiom of combinatory models, which indeed allows us to characterise an equationally definable counterpart of combinatory models. This new structure, called strongly reflexive combinatory algebra, admits a finite axiomatisation with seven closed equations, and the structure is shown to be exactly the retract of combinatory models. Lambda algebras can be characterised as strongly reflexive combinatory algebras which are stable. Moreover, there is a canonical construction of a lambda algebra from a strongly reflexive combinatory algebra. The resulting axiomatisation of lambda algebras by the seven axioms for strong reflexivity together with those for stability is shown to correspond to the axiomatisation of lambda algebras due to Selinger [J.Funct.Programming, 12(6), 549--566, 2002].

cs.LO↗

arXiv2021

Predicative theories of continuous lattices

We introduce a notion of strong proximity join-semilattice, a predicative notion of continuous lattice which arises as the Karoubi envelop of the category of algebraic lattices. Strong proximity join-semilattices can be characterised by the coalgebras of the lower powerlocale on the wider category of proximity posets (also known as abstract bases or R-structures). Moreover, locally compact locales can be characterised in terms of strong proximity join-semilattices by the coalgebras of the double powerlocale on the category of proximity posets. We also provide more logical characterisation of a strong proximity join-semilattice, called a strong continuous finitary cover, which uses an entailment relation to present the underlying join-semilattice. We show that this structure naturally corresponds to the notion of continuous lattice in the predicative point-free topology. Our result makes the predicative and finitary aspect of the notion of continuous lattice in point-free topology more explicit.

cs.LO↗

arXiv2020

Decidable fan theorem and uniform continuity theorem with continuous moduli

The uniform continuity theorem (UCT) states that every pointwise continuous real-valued function on the unit interval is uniformly continuous. In constructive mathematics, UCT is stronger than the decidable fan theorem (DFT); however, Loeb [Ann. Pure Appl. Logic, 132(1):51-66, 2005] has shown that the two principles become equivalent with a suitable coding of "continuous functions" as type-one objects. The question remains whether DFT can be characterised by a weaker version of UCT using a natural subclass of pointwise continuous functions without such a coding. We show that when "pointwise continuous" is replaced with "having a continuous modulus", UCT becomes equivalent to DFT. We also show that this weakening of UCT is equivalent to a similar principle for real-valued functions on the Cantor space $\{0,1\}^{\mathbb{N}}$. These results extend Berger's characterisation of DFT by the similar principle for functions from $\{0,1\}^{\mathbb{N}}$ to $\mathbb{N}$, and unifies these characterisations of DFT in terms of functions having continuous moduli. Furthermore, we directly show that the continuous real-valued functions on the unit interval having continuous moduli are exactly those functions which admit the coding of "continuous functions" due to Loeb. Our result allows us to interpret her work in the usual context of mathematics.

math.LO↗

arXiv2020

Presenting de Groot duality of stably compact spaces

We give a constructive account of the de Groot duality of stably compact spaces in the setting of strong proximity lattice, a point-free representation of a stably compact space. To this end, we introduce a notion of strong continuous entailment relation, which can be thought of as a presentation of a strong proximity lattice by generators and relations. The new notion allows us to identify de Groot duals of stably compact spaces by analysing the duals of their presentations. We carry out a number of constructions on strong proximity lattices using strong continuous entailment relations and study their de Groot duals. The examples include various powerlocales, patch topology, and the space of valuations. These examples illustrate the simplicity of our approach by which we can reason about the de Groot duality of stably compact spaces.

cs.LO↗

arXiv2019

On the commutativity of the powerspace constructions

We investigate powerspace constructions on topological spaces, with a particular focus on the category of quasi-Polish spaces. We show that the upper and lower powerspaces commute on all quasi-Polish spaces, and show more generally that this commutativity is equivalent to the topological property of consonance. We then investigate powerspace constructions on the open set lattices of quasi-Polish spaces, and provide a complete characterization of how the upper and lower powerspaces distribute over the open set lattice construction.

math.GN↗

arXiv2019

Equivalents of the finitary non-deterministic inductive definitions

We present statements equivalent to some fragments of the principle of non-deterministic inductive definitions (NID) by van den Berg (2013), working in a weak subsystem of constructive set theory CZF. We show that several statements in constructive topology which were initially proved using NID are equivalent to the elementary and finitary NIDs. We also show that the finitary NID is equivalent to its binary fragment and that the elementary NID is equivalent to a variant of NID based on the notion of biclosed subset. Our result suggests that proving these statements in constructive topology requires genuine extensions of CZF with the elementary or finitary NID.

math.LO↗

arXiv2019

Representing definable functions of $\mathrm{HA}^ω$ by neighbourhood functions

Brouwer (1927) claimed that every function from the Baire space to natural numbers is induced by a neighbourhood function whose domain admits bar induction. We show that Brouwer's claim is provable in Heyting arithmetic in all finite types ($\mathrm{HA}^ω$) for definable functions of the system. The proof does not rely on elaborate proof theoretic methods such as normalisation or ordinal analysis. Instead, we internalise in $\mathrm{HA}^ω$ the dialogue tree interpretation of Gödel's system T due to Escardó (2013). The interpretation determines a syntactic translation of terms, which yields a neighbourhood function from a closed term of $\mathrm{HA}^ω$ with the required property. As applications of this result, we prove some well-known properties of $\mathrm{HA}^ω$: uniform continuity of definable functions from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ on the Cantor space; closure under the rule of bar induction; and closure of bar recursion for the lowest type with a definable stopping function.

math.LO↗

arXiv2019

The principle of pointfree continuity

In the setting of constructive pointfree topology, we introduce a notion of continuous operation between pointfree topologies and the corresponding principle of pointfree continuity. An operation between points of pointfree topologies is continuous if it is induced by a relation between the bases of the topologies; this gives a rigorous condition for Brouwer's continuity principle to hold. The principle of pointfree continuity for pointfree topologies $\mathcal{S}$ and $\mathcal{T}$ says that any relation which induces a continuous operation between points is a morphism from $\mathcal{S}$ to $\mathcal{T}$. The principle holds under the assumption of bi-spatiality of $\mathcal{S}$. When $\mathcal{S}$ is the formal Baire space or the formal unit interval and $\mathcal{T}$ is the formal topology of natural numbers, the principle is equivalent to spatiality of the formal Baire space and formal unit interval, respectively. Some of the well-known connections between spatiality, bar induction, and compactness of the unit interval are recast in terms of our principle of continuity. We adopt the Minimalist Foundation as our constructive foundation, and positive topology as the notion of pointfree topology. This allows us to distinguish ideal objects from constructive ones, and in particular, to interpret choice sequences as points of the formal Baire space.

cs.LO↗

arXiv2018

Factorizing the Top-Loc adjunction through positive topologies

We characterize the category of Sambin's positive topologies as a fibration over the category of locales Loc. The fibration is obtained by applying the Grothendieck construction to a doctrine over Loc. We then construct an adjunction between the category of positive topologies and that of topological spaces Top, and show that the well-known adjunction between Top and Loc factors through the newly constructed adjunction.

math.GN↗

arXiv2018

A continuity principle equivalent to the monotone $Π^{0}_{1}$ fan theorem

The strong continuity principle reads "every pointwise continuous function from a complete separable metric space to a metric space is uniformly continuous near each compact image." We show that this principle is equivalent to the fan theorem for monotone $Π^{0}_{1}$ bars. We work in the context of constructive reverse mathematics.

math.LO↗

arXiv2018

Principles of bar induction and continuity on Baire space

Brouwer-operations, also known as inductively defined neighbourhood functions, provide a good notion of continuity on Baire space which naturally extends that of uniform continuity on Cantor space. In this paper, we introduce a continuity principle for Baire space which says that every pointwise continuous function from Baire space to the set of natural numbers is induced by a Brouwer-operation. Working in Bishop constructive mathematics, we show that the above principle is equivalent to a version of bar induction whose strength is between that of the monotone bar induction and the decidable bar induction. We also show that the monotone bar induction and the decidable bar induction can be characterised by similar principles of continuity. Moreover, we show that the $Π^{0}_{1}$ bar induction in general implies LLPO (the lesser limited principle of omniscience). This, together with a fact that the $Σ^{0}_{1}$ bar induction implies LPO (the limited principle of omniscience), shows that an intuitionistically acceptable form of bar induction requires the bar to be monotone.

math.LO↗

arXiv2017

Formally continuous functions on Baire space

A function from Baire space to the natural numbers is called formally continuous if it is induced by a morphism between the corresponding formal spaces. We compare formal continuity to two other notions of continuity on Baire space working in Bishop constructive mathematics: one is a function induced by a Brouwer-operation (i.e. inductively defined neighbourhood function); the other is a function uniformly continuous near every compact image. We show that formal continuity is equivalent to the former while it is strictly stronger than the latter.

math.LO↗

arXiv2017

Localic completion of uniform spaces

We extend the notion of localic completion of generalised metric spaces by Steven Vickers to the setting of generalised uniform spaces. A generalised uniform space (gus) is a set X equipped with a family of generalised metrics on X, where a generalised metric on X is a map from the product of X to the upper reals satisfying zero self-distance law and triangle inequality. For a symmetric generalised uniform space, the localic completion lifts its generalised uniform structure to a point-free generalised uniform structure. This point-free structure induces a complete generalised uniform structure on the set of formal points of the localic completion that gives the standard completion of the original gus with Cauchy filters. We extend the localic completion to a full and faithful functor from the category of locally compact uniform spaces into that of overt locally compact completely regular formal topologies. Moreover, we give an elementary characterisation of the cover of the localic completion of a locally compact uniform space that simplifies the existing characterisation for metric spaces. These results generalise the corresponding results for metric spaces by Erik Palmgren. Furthermore, we show that the localic completion of a symmetric gus is equivalent to the point-free completion of the uniform formal topology associated with the gus. We work in Aczel's constructive set theory CZF with the Regular Extension Axiom. Some of our results also require Countable Choice.

math.GN↗

arXiv2017

Geometric theories of patch and Lawson topologies

We give geometric characterisations of patch and Lawson topologies in the context of predicative point-free topology using the constructive notion of located subset. We present the patch topology of a stably locally compact formal topology by a geometric theory whose models are the points of the given topology that are located, and the Lawson topology of a continuous lattice by a geometric theory whose models are the located subsets of the given lattice. We also give a predicative presentation of the frame of perfect nuclei on a stably locally compact formal topology, and show that it is essentially the same as our geometric presentation of the patch topology. Moreover, the construction of Lawson topologies naturally induces a monad on the category of compact regular formal topologies, which is shown to be isomorphic to the Vietoris monad.

math.CT↗