3rd Workshop on Proof Theory and Rewriting

We discuss what kind of quantitative information one can extract under which circumstances from proofs of convergence statements in analysis. We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functionals $B$, $L$, where $L$ is a learning procedure for a rate of convergence which succeeds after at most $B(a)$-many mind changes. This $(B,L)$-learnability provides quantitative information strictly in between a full rate of convergence (obtainable in general only from semi-constructive proofs) and a rate of metastability in the sense of Tao (extractable also from classical proofs). In fact, it corresponds to rates of metastability of a particular simple form. Moreover, if a certain gap condition is satisfied, then $B$ and $L$ yield a bound on the number of possible fluctuations. We explain recent applications of proof mining to ergodic theory in terms of these results. (joint work with Pavol Safarik)

Interesting properties of rewrite systems, like termination or non-termination, in some cases can be deduced from the existence of finite certificates, like (matrix) interpretations, or (looping) derivations, respectively. We are interested in certificates whose validity can be described in Presburger Logic, and is thus decidable. We obtain a unified description of several known (non-)termination proof methods, and derive some extensions.

In this talk, based on joint work with Andrei Popescu, we present an Isabelle/HOL formalization of the fact that every well-founded relation can be extended to a total well-order.

Constructive Analysis (aka BISH) was introduced by Errett Bishop as a `computational' redevelopment of Mathematics in the spirit of the intuitionistic tradition. As such, BISH is based on the BHK (Brouwer-Heyting-Kolmogorov) interpretation of logic, where the notions of `proof' and `algorithm' are central. Constructive Reverse Mathematics (CRM) is a spin-off from Harvey Friedman's `Reverse Mathematics' program where the base theory is based on BISH.

In this talk, we introduce an interpretation of BISH in classical Nonstandard Analysis. The role of `proof' in this interpretation is played by the Transfer Principle of Nonstandard Analysis. The role of `algorithm' is played by `$\Omega$-invariance'. Intuitively, an object is $\Omega$-invariant if it does not depend on the choice of infinitesimal used in its definition. Using this new interpretation, we obtain many of the well-known results form CRM. In particular, all non-constructive principles (like LPO, LLPO, MP, etc) are interpreted as Transfer Principles, which are not available in our (nonstandard) base theory. Finally, our interpretation preserves the property of BISH that not all $\Delta_1$-formulas are decidable.

This is joint work with Harvey Friedman. We examine two Ramsey like theorems which are independent of PA. The first one is the finite adjacent Ramsey theorem and the second one is the Paris-Harrington theorem. We provide a proof of independence for both theorems which is based on Friedman's result which states that the infinite adjacent Ramsey theorem implies the well ordering of $\epsilon_0$.

Kirby and Paris (1982) proved in a celebrated paper that a theorem of Goodstein (1944) cannot be established in Peano (1889) arithmetic. We present an encoding of Goodstein's theorem as a termination problem of a finite rewrite system. Using a novel implementation of ordinal interpretations, we are able to automatically prove termination of this system, resulting in the first automatic termination proof for a system whose derivational complexity is not multiply recursive. The talk is based on joint work with Sarah Winkler and Harald Zankl.

The unfolding of a schematic system $S$, as defined by Feferman, seeks to answer the question: Given $S$, which operations and predicates, and which principles concerning them, ought to be accepted if one has accepted $S$? I will relate the results of my investigations into the proof theory of the unfolding of ID1, the schematic system of one arithmetical inductive definition. The proof-theoretic ordinal arises as the collapse of the first strongly critical ordinal after the first uncountable ordinal. The techniques used are proof-theory of admissible set theory and asymmetric interpretation.

Kolmogorov in his ``Deutung der intuitionistischen Logik'' views mathematical propositions as problems, asking for a solution. The fact that nested implications may occur requires a concept of higher type computation. Concrete computable functionals are naturally defined by equations, which can be used as rewrite rules. They do not need to terminate: an example is the fixed point functional $Y$, defined by $Y f = f(Y f)$. However, such rewrite rules give rise to a denotational semantics of a higher type term language, in the context of the Scott - Ershov model of partial continuous functionals. A recent attempt to build a formal theory of computable functionals along these lines is presented. As an example, we discuss how Kreisel's density theorem can be formalized, and what use can be made of the formal proof obtained.

One of modern approaches to computability with realistic resources, e.g., polynomial-time computability, consists of (i) predicative/ impredicative type distinction (initiated by S. Bellantoni/ S. Cook, or D. Leivant) and (ii) linearity. The purpose of introducing linearity is to control multiple occurrence of the same objects. In terms of termination orderings, linearity is made possible by imposing constraints on rewriting, e.g., by employing innermost rewriting strategy. In this talk we will discuss about termination orderings over term graphs to make linearity possible without restrictive rewriting strategies.

Total NP search problems play an important role in analysing bounded arithmetic and related propositional proof systems. In the talk we will explain this connection for the case of second order bounded arithmetic theories, which have proof theoretic strengths corresponding to polynomial space and exponential time computation. In particular, we will explain improved witnessing theorems for second order bounded arithmetic, and a theory of nondeterministic polynomial space computation for the theory corresponding to polynomial space. Kołodziejczyk, Nguyen, and Thapen have introduced local improvement properties to characterize the provably total NP functions of the second order theories. Our characterisations will strengthen their results, and in particular show that the strengths of their local improvement principles over second order bounded arithmetic depend primarily on the topology of the underlying graph, not the number of rounds in the local improvement games.

This is joint work with Sam Buss.

We present a smooth approach to generate Goodstein principles which are true but unprovable in theories of iterated inductive definitions, $\mathit{ID}_n$, and eventually the theory $\Pi_1^1$-$\mathit{CA}_0$ This is joint work with Andreas Weiermann.

(joint work with Jianqi Li)

A class of set-theoretic functions, predicatively computable set functions, is introduced, and each function in the class is shown to be polynomial time computable on hereditarily finite sets. I plan to discuss some open problems on the class such as complexity analysis by term rewriting and formal theory proving the totality of functions in the class.

Consider the following problem: given a simply typed lambda term of Boolean type and of order $r$, does it normalize to "true"? A related problem is: given a term $M$ of word type and of order $r$ together with a finite automaton $D$, does $D$ accept the word represented by the normal form of $M$? We prove that these problems are $n$-EXPTIME complete for $r = 2n + 2$, and $n$-EXPSPACE complete for $r = 2n + 3$. While the hardness part is routine (encoding Turing machines), the membership part is not so obvious; in particular, simply applying beta reduction does not work. Some preceding works employ semantic evaluation in the category of sets and functions, but it is not efficient enough for our purpose. We present an algorithm for the above problems that is a fine blend of beta reduction, Krivine abstract machine and semantic evaluation in a category based on preorders and order ideals, also known as the Scott model of linear logic. The semantic evaluation can also be presented as intersection type checking. This work was presented at RTA 2012 in Nagoya.

How to draw an automaton on a surface without crossing edges? We describe the problem and we introduce the concept of genus. We show that the size of alphabets plays a key role, we prove that there is no equivalent to Myhill-Nerode Theorem. We extract some general properties to compute the genus of regular languages. (joint work with Florian Deloup)

TCT is an automated complexity prover for rewrite systems, and implements a majority of the techniques found in the literature. In this talk we will see the combination framework underlying TCT, and a novel technique which allows TCT to decompose the analysed systems into more manageable pieces.

Interaction nets form a local and strongly confluent model of computation that is per se parallel. However, the elegance of nets comes at some cost: interaction nets crucially lack a sufficient amount of structure that directly yields for a correctness criteria. We introduce a deep inference presentation of linear logic that provides a type system for nets. We believe (work in progress) that it inherits their strong confluence and admits strong normalisation. The normalisation proof is an adaptation of Girard's reducibility method and thus modular and readily gives rise to generalisations (e.g. polymorphism).

This a joint work with Tom Gundersen and Willem Heijtjes. We present an explicit–sharing lambda calculus based on a Curry–Howard-style interpretation of of deep-inference formalisation of intuitionistic logic. Duplication of subterms during reduction proceeds `atomically', i.e. on individual constructors, similar to optimal graph reduction in the style of Lamping. This explicit–sharing lambda calculus admit a sequent-based type system, preserves strong normalisation with respect to the lambda-calculus, and achieves fully lazy sharing.

In this talk we introduce the notion of map, which is a notation for occurrence of a symbol in syntactic expressions such as formulas or λ-terms. We use binary trees over 0 and 1 as maps, but some well-formedness conditions are required. We develop a representation of lambda terms using maps. The representation is concrete (inductively definable in HOL or Constructive Type Theory) and canonical (one representative per λ-term). We define substitution for our map representation, and prove the representation is in substitution preserving isomorphism with both nominal logic λ-terms and de Bruijn nameless terms. These proofs are mechanically checked in Isabelle/HOL and Minlog respectively.

The map representation has good properties. Substitution does not require adjustment of binding information: neither α-conversion of the body being substituted into, nor de Bruijn lifting of the term being implanted. We have a natural proof of the substitution lemma of λ calculus that requires no fresh names, or index manipulation.

Using the notion of map we study conventional raw λ syntax. E.g. we give, and prove correct, a decision procedure for α-equivalence of raw λ terms that does not require fresh names. (joint work with Randy Pollack, Helmut Schwichtenberg and Takafumi Sakurai)

Girard showed that every type of sort $*$ (i.e., every proposition) is inhabited in λU. Barendregt states without proof that every type of sort $\Box$ (i.e., every domain) is also inhabited in the system. In this talk we show that the second statement is not the case by giving a partial translation from λU to λ2.

The aim of implicit computational complexity is to provide model of complexity classes. These models are all based on a data ramification, which governs the information data flow inside a computation. Recently (lics'11), we have shown that the mechanism controlling the data flow is similar to the ones investigated in security-typed programming languages. Another important feature is the data structure on which the computation is run. We introduce an imperative language with pointers based on while-loops and recursive function calls. The domain of computation consists of first-order structures like in Hofmann and Schöpp works. However here, structures may evolve during a computation. For this, there are a new and a free operations. As a result, the data structure is closed to records, C-struct construction or to objects. We establish a characterization of PTime. This work takes inspiration from reference machines like Kolmogorov Uspensky machines, Schönhage's machines, and Gurevich's abstract state machines.

In earlier work we introduced the programming language Purple to formalise the common intuition of logspace-algorithms as pure pointer programs that take as input some structured data (e.g. a graph) and store in memory only a constant number of pointers to the input (e.g. to the graph nodes). It was shown that Purple is strictly contained in logspace, being unable to decide s-t-connectivity in undirected graphs.

We study the options of strengthening Purple as a manageable idealisation of computation with logarithmic space that may be used to give some evidence that Ptime-problems such as Horn satisfiability cannot be solved in logarithmic space. We show that with counting, Purple captures all of logspace on locally ordered graphs. Our main result is that without a local ordering, even with counting and nondeterminism, Purple cannot solve tree isomorphism. This generalises the same result for Transitive Closure Logic with counting, to a formalism that can iterate over the input structure, furnishing a new proof as a by-product.

The talk will outline this result which will be presented at Fossacs 2013 and put it in perspective. This is joint work with Ramyaa Ramyaa and Uli Schoepp.

In this lecture we will present analytic calculi representing the proof of validity for first order formulas in nonclassical logics. We will focus on the comparison of classical calculi for Kripke semantics and LJ. As corollaries we obtain versions of full Skolemization, Herbrand Theorems etc. (joint work with Georg Moser)

In our quest for understanding the expressive power of standard first order language over linear orders, we present recent separation results between logics of linear Kripke frames with constant domains of order type of an ordinal up to $\omega^\omega$. These separation results are carried out in a monadic language with one predicate symbol only. (joint work with Arnold Beckmann)

Various approaches to automatically synthesizing termination proofs via matrix interpretations are used in state-of-the-art provers, most notably those based on satisfiability solving. In this talk, an alternative idea for the particular case of string rewriting is presented, exploiting the view of matrix interpretations as weighted automata. A demo of a prototype implementation will show the utility of this approach, as well as its limitations.

In this talk, based on joint work with Aart Middeldorp, we present a confluence criterion that generalises orthogonality (Rosen, 1973) and Knuth and Bendix' criterion (1970) for left-linear term rewrite systems. The result is extended so as to subsume weak orthogonality by using van Oostrom's orthogonalisation technique, in which proof terms play a crucial role.

In this talk we study amortised cost analysis for constructor rewrite systems $\mathcal{R}$ and show that well-typedness yields the existence of typed polynomial interpretations that orients $\mathcal{R}$. (joint work with M. Hofmann)

We introduce a linear infinitary lambda calculus, and study its basic properties. It is a linear lambda calculus where not only finite but also infinite terms can be built. Two exponential modalities are available, the first one being the usual, finitary one, the other being the only coinductive construct. The obtained calculus embeds the infinitary applicative lambda calculus and is universal for computations over infinite strings. What is particularly interesting, however, is that the refinement induced by linear logic allows to restrict both modalities, so as to get calculi which are terminating inductively and productive coinductively. We exemplify this idea by analyzing a fragment of the calculus built around the principles of SLL and 4LL. Interestingly, it enjoys weak normalization and confluence, contrarily to what happens in ordinary infinitary lambda calculi.