PhD Thesis:
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:
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
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.
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.
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.
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.
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".
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.
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.
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.
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.
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.
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.
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.
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.
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
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.