Tag Archives: visit

Logic Minisymposium at Swansea University

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


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


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.

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.

Jan Peleska and Wen-ling Huang visiting

Jan Peleska and Wen-ling Huang from the University of Bremen are visiting Swansea this week. Jan will give a talk on Safety-complete Test Suites as a part of Computational Foundry Seminar series.

More information: This presentation is about property-oriented testing. A novel safety-related variant of complete test suites for finite state machines is introduced. Under certain hypotheses which are similar to the ones used in the well-known complete testing methods like W-Method, Wp-Method, HSI-Method, or H-Method, the new method guarantees to uncover every safety violation, while erroneous outputs without safety-relevance may remain undetected. In well-defined situations that can be precisely pre-determined from the reference model, this leads to a substantial reduction of test cases in comparison to the size of the analogous W, WP, HSI, H-test suites. We advocate this new test strategy for situations, where exhaustive testing of the complete system is too expensive. In these cases, strong guarantees with respect to fault coverage should only be given for the errors representing safety violations, while it is considered as acceptable if less critical errors remain undetected. An original version of this material has been published at the ICTSS 2017 conference; in this talk, we present a refined test suite based on the H-method which can be shown to always produce less or equally many test cases as when applying the original H-method. We sketch how this strategy can be extended to safety-complete equivalence class testing for systems with infinite input domains but finitely many internal states and finite output domains.