# Seminar series on Computability Theory and its Applications

Our colleague Arno Pauly is on the Programme Committee of the Computability Theory and its Applications seminar series, which currently is taking place virtually.

The seminar now has a YouTube channel where you can find the recordings of past talks you may have missed. The information on future talks, the timings of those, and the links to the videos are all available on the webpage here:

# Paul Shafer is coming to Swansea

We are looking forward to welcome Paul Schafer, who will be visiting Swansea University on 18 to 23 January.

# Hideki Tsuiki is back in Swansea

We are glad to welcome Hideki Tsuiki in Swansea again.  This Thursday we really enjoyed his talk on “Imaginary Cubes —  Mathematics, Puzzle, Art and Education”.

Abstract: Imaginary cubes are three-dimensional objects with square projections in three orthogonal ways just as a cube has.   How many different kinds of imaginary cubes can you imagine?  In this talk we  show that there are 16 kinds of minimal convex imaginary cubes which includes regular tetrahedron, cuboctahedron, and two objects that we call H and T.  As we will explain, H and T have a lot of beautiful mathematical properties related to tiling, fractal, and higher-dimensional geometry, and based on these properties, the speaker has designed a puzzle, constructed three-dimensional math-art objects, and used them for educations at various levels from elemental school to graduate schools. In this talk, I will explain mathematics of imaginary cubes and show the activities I have been engaged in.  I will carry a couple of copies of the puzzle and some of the math-art objects so that the audience can enjoy them while I am staying in Swansea.

# Philipp Schlicht visiting

Philipp Schlicht is visiting us today from Bristol. He’ll give us an introduction to automatic structures in the theory seminar today (2pm, CoFo 201).

Abstract: Automatic structures were first studied by Khoussainov and Nerode in 1995. I will first give an introduction with a focus on automatic ordinals and groups and then talk about tree-automatic structures. In particular, I will mention some recent partial results with Jain, Khoussainov and Stephan on the isomorphism problem for tree-automatic ordinals.

# Matthew Luckcuck visiting

Today Matthew Luckcuck (Liverpool) is visiting us today. He will give a talk on “Robotics and Integrated Formal Methods: Necessity meets Opportunity“.

Abstract: Robotic systems are multi-dimensional entities, combining both hardware and software, that are heavily dependent on, and influenced by, interactions with the real world. They can be variously categorised as embedded, cyberphysical, real-time, hybrid, adaptive and even autonomous systems, with a typical robotic system being likely to contain all of these aspects. The techniques for developing and verifying each of these system varieties are often quite distinct. This, together with the sheer complexity of robotic systems, leads us to argue that diverse formal techniques must be integrated in order to develop, verify, and provide certification evidence for, robotic systems. Furthermore, we propose the fast evolving field of robotics as an ideal catalyst for the advancement of integrated formal methods research, helping to drive the field in new and exciting directions and shedding light on the development of large-scale, dynamic, complex systems.

# Ryota Akiyoshi visiting

As a part of our Theory Seminars, today we welcomed Ryota Akiyoshi from Waseda University, who gave a talk on Takeuti’s finitism.

Abstract:  In this talk, we address several mathematical and philosophical issues of Gaisi Takeuti’s proof theory, who is one of the most distinguished logicians in proof theory after Hilbert and Gentzen. He furthered the realization of Hilbert’s program by formulating Gentzen’s sequent calculus for higher-oder logics, conjecturing that the cut-elimination holds for it (Takeuti’s conjecture), and obtaining several stunning results in the 1950-60’s towards the solution of his conjecture.
This talk consists of two parts. (1) To summarize Takeuti’s background and the argument of the well-ordering proof of ordinals up to ε0 , (2) To evaluate it on philosophical grounds. Also, we will explain several mathematical and philosophical issues to be solved. This is joint work with Andrew Arana.

# Logic Minisymposium at Swansea University

Tomorrow we are holding our end-of-summer logic minisymposium.

Speakers:

• Åsa Hirvonen
• Ken-etsu Fujita
• Masahiko Sato

Schedule:

2:00 Åsa Hirvonen (Helsinki University): On continuous logic
2:40 Coffee & Cake
3:00 Ken-etsu Fujita (Gunma University): A constructive proof of the Church—Rosser theorem
3:50 Masahiko Sato (Kyoto University): Unification of the Lambda-Calcululs and Combinatory Logic

On continuous logic, Åsa Hirvonen (Helsinki University)

Continuous first order logic in its current form was developed at the beginning of this millennium to offer a language for the model theoretic study of metric structures, such as Banach spaces and probability spaces. It is a many-valued logic but has a different motivation and semantic than, e.g., Lukasiewicz logic. Many model theoretical properties of first order logic generalise to it, such as compactness and Löwenheim-Skolem theorems. This talk is a general introduction to the syntax and semantics as well as some basic properties of continuous logic.

A constructive proof of the Church—Rosser theorem, Ken-etsu Fujita (Gunma University)

My motivation behind this talk comes from a quantitative analysis of reduction systems based on the two viewpoints, computational cost and computational orbit.

In the first part, we show that an upper bound function for the Church—Rosser theorem of type-free lambda-calculus with beta-reduction must be in the fourth level of the Grzegorczyk hierarchy. That is, the number of reduction steps to arrive at a common reduct is bounded by a function in the smallest Grzegorczyk class properly extending that of elementary functions. At this level we also find common reducts for the confluence property. The proof method developed here can be applied not only to type-free lambda-calculus with beta-eta-reduction
but also to typed lambda-calculi such as Pure Types Systems.

In the second part, we propose a formal system of reduction paths for parallel reduction, wherein reduction paths are generated from a quiver by means of three path-operators, concatenation, monotonicity, and cofinality. Next, we introduce an equational theory and reduction rules for the reduction paths, and show that the rules on paths are terminating and confluent so that normal paths are obtained. Following the notion of normal paths, a graphical representation of reduction paths is provided, based on which unique path and universal common-reduct properties are established. Finally, transformation rules from a conversion sequence to a reduction path leading to the universal common-reduct are given, and path matrices are also defined as block matrices of adjacency matrices in order to count reduction orbits.

Unification of the Lambda-Calcululs and Combinatory Logic, Masahiko Sato (Kyoto University):

The Lambda calculus and combinatory logic have been studied as two closely related but distinct systems of logic and computation. In this talk, however, we will argue that they are in fact one and the same calculus.

We substantiate our argument by introducing what we will call the external syntax and the internal syntax for the two calculi. The external syntax will be given as a natural common extension of syntax for the \lambda-calculus and combinatory logic.

The terms defined by the internal syntax will be characterized as the closed alpha eta normal terms of the external syntax. Thus, the external syntax provides us with human readable syntax containing all the traditional \lambda-terms and combinatory-terms, and the internal syntax is suitable for the infrastructure of a proof assistant.

This is an ongoing joint work with Takafumi Sakurai and Helmut Schwichtenberg.

# Founding the Foundry Lecture series welcome Prof. Moshe Vardi (Rice University)

Professor Moshe Vardi from Rice University, Texas, will give a talk on The Automated-Reasoning Revolution: From Theory to Practice and Back Wednesday 27th June, 12-1pm, Computational Foundry Seminar Room (Talbot 909).

Abstract:
For the past 40 years computer scientists generally believed that NP-complete problems are intractable. In particular, Boolean satisfiability (SAT), as a paradigmatic automated-reasoning problem, has been considered to be intractable. Over the past 20 years, however, there has been a quiet, but dramatic, revolution, and very large SAT instances are now being solved routinely as part of software and hardware design. In this talk I will review this amazing development and show how automated reasoning is now an industrial reality.

I will then describe how we can leverage SAT solving to accomplish other automated-reasoning tasks.  Counting the number of satisfying truth assignments of a given Boolean formula or sampling such assignments uniformly at random are fundamental computational problems in computer science with applications in software testing, software synthesis, machine learning, personalized learning, and more.  While the theory of these problems has been thoroughly investigated since the 1980s, approximation algorithms developed by theoreticians do not scale up to industrial-sized instances.  Algorithms used by the industry offer better scalability, but give up certain correctness guarantees to achieve scalability. We describe a novel approach, based on universal hashing and Satisfiability Modulo Theory, that scales to formulas with hundreds of thousands of variables without giving up correctness guarantees.

# Amir Tabatabai and Rahele Jalali visiting

Amir Tabatabai and Rahele Jalali, both PhD students at the Institute of Mathematics of the Czech Academy of Sciences under the supervision of Pavel Pudlak, are visiting Swansea University 13 Nov – 6 Dec 2017.

Amir will give a talk on Computational Flows in Arithmetic on 16 November.

More information: A computational flow is a pair consisting of a sequence of computational  problems of a certain sort and a sequence of computational reductions among
them. In this talk we will explain the basics of the theory of computational
flows and how they make a sound and complete interpretation for bounded
theories of arithmetic. This property helps us to decompose a first order
arithmetical proof to a sequence of computational reductions by which we can
extract the computational content of the low complexity statements in some
bounded theories of arithmetic such as  $I\Delta_0, T^k_n, I\Delta_0 + EXP \text{ and } PRA$.