PhD Thesis:

1. Terminating via Ramsey's Theorem (supervisor Stefano Berardi, co-supervisor Paulo Oliva), Università degli Studi di Torino
   Abstract Hide

   The goal of this thesis is to investigate in suitable logical settings termination results, which make use of Ramsey's Theorem for pairs, in order to extract bounds for termination. Amongst the several applications of Ramsey's Theorem for pairs in Computer Science, we focus on the Termination Theorem by Podelski and Rybalchenko and the Size-Change Termination Theorem by Lee, Jones and Ben-Amram. This work is divided in three main parts. We start by isolating a fragment of Ramsey's Theorem for pairs which is provable in Second Order Intuitionistic Arithmetic; from this result we provide intuitionistic proofs and corresponding bounds for termination results. A second part is devoted to study bounds for the Termination Theorem by using a fundamental tool of Proof Theory: Spector's bar recursion. Eventually, we investigate termination analysis from the viewpoint of Reverse Mathematics.

Papers:

1. The strength of SCT soundness (with Emanuele Frittaion, Florian Pelupessy and Keita Yokoyama), Journal of Logic and Computation, Volume 28, Issue 6, 5 September 2018, Pages 1217–1242
   Abstract Hide

   In this paper we continue the study, from Frittaion, Steila and Yokoyama (2017), on size-change termination in the context of Reverse Mathematics. We analyze the soundness of the SCT method. In particular, we prove that the statement "any program which satisfies the combinatorial condition provided by the SCT criterion is terminating" is equivalent to WO(omega_3) over RCA_0

2. About some fixed point axioms and related principles in Kripke-Platek environments (with Gerhard Jäger), Journal of Symbolic Logic, Volume 83, Issue 2, June 2018, pp. 642-668
   Abstract Hide

   Starting point of this article are fixed point axioms for set-bounded monotone Sigma_1 definable operators in the context of Kripke-Platek set theory KP. We analyze their relationship to other principles such as maximal iterations, bounded proper injections, and Sigma_1 subset-bounded sparation. One of our main results states that in KP + (V=L) all these principles are equivalent to Sigma_1 separation.

3. A combinatorial bound for a restricted form of the Termination Theorem, Accepted for: Well quasi-orders in computation, logic, language and reasoning. A unifying concept of proof theory, automata theory, formal languages and descriptive set theory. Ed. Peter Schuster, Monika Seisenberger, Andreas Weiermann, Trends in Logic, Springer.
   Abstract Hide

   We present a combinatorial bound for the H-bounded version of the Termination Theorem. As a consequence we improve the result by Solovay and Ketonen on the relationship between Paris Harrington's Theorem and the Fast Growing Hierarchy.

4. The strength of the SCT criterion (with Emanuele Frittaionand Keita Yokoyama), TAMC 2017: 260-273
   Abstract Hide

   We undertake the study of size-change analysis in the context of Reverse Mathematics. In particular, we prove that the SCT criterion is equivalent to Sigma-0-2-induction over RCA_0.

5. A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem (with Paulo Oliva), Journal of Symbolic Logic, Volume 83, Issue 1, March 2018 , pp. 70-83
   Abstract Hide

   In 1979 Schwichtenberg showed that a rule-like version Spector's bar recursion of lowest type levels 0 and 1 is closed under system T. More precisely, if the functional Y which controls the stopping condition of Spector's bar recursor is T-definable, then the corresponding bar recursion of type levels 0 and 1 is already T-definable. Schwichtenberg's original proof, however, relies on a detour through Tait's infinitary terms and the correspondence between ordinal recursion for alpha < epsilon_0 and primitive recursion over finite types. This detour makes it hard to calculate on given concrete system T input, what the corresponding system T output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into T-definitions under the conditions of Schwichtenberg's theorem. Finally, with the explicit construction we can also easily state a sharper result: if Y is in the fragment Ti then terms built from BR(N,sigma) for this particular Y are definable in the fragment Ti+max{1,level(sigma)}+1.

6. Some algebraic equivalent forms of all reals are constructible, submitted
   Abstract Hide

   We study Sigma-1-2 definable counterparts for some algebraic equivalent forms of the Continuum Hypothesis. These turn out to be equivalent to "all reals are constructible".

7. Ramsey's Theorem for Pairs and k Colors as a Sub-Classical Principle of Arithmetic (with Stefano Berardi), Journal of Symbolic Logic, Volume 82, Issue 2, June 2017, pp. 737-753
   Abstract Hide

   The purpose is to study the strength of Ramsey's Theorem for pairs restricted to recursive assignments of k-many colors, with respect to Intuitionistic Heyting Arithmetic. We prove that for every natural number k>1, Ramsey's Theorem for pairs and recursive assignments of k colors is equivalent to the Limited Lesser Principle of Omniscience for Sigma-0-3 formulas over Heyting Arithmetic. Alternatively, the same theorem over intuitionistic arithmetic is equivalent to: for every recursively enumerable infinite k-ary tree there is some i < k and some branch with infinitely many children of index i.

8. Generic Large Cardinals and Systems of Filters (with Giorgio Audrito), Journal of Symbolic Logic, Volume 82, Issue 3, September 2017, pp. 860-892
   Abstract Hide

   We introduce C-system of filters, a notion which generalizes the standard definitions of both extenders and towers of normal ideals and which provides a framework to develop the theory of extenders and towers in a more general and concise way. In this framework we investigate generic large cardinals properties.

9. Reverse Mathematical bounds for the Termination Theorem (with Keita Yokoyama), Annals of Pure and Applied Logic, 167(12):1213-1241, 2016
   Abstract Hide

   In 2004 Podelski and Rybalchenko expressed the termination of transition-based programs as a property of well-founded relations. The classical proof by Podelski and Rybalchenko requires Ramsey's Theorem for pairs which is a purely classical result, therefore extracting bounds from the original proof is non-trivial task. Our goal is to investigate the termination analysis from the point of view of Reverse Mathematics. By studying the strength of Podelski and Rybalchenko's Termination Theorem we can extract some information about termination bounds.

10. An intuitionistic version of Ramsey's Theorem and its use in Program Termination (with Stefano Berardi), Annals of Pure and Applied Logic, 166(12):1382-1406, 2015
    Abstract Hide

    Ramsey's Theorem for pairs is a fundamental result in combinatorics which cannot be intuitionistically proved. In this paper we present a new form of Ramsey's Theorem for pairs we call the H-closure Theorem, where H stands for "homogeneous". The H-closure Theorem is a property of well-founded relations, intuitionistically provable, informative, and simple to use in intuitionistic proofs. Using our intuitionistic version of Ramsey's Theorem we intuitionistically prove the Termination Theorem by Podelski and Rybalchenko. The Termination Theorem concerns an algorithm inferring termination for while-programs, and was originally proved from the classical Ramsey Theorem. Vytiniotis, Coquand, and Wahlstedt provided an intuitionistic proof of the Termination Theorem, using the Almost Full Theorem, an intuitionistic version of Ramsey's Theorem different from the H-closure Theorem. We provide a second intuitionistic proof of the Termination Theorem using the H-closure Theorem. In another paper, we use our proof to extract bounds for the Termination Theorem.

11. An Analysis of the Podelski-Rybalchenko Termination Theorem via Bar Recursion (with Stefano Berardi and Paulo Oliva), Journal of Logic and Computation, First published online: August 28, 2015
    Abstract Hide

    We present an effective proof (with explicit bounds) of the Podelski and Rybalchenko Termination Theorem. The sub-recursive bounds we obtain make use of bar recursion, in the form of the product of selection functions, as this is used to interpret the Weak Ramsey theorem for pairs. The construction can be seen as calculating a modulus of well-foundedness for a given program given moduli of well-foundedness for the disjunctively well-founded finite set of covering relations. When the input moduli are in system T, this modulus is also definable in system T by a result of Schwichtenberg on bar recursion.

12. An intuitionistic analysis of size-change termination, TYPES 2014:288-307
    Abstract Hide

    In 2001 Lee, Jones and Ben-Amram introduced the notion of size-change termination (SCT) for first order functional programs, a sufficient condition for termination. They proved that a program is size-change terminating if and only if it has a certain property which can be statically verified from the recursive definition of the program. Their proof of the size-change termination theorem used Ramsey's Theorem for pairs, which is a purely classical result. In 2012 Vytiniotis, Coquand and Wahlsteldt intuitionistically proved a classical variant of the size-change termination theorem by using the Almost-Full Theorem instead of Ramsey's Theorem for pairs. In this paper we provide an intuitionistic proof of another classical variant of the SCT theorem: our goal is to provide a statement and a proof very similar to the original ones. This can be done by using the H-closure Theorem, which differs from Ramsey's Theorem for pairs only by a contrapositive step. As a side result we obtain another proof of the characterization of the functions computed by a tail-recursive SCT program, by relating the SCT Theorem with the Termination Theorem by Podelski and Rybalchenko. Finally, by investigating the relationship between them, we provide a property in the language of size-change termination which is equivalent to Podelski and Rybalchenko's termination.

13. A Boolean Algebraic Approach to Semiproper Iterations (with and Matteo Viale and Giorgio Audrito), preprint
    Abstract Hide

    These notes present a compact and self-contained approach to iterated forcing with a particular emphasis on semiproper forcing. We tried to make our presentation accessible to any scholar who has some familiarity with forcing and boolean valued models and full details of all proofs are given.

    We focus our presentation using the boolean algebra language and defining an iteration system as a directed and commutative system of complete and injective homomorphisms between complete and atomless boolean algebras.

    It is well known that the boolean algebra approach to forcing and iterations is fully equivalent to the standard one. While there are several monographs where forcing is introduced by means of boolean valued models, to our knowledge no detailed account of iterated forcing following a boolean algebraic approach has yet appeared. We believe that this different approach is fruitful since the richness of the algebraic language simplifies many calculations and definitions, among which that of RCS-limits. Some of the advantages of this approach have been already outlined by Donder and Fuchs.

    The first part of these notes present the general framework needed to develop the notion of limit of an iterated system of forcings in the boolean algebraic language. The second part contains a proof of the main result of Shelah on semiproper iterations, i.e. that RCS-limit of semiproper iterations are semiproper.

14. Proving termination of programs having transition invariants of height omega (with Stefano Berardi and Paulo Oliva), ICTCS 2014: 237-240
    Abstract Hide

    We study the proof of a recent and relevant result about termination of programs, the Termination Theorem by Podelski and Rybalchenko. We prove that in a special case, the only case which is used in applications, all programs proved to be terminating may be described by some primitive recursive map.

15. Ramsey Theorem as an Intuitionistic Property of Well Founded Relations (with Stefano Berardi), RTA-TLCA 2014: 93-107
    Abstract Hide

    Ramsey Theorem for pairs is a combinatorial result that cannot be intuitionistically proved. In this paper we present a new form of Ramsey Theorem for pairs we call H-closure Theorem. H-closure is a property of well-founded relations, intuitionistically provable, informative, and simple to use in intuitionistic proofs. Using our intuitionistic version of Ramsey Theorem we intuitionistically prove the Termination Theorem by Poldenski and Rybalchenko. This theorem concerns an algorithm inferring termination for while-programs, and was originally proved from the classical Ramsey Theorem, then intuitionistically, but using an intuitionistic version of Ramsey Theorem different from our one. Our long-term goal is to extract effective bounds for the while-programs from the proof of Termination Theorem, and our new intuitionistic version of Ramsey Theorem is designed for this goal.

    This is a conference paper which prepares An intuitionistic version of Ramsey's Theorem and its use in Program Termination

16. Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic (with Stefano Berardi), TYPES 2013:64-83
    Abstract Hide

    We produce a first order proof of a famous combinatorial result, Ramsey Theorem for pairs and in two colors. Our goal is to find the minimal classical principle that implies the "miniature" version of Ramsey we may express in Heyting Arithmetic (HA). We are going to prove that Ramsey Theorem for pairs with recursive assignments of two colors is equivalent in (HA) to the sub-classical principle 3-LLPO. One possible application of our result could be to use classical realization to give constructive proofs of some combinatorial corollaries of Ramsey; another, a formalization of Ramsey in (HA), using a proof assistant.

    In order to compare Ramsey Theorem with first order classical principles, we express it as a schema in the first order language of arithmetic, instead of using quantification over sets and functions as it is more usual: all sets we deal with are explicitly defined as arithmetical predicates. In particular, we formally define the homogeneous set which is the witness of Ramsey theorem as a Delta-0-3-arithmetical predicate.