arXiv subjects

Hideki Tsuiki

Publications and source records attributed to Hideki Tsuiki.

8 recordsLinked to original sources

arXiv2026

Extracting total Amb programs from proofs

We present a logical system CFP (Concurrent Fixed Point Logic) supporting the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators: Restriction (binary), a strengthening of implication, and a unary operator for total concurrency. The source of the extraction is formal CFP proofs, the target is a lambda calculus with constructors and recursion extended by a constructor Amb (for McCarthy's amb) which is interpreted operationally as globally angelic choice and is used to implement nondeterminism and concurrency. The correctness of extracted programs is proven via an intermediate domain-theoretic denotational semantics. We demonstrate the usefulness of our system by extracting a nondeterministic program that translates infinite Gray code into the signed digit representation. A noteworthy feature of CFP is the fact that the proof rules for restriction and concurrency involve variants of the classical law of excluded middle that would not be interpretable computationally without Amb. This is a revised and extended version of the conference paper presented at ESOP 2022 with the same title that contains full proofs of all major results.

cs.LO↗

arXiv2025

Projected images of the Sierpinski tetrahedron and other layered fractal imaginary cubes

The Sierpinski tetrahedron has a remarkable property: It is projected to squares in three orthogonal directions, and moreover, to sets with positive Lebesgue measures in numerous directions. This paper proposes a method for characterizing directions along which the Sierpinski tetrahedron and other similar fractal 3D objects are projected to sets with positive measures. We apply this methodology to layered fractal imaginary cubes and achieve a comprehensive characterization for them. Layered fractal imaginary cubes are defined as attractors of iterated function systems with layered structures, and they are projected to squares in three orthogonal directions. Within this class, the Sierpinski tetrahedron, T-fractal, and H-fractal stand out as exemplary cases.

math.DS↗

arXiv2023

Intuitionistic Fixed Point Logic

We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract computational content from proofs about abstract structures specified by arbitrary classically true disjunction free formulas. The interpretation is shown to be sound with respect to a domain-theoretic denotational semantics and a corresponding lazy operational semantics of a functional language for extracted programs. We also show how extracted programs can be translated into Haskell. As an application we extract a program converting the signed digit representation of real numbers to infinite Gray-code from a proof of inclusion of the corresponding coinductive predicates.

cs.LO↗

arXiv2023

Concurrent Gaussian elimination

Working in a semi-constructive logical system that supports the extraction of concurrent programs, we extract a program inverting non-singular real valued matrices from a constructive proof based on Gaussian elimination. Concurrency is used for efficient pivoting, that is, for finding an entry that is apart from zero in a non-null vector of real numbers.

cs.LO↗

arXiv2022

Extracting total Amb programs from proofs

We present a logical system CFP (Concurrent Fixed Point Logic) from whose proofs one can extract nondeterministic and concurrent programs that are provably total and correct with respect to the proven formula. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators, A || B (restriction, a strengthening of the implication B -> A) and $\ddownarrow(A)$ (total concurrency). The target of the extraction is a lambda calculus with constructors and recursion extended by a constructor Amb (for McCarthy's amb) which is interpreted operationally as globally angelic choice. The correctness of extracted programs is proven via an intermediate domain-theoretic denotational semantics. We demonstrate the usefulness of our system by extracting a concurrent program that translates infinite Gray code into the signed digit representation. A noteworthy feature of our system is that the proof rules for restriction and concurrency involve variants of the classical law of excluded middle that would not be interpretable computationally without Amb.

cs.LO↗

arXiv2018

Computable dyadic subbases and $\mathbf{T}^ω$-representations of compact sets

We explore representing the compact subsets of a given represented space by infinite sequences over Plotkin's $\mathbb{T}$. We show that computably compact computable metric spaces admit representations of their compact subsets in such a way that compact sets are essentially underspecified points. We can even ensure that a name of an $n$-element compact set contains $n$ occurrences of $\bot$. We undergo this study effectively and show that such a $\mathbb{T}^ω$-representation is effectively obtained from structures of computably compact computable metric spaces. As an application, we prove some statements about the Weihrauch degree of closed choice for finite subsets of computably compact computable metric spaces. Along the way, we introduce the notion of a computable dyadic subbase, and prove that every computably compact computable metric space admits a proper computable dyadic subbase.

cs.LO↗

arXiv2015

Domain Representations Induced by Dyadic Subbases

We study domain representations induced by dyadic subbases and show that a proper dyadic subbase S of a second-countable regular space X induces an embedding of X in the set of minimal limit elements of a subdomain D of $\{0,1,\perp\}ω$. In particular, if X is compact, then X is a retract of the set of limit elements of D.

math.GN↗

arXiv2013

Every Separable Metrizable Space has a Proper Dyadic Subbase

The notions of a proper dyadic subbase and an independent subbase was introduced by H. Tsuiki to investigate in {0, 1, bot}-sequence codings of topological spaces. We show that every separable metrizable space has a proper dyadic subbase whose restriction to the perfect set defined by the Cantor-Bendixson theorem forms an independent subbase of the restricted space.

math.GN↗