Tutorial: Sewon Park (Kyoto), Verified computation over real numbers and other continuous objects

In this tutorial session, I give an introductory talk about verifying computations over continuous objects mainly focusing on real numbers. iRRAM is a C++ library for exact real number computation. When the users import the library, they can create real number typed variables that can store the infinite information that real numbers have, and perform exact computations over them. Inspired by the library, we formalized an imperative programming language that can model core fragments of iRRAM and other imperative languages for exact real number computation.

The aim is that by formalizing (a core fragment of) real number computation software, we adopt the existing program verification methodologies to real number computation for imperative languages. As a result, we obtain a simple imperative language and its formal domain theoretic set-valued semantics (for nondeterminism/multivaluedness in computable analysis). We also devise a convenient-to-use Hoare-style verification calculus that can be used to formally prove the correctness of real number computation programs. Later, we discuss how the procedure can get extended with further continuous objects.

Tutorial: Takayuki Kihara (Nagoya), Lawvere-Tierney topologies for computability theorists, an introduction

Let us reconsider what an oracle is. First, an oracle is a blackbox; and second, an oracle is an operation on the object of truth-values. The latter approach is formulated using a topos-theoretic notion called Lawvere-Tierney topology. The notion of Lawvere-Tierney topology can be considered as a generalization of Grothendieck topology.

On the first day of the tutorial, the following topics will be discussed: (1) Grothendieck topology; (2) an abstract characterization of oracle; and (3) oracle as an operation on truth-values.

On the second day of the tutorial, the following topics will be discussed: (1) Beyond generalized Weihrauch degrees; (3) Reduction game; and (3) The lattice structure of Lawvere-Tierney topologies.

Ryoma Sin'ya (Akita), A quantitative approach to the primitive words conjecture

TBA

Margarita Korovina (Ershov Institute), Ksmt calculus for non-linear systems

In this talk we report on ongoing research on solving non-linear systems over the reals occurring in a wide range of applications, including hybrid models. In our framework methods from Computable Analysis and Automated Reasoning are combined to meet efficiency and expressiveness. This approach is applicable to a large number of constraints involving computable non-linear functions, piecewise polynomial splines, transcendental functions and solutions of polynomial differential equations. We give an introduction to the ksmt calculus for checking satisability of nonlinear systems in a CDCL style way inspired by advances in SAT solving. Along proof search ksmt resolves two type of conflicts: linear and non-linear. Linear conflicts are delegated to a decision procedure for linear real arithmetic and non-linear conicts are resolved by local linearisations separating the solution set and the current conflict. For constructing these linearisations we use the duality of both, analytical and algebraical properties of the non-linear functions involved in the formula. This duality gives rise to specic classes of functions which can be linearised effectively. We discuss open problems in this area. Joint work with F. Brauesse, K. Korovin, and N. Th. Muller.

Oleg Kudinov (Sobolev Institute), Order computable fields

The computability notion based on numberings is well established with a number of prominent results. Nevertheless applied to ordered fields it fails to capture some natural properties. For example the field of primitive recursive real numbers is not computable and there exists a computable real closed field with non-computable maximal Archemidean sufbields. In this paper we introduce the notion of order computable (or, o-computable) fields which aims to overcome these limitations. We present a general criterion when an ordered field is o-computable. Using this criterion we show that the field of primitive recursive real numbers is o-computable and that Archemidean parts of o-computable real closed fields are o-computable. We also state several open problems relating computability and o-computability. Joint work with Margarita Korovina.

Victor Selivanov (Ershov Institute), Effective descriptive theory of qcb_0-spaces

This is a brief survey of recent achievements in (effective) descriptive theory of qcb_0-spaces, with emphasis on (effective) quasi-Polish spaces and some simple non-countably based qcb_0-spaces like the space of unary real polynomials. Along with some recent results (including the results of project participants), possible new research directions and open questions will be discussed.

Yudai Suzuki (Tohoku), Fixed point for monotone operators and Weihrauch reducibility

Any monotone operator on the Cantor Space 2^ω has a fixed point. In the context of reverse mathematics, Avigad proved that the existence of fixed points for arithmetically definable operators (Σ^1_0 FP) is equivalent to ATR_0 over RCA_0. In this talk, we introduce some variants of Σ^1_0 FP and discuss the relations between them, ATR and single choice from the viewpoint of Weihrauch reducibility. This is joint work with Keita Yokoyama.

Holger Thies (Kyoto), Extracting exact real computation programs from proofs in type theory

We describe some recent progress on formal verification of exact real computation. We propose a constructive axiomatization of real numbers in a dependent type theory which formalizes real numbers in a conceptually similar way as some mature implementations of exact real computation. We implemented our theory in the Coq proof assistant and use Coq’s code extraction tools to extract Haskell programs from proofs. We extended the extraction to map primitive operations on constructive real numbers directly to the corresponding operation in the AERN framework, a Haskell implementation of exact real computation. We present some of the main features of this implementation and discuss several examples. (This talk is based on j.w.w. Sewon Park and Michal Konečný)

Mizuhito Ogawa (JAIST), Forward analysis of well-structured pushdown systems

TBA

Alexander Okhotin (St. Petersburg), Concatenation and star for event-clock input-driven pushdown automata

A timed extension of input-driven pushdown automata (also known as visibly pushdown automata and as nested word automata) under the event-clock model was introduced by Nguyen and Ogawa ("Event-clock visibly pushdown automata", SOFSEM 2009), who showed that this model can be determinized using the method of region construction. A new, direct determinization procedure for these automata was obtained by Ogawa and Okhotin ("On the determinization of event-clock input-driven pushdown automata", CoRR abs/2103.04079, 2021): an n-state nondeterministic automaton with k different clock constraints is transformed to a deterministic automaton with 2^{n^2} states, 2^{n^2+k} stack symbols and the same clock constraints as in the original automaton, and this construction is asymptotically optimal with respect to both the number of states and the number of stack symbols. In this talk, another direct construction will be presented: for any two event-clock input-driven automata, an event-clock input-driven automaton for their concatenation is obtained; similarly, an automaton recognizing the Kleene star of any given automaton is constructed. The new constructions are first presented for the case of event-clock finite automata without a stack, and then lifted to the case with a stack. (joint work with Prof. Mizuhito Ogawa from JAIST)

Tatsuya Goto (Nagoya), Goldstern's principle about unions of null sets

Goldstern showed that the union of an increasing sequence of Lebesgue measure zero sets with respect to full domination order of ω^ω has also Lebesgue measure zero provided that the sets are uniformly Σ^1_1. Our aim is how much we can drop the Σ^1_1 assumption.

We show that CH implies the negation of Goldstern's principle for the pointclass of all subsets. Moreover we show that Goldstern's principle for the pointclass of all subsets is consistent with ZFC. Also we prove that Goldstern's principle for the pointclass of all subsets holds in ZF+AD+DC.

Leonardo Pacheco (Tohoku), Determinacy and reflection principles in second-order arithmetic

Working in second order arithmetic, we characterize determinacy of finite differences of open and Σ^0_2 sets as reflection principles. In order to do so we study sequences of coded β-models. More precisely, we prove that: over ACA_0, Π^1_2-\refl(ACA_0) is equivalent to ∀n.(Σ^0_1)_n-Det^*_0, and Π^1_3-\refl(Π^1_1-CA_0) is equivalent to ∀n.(Σ^0_1)_n-Det; over ATR_0, Π^1_3-\refl(Π^1_2-CA_0) is equivalent to ∀n.(Σ^0_2)_n-Det. This is joint work with Keita Yokoyama.

Riccardo Gozzi (Kyoto), Analog characterization of complexity classes

In this talk I will present an introduction on how to use particular systems of polynomial ODEs in order to continuously characterize stardard complexity classes. This approach finds its foundations in the analog model of computation called General Purpose Analog Computational model, originally presented by Shannon in order to describe the behaviour of the analog machine known as the differential analyzer. The model was then extended and proved to be equivalent to the framework of computable analysis on a computability level. Indeed, it can be showed that analog classes inspired by this model are able to simulate Turing machines and in this way standard complexity classes such as FP or FEXPTIME can be univocally represented by means of solutions of Polynomial Initial Value Problems satisfying precise conditions. The same treatment can be reserved to characterize each level of the Grzegorczyk hierarchy, and, with suitable modifications, also classes of sets such as P or EXPTIME or space complexity classes such as FPSPACE and PSPACE.

Svetlana Selivanova (KAIST), Computational complexity of classical solutions of partial differential equations

We survey recent achievements in estimating computational complexity of partial differential equations (PDEs), as well as computing solutions with guaranteed precision within the exact real computation approach. The emphasis is on classical solutions and linear PDE systems, since these are the cases where most of the progress has been achieved so far. Complexity, as it turns out, heavily depends on the smoothness of the initial data, which has similarities with the situation for ordinary differential equations (ODEs).

Ruslan Kornev (Novosibirsk), On punctual presentations of Polish metric spaces

A Polish metric space is called computably categorical if has a unique computability structure up to computable isometry. In the spirit of the modern “punctual” approach to primitive recursive structures, we discuss the notions of a punctually categorical metric space and primitive recursive reducibility of presentations of a space.

Keita Yokoyama (Tohoku), Similarity and difference between reverse mathematics and Weihrauch degrees for hyperarithmetical problems

TBA