On Threshold Problems for Orbits of Semigroup Actions by Eike

Today Eike Neumann will give a talk on Threshold Problems for Orbits of Semigroup Actions as a part of our theory seminar series.

Abstract:

Consider the following computational problem: Given a real function g on a space X, a compactly generated semi-group S acting on X, and a point x in X, is g positive on every point of the orbit of x under S?

This generalises a large number of widely studied problems, such as safety and liveness verification for discrete-time dynamical systems (corresponding to semi-groups with a single generator), threshold problems for stochastic (corresponding stochastic matrices acting on probability distributions) or quantum automata (corresponding to unitary operators acting on Hilbert spaces) and more.

When the objects above are presented via rational or algebraic data, the associated problems quickly become undecidable or very sensitive to the problem formulation. For example, threshold problems for stochastic automata are undecidable in general, and threshold problems for quantum automata are decidable if and only if they are formulated using strict inequality.

I will consider the above problem in its general form from the computable analysis perspective, replacing decidability with maximal partial decidability. I will give a sound algorithm that partially decides the problem over effectively locally compact spaces. I will show that the algorithm is complete when the space is zero-dimensional or locally contractible, and give some examples of spaces where the algorithm is not complete but the problem is maximally partially decidable and spaces where the problem is not maximally partially decidable at all.

Giorgio Genovesi on Characterizing Regular Countable Second Countable Spaces in Second Order Arithmetic

Today's seminar talk is by Giorgio Genovesi from Leeds, who will be talking about countable second countable topological spaces in the context of reverse mathematics. 

Title: Characterizing Regular Countable Second Countable Spaces in Second Order Arithmetic

Abstract: Regular countable second countable (CSC) spaces admit rather nice characterizations and can easily be formalized in second order arithmetic. It is natural to ask what set existence axioms are needed to ensure regular CSC spaces remain nice. It turns out many theorems which characterize regular CSC are equivalent to one of the big five subsystems of second order arithmetic.

Hideki Tsuiki visiting Swansea

Professor Hideki Tsuiki from Kyoto University is visiting Swansea University from 22nd to 24th of January. Yesterday, he gave a talk on Coinductive View of Shadows of 3D Fractals. 

The talk did not only give insight into a fascinating area of research, but was also entertaining. You may want to check out some of Prof. Tsuiki's videos, e.g. https://www.youtube.com/watch?v=VsFD37f-2ck  

Elvira Mayordomo visiting Swansea

Elvira Mayordomo is visiting us this week. Today she gave a talk as a part of our seminar series.

Title: On information theory in geometric measure theory

Abstract

Effective and resource-bounded dimensions were defined by Lutz in 2003 and have proven to be useful and meaningful for quantitative analysis in the contexts of algorithmic randomness, computational complexity and fractal geometry.

The point-to-set principle (PSP) of J. Lutz and N. Lutz (2018) fully characterizes Hausdorff and packing dimensions in terms of effective dimensions in the Euclidean space, enabling effective dimensions to be used to answer open questions about fractal geometry, with already an interesting list of geometric measure theory results.

In this talk I will review the point-to-set principles focusing on recent applications and extensions and presenting open questions as well as further application opportunities.

Oliver Kullmann's talk

Today Oliver Kullmann will give a talk on Automated search for special Latin squares as a part of our Seminar series.

Abstract: 

Latin squares have been studied since the days of Euler. After some overview on the history and background, an effort for a complete enumeration of special types of Latin squares of order 13, by as completely automated means as possible (which is currently actually not possible), will be presented and evaluated. The main method here is Cube-and-Conquer, a kind of 2-stage SAT-solving (as invented by the presenter). Quite some fine-tuning of representation and choice of solver was needed, and will be discussed (at some high level)

Matteo Acclavio visiting Swansea

Next week's theory seminar will be given by Matteo Acclavio from the University of Sussex, who is visiting us for a few days. The topic will be a new logical framework for concurrent programs, abstract below.

Title: A new logical framework for concurrent programs

Abstract:
Designing logical frameworks to reason about the properties of concurrent programs while accurately capturing the essence of concurrency is a challenging task.
The main difficulties can be traced back to the syntactic constraints of the languages used for this purpose.

In this talk, I will present my ongoing line of research, which aims to provide a new computation-as-deduction paradigm for the study of concurrent programs.
In particular, I will show you a non-commutative logic where we can interpret proofs as computation trees for the pi-calculus, and use proof nets to provide canonical representations of these trees modulo interleaving concurrency.

This work is based on joint works with Giulia Manara and Fabrizio Montesi

Next week's Theory Seminar Series

Next week Troy will give a talk on Conceptualising Programming Language Semantics as a part of our seminar series.

Abstract:

Research on the semantics of programming language has tended towards formalisation. Following the successful deployment and myriad uses of formal syntax, many of those working on semantics assumed similar successes would be realised with formal semantics. 

The reality was different, and the resultant language specifications were large, complicated, technical artefacts. My previous historical research has studied those from a technical perspective. 

In this talk, I will explore the conceptual surroundings of the semantics, examining the use of metaphors, analogies, and illustrative language used to accompany or explain the formal documents.

It is early stage research and will focus primarily on picking examples from the history of semantics for deeper analysis in the future.

I will also present some philosophical frameworks I am considering for use in this analysis and begin to discuss how they might help us understand the topic.

This research will ultimately lead to a conference presentation and journal article next year, as well as forming a pilot study for a research grant proposal.

An introduction to effective fractal dimension by Benjamin Koch

Today's theory seminar will be given by Benjamin Koch, who will give as an introduction to effective fractal dimension. 

Abstract:

The purpose of this talk is to give an overview of effective fractal dimension, which is an application of computability theory to geometric measure theory. I will start with an overview of two of the most important notions of dimension in classical measure theory, the Hausdorff and packing dimensions. Following this will be the formulation of so-called effective dimensions for points in R^n via Kolmogorov complexity. The highlight of the study of effective dimension thus far has been the “point-to-set principle”, which connects the effective dimension of points in R^n to the classical dimension of the subsets in which they reside. I will discuss a handful of the results that have come from this connection, which include an alternate proof of the Kakeya conjecture in R^2, an improved lower bound on the Hausdorff dimension of Furstenburg sets (which generalize Kakeya sets in R^2), and a generalization of an upper bound on the Hausdorff dimension of intersections and products of subsets of R^n

Theory Seminar Series

The theory seminar tomorrow will be given by Eike on "Robust Decidability of Escape Problems for General Non-Linear Systems."

Abstract:
A wide range of problems from a diverse range of areas can be formulated as "escape problems": does a given point escape a set under the iteration of a function, or do all points in a given set escape the set under the function.

The decidability of these problems is almost exclusively studied under the assumption that points, functions, and sets are specified exactly by a finite amount of data (e.g. rational or algebraic parameters). In this setting, positive results are largely limited to linear systems, since already very simple non-linear systems can have undecidable escape problems.

When working with systems that involve real data, say, coming from scientific or engineering applications, the assumption that the system be known to infinite precision is arguably unrealistic. One should rather assume that the system is known only up to finite precision. In that case, the natural question becomes whether the system's behaviour -- escaping or not escaping -- is robust under all sufficiently small perturbations. On the one hand, this requires us in some sense to do more than to decide the problem for a single given point at a time. On the other hand, there appears to be little value in determining the status of problem instances that lie on a "decision boundary", i.e. instances that are not robust under small perturbation. The latter point is interesting in light of the aforementioned undecidability results in the discrete-data setting, which appear to rely on the existence of very difficult non-robust instances.

The aim of this talk is to demonstrate by means of a case study that computable analysis constitutes an excellent framework for the discussion of robust decidability questions, such as the above. I will study to escape problems for very general non-linear systems and show at least in one case that the problem becomes as close to decidable as one can hope it to be in this setting. The Point Escape Problem is to decide for a given continuous map f, a given closed set A, and a given point x in A whether x escapes A under iteration of f. The Set Escape Problem is to decide for a given continuous map f and a given compact set K whether all points of K escape K under iteration of f. I will give a complete algorithm for the Point Escape Problem and a potentially not complete algorithm for the Set Escape Problem.  I will show that both algorithms terminate generically, and discuss some concrete examples of termination problems.

Research visit

Thomas Powell and Davide Barbarossa (Bath University) are visiting Swansea this week. This afternoon Thomas will give a talk on the "Rates of convergence for stochastic processes" as a part of our seminar series.  

Abstract: I will present two ongoing projects in the new area of proof mining  in stochastic optimization, each representing a distinct inroad into the area.  First, I will give an account of recent work with Morenikeji Neri that focuses on convergence proofs based on martingales: This quantitative study of  martingale convergence has resulted in several variants of the famous  Robbins-Siegmund theorem that come equipped with numerical information, with applications including stochastic quasi-Fejer monotone sequences and gradient-descent type algorithms. Second, I will report on some work in progress with Nicholas Pischkeon a new stochastic alternating Halpern-Mann scheme with noise terms: In addition to new convergence results (both qualitative and quantitative), this project has led to an interesting application in reinforcement learning, demonstrating that the techniques of proof mining are relevant for current research in the mathematics of artificial intelligence.

Máté Szabó's talk

Máté Szabó is visiting Swansea. He will give a talk today as a part of our theory seminar series:

Gödel's and Post's Proofs of the Incompleteness Theorem

This talk examines and compares two strikingly different proofs of the first incompleteness theorem. The first proof of the theorem was famously published by Kurt Gödel in 1931. However, during the previous decade, Emil Post already made significant breakthroughs in this topic, even though he was unable to publish his work for various reasons. After taking a short look at Gödel's diagonal proof, we will engage in more detail with Post's lesser-known proof. The latter proof is purely syntactic, and computer scientists of the day could recognize Post's approach as presenting one of the earliest term rewrite systems. By the end of the talk the audience will hopefully agree with Post stating that “with the Principia Mathematica as a common starting point [i.e. of Gödel and Post], the roads followed towards our common conclusions are so different that much may be gained from a comparison of these parallel evolutions”.

Pieter Collins visiting

Pieter Collins is currently visiting us from Maastricht. Today he will give a talk on "Verified Verification: Formal Proofs of Rigorous Numerical Methods for Model-Checking Dynamic Systems" as a part of our Theory Seminar series.