JAIST Logic Workshop Series

3rd Workshop on Proof Theory and Rewriting

4 (Mon) – 8 (Fri) March, 2013
Kanazawa, Japan


About This Workshop

The workshop aims at bringing together researchers in proof theory and rewriting to facilitate the exchange of ideas between these tightly connected fields. The workshop is organised as informal one, and not only presentations about published results but also about work in progress are welcome. We welcome participants from all areas, but due to space restrictions in the venue, we kindly ask to contact Nao Hirokawa beforehand.

Previous editions of the workshop were held in Obergurgl (2010) and Obergurgl (2006).


We solicit presentations on the following topics:


The workshop takes place at the next venue:
Hall in the main museum (March 4-6, 8); seminar room in the Hirosaka-Bekkan (March 7)
Ishikawa Prefectural Museum of Art
2-1 Dewa-machi, Kanazawa, Ishikawa, Japan
Main Building of Ishikawa Prefectural Art Museum Hirosaka Annex of Ishikawa Prefectural Art Museum
which is located in the famous sightseeing spot of Kanazawa, including Kenrokuen (Six Attributes Garden), Kanazawa Castle, 21st Century Museum of Contemporary Art, etc... See Kanazawa Tourist Information Guide for more places (in particular, home → tour guide → 01).
Kenrokuen Kanazawa Castle 21st Century Museum


4 (Mon)5 (Tue)6 (Wed) 7 (Thu)8 (Fri)
9:00 – 10:20
10:20 – 10:40 coffee break
10:40 – 12:00
12:00 – 13:30 lunch closing
13:30 – 14:50
14:50 – 15:10 coffee break
15:10 – 17:00 Prof. Futatsugi's Retirement Lecture at JAIST
19:00 – banquet



09:10 - 12:00 Fluctuations, Effective Learnability and Metastability in Analysis (50 min)
Ulrich Kohlenbach

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)

– Coffee Break –

[Termination and Certification]

Rewrite Properties and Presburger Logic (35 min)
Johannes Waldmann

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.

Formalizing the Order-Extension Principle in Isabelle/HOL
Christian Sternagel

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.

– Lunch –

13:30 - 16:50 Reuniting the Antipodes: Bringing together Nonstandard and Constructive Analysis (60 min)
Sam Sanders

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.

– Coffee Break –

A Short Proof of Two Ramsey Like Independence Results
Florian Pelupessy

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$.

Constructive Formulation of the Big 5 Subsystems of Second-Order Arithmetic
Gyesik Lee


09:10 - 12:00 Beyond Peano Arithmetic - Automatically Proving Termination of the Goodstein Sequence (50 min)
Aart Middeldorp

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.

– Coffee Break –

The Unfolding of ID1
Ulrik Buchholtz

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.

Higher Type Computation and Rewriting (45 min)
Helmut Schwichtenberg

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.

– Lunch –

13:30 - 16:50 On Higman's Lemma (30 min)
Josef Berger

Termination Orderings over Term Graphs (35 min)
Naohi Eguchi

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.

– Coffee Break –

Total NP Search Problems for Second-Order Bounded Arithmetic and Improved Witnessing (45 min)
Arnold Beckmann

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.

Goodstein Sequences for Prominent Ordinals up to the Ordinal of $\Pi_1^1$-$\mathit{CA}_0$
Gunnar Wilken

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.


09:10 - 12:00 [Higher-Order]

Formalization of Lambda-Calculus and Tait-Girard's Computability Predicates (Work in Progress)
Frédéric Blanqui

Dependent Computability Path Ordering (35 min)
Jean-Pierre Jouannaud

(joint work with Jianqi Li)

– Coffee Break –

[Logic and Complexity]

Predicatively Computable Functions on Hereditarily Finite Sets (40 min)
Toshiyasu Arai

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.

Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus
Kazushige Terui

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.

– Lunch –

13:30 - 16:50 On the Genus of Regular Languages (35 min)
Guillaume Bonfante

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)

A Combinatorial Framwork for Complexity (45 min)
Martin Avanzini

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.

– Coffee Break –

[Deep Inference]

The Structure of Interaction
Stéphane Gimenez

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).

Atomic Lambda Calculus: A Typed Lambda-Calculus with Explicit Sharing tba
Michel Parigot

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.

19:00 - 21:00 – Banquet –


09:10 - 12:00 Viewing Lambda-Terms through Maps (45 min)
Masahiko Sato

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)

– Coffee Break –

[Lambda and CL]

A Partial Translation from λU to λ2
Toshihiko Uchida

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.

Repetitive Right Applications of B Terms (30 min)
Keisuke Nakano

– Lunch –

13:30 - 16:50 [Complexity]

Information Flow and Evolving Structures
Jean-Yves Marion

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.

Pure Pointer Programs and Tree Isomorphism
Martin Hofmann

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.

– Coffee Break –

[Proof Theory]

Proof Theoretic Representation of Semantic Validation
Matthias Baaz

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)

Expressivity of One Monadic Predicate Symbol over Linear Kripke Frames with Constant Domains
Norbert Preining

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)


09:10 - 12:00 [Confluence and Termination]

Synthesizing Matrix Interpretations via Backward Completion (35 min)
Dieter Hofbauer

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.

Confluence and Proof Terms (35 min)
Nao Hirokawa

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.

– Coffee Break –

[Complexity and Lambda]

Amortised Cost Analysis for Term Rewriting Systems (45 min)
Georg Moser

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)

Infinitary Lambda Calculi from a Linear Viewpoint
Ugo Dal Lago

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.

12:00 – Closing –

Banquet on March 6 (Wed)

Bistro Kamiya Ichibee
1-8-21 Katamachi, Kanazawa


Access to Kanazawa

from Tokyo Narita Airport to Kanazawa Station:

Please take a limousine bus to Haneda Airport (HND), fly to Komatsu Airport (KMQ), and then take an airport bus (time table) to Kanazawa. Note that there are also direct flights between Narita and Komatsu (but not many).

from Kansai International Airport to Kanazawa Station:

Please take a suitable train (type "Kansai Airport" in "From" and "Kanazawa" in "To"). Since trains are going frequently, you can simply take the next one. You must change trains at Shin-Osaka. For general information, please see this website. The site describes how to get to Fukui (a city between Shin-Osaka and Kanazawa) in great detail, including instructions for buying tickets and changing trains.

from Kanazawa Station to Venue and Hotels around Venue:

The easiest way is to go by taxi (approx 1,000 yen) from the station.

Hotels in Kanazawa

We recommend to stay at a hotel in the center of the city (Katamachi or Korinbou) rather than one around Kanazawa Station. Here we list a few hotels (4,000 – 10,000 JPY). You may find many other hotels at: Rakuten Travel

Organising Committee

Logic Related Events