News
- Feb 27, 2013: Fixed the program.
- Feb 26, 2013: Added link to map and tentative program.
- Feb 25, 2013: Banquet registration was closed.
- Oct 29, 2012: Added hotel informations.
- Sep 6, 2012: The workshop dates and venue were changed.
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).
Scope
We solicit presentations on the following topics:- proof theory and applications
- classical logic, intuitionistic logic, linear logic
- term rewriting, higher-order rewriting, graph rewriting
- typed/untyped lambda calculi
- complexity analysis, implicit computational complexity
- decidability, computability
- theorem proving
- ...
Venue
The workshop takes place at the next venue:Ishikawa Prefectural Museum of Art
2-1 Dewa-machi, Kanazawa, Ishikawa, Japan
map
Schedule
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 |
Program
Monday
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 |
Tuesday
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. |
Wednesday
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 – |
Thursday
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) |
Friday
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)
1-8-21 Katamachi, Kanazawa
Speakers
- Toshiyasu Arai (Chiba University)
- Martin Avanzini (University of Innsbruck)
- Matthias Baaz (University of Technology, Vienna)
- Arnold Beckmann (Swansea University)
- Josef Berger (University of Greifswald)
- Frédéric Blanqui (INRIA-LIAMA)
- Guillaume Bonfante (LORIA)
- Ulrik Buchholtz (Stanford University)
- Ugo Dal Lago (Bologna)
- Naohi Eguchi (Tohoku University)
- Nao Hirokawa (JAIST)
- Dieter Hofbauer (ASW BA Saarland)
- Martin Hofmann (LMU München)
- Jean-Pierre Jouannaud (École Polytechnique)
- Ulrich Kohlenbach (TU Darmstadt)
- Gyesik Lee (Hankyong National University)
- Jean-Yves Marion (LORIA)
- Aart Middeldorp (University of Innsbruck)
- Georg Moser (University of Innsbruck)
- Keisuke Nakano (University of Electro-Communications, Tokyo)
- Michel Parigot (CNRS, Paris)
- Florian Pelupessy (Ghent University)
- Norbert Preining (JAIST)
- Sam Sanders (Ghent University)
- Masahiko Sato (Kyoto University)
- Helmut Schwichtenberg (LMU München)
- Stéphane Gimenez (University of Innsbruck)
- Christian Sternagel (JAIST)
- Kazushige Terui (Kyoto University)
- Toshihiko Uchida (SOKENDAI, Tokyo)
- Johannes Waldmann (HTWK Leipzig)
- Gunnar Wilken (OIST)
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).- APA hotels (search at
www.expedia.com
with keywords ``Kanazawa Japan'')
- APA Hotel Kanazawa-Katamachi
- APA Hotel Kanazawa-Chuou
- APA Villa Hotel Kanazawa-Katamachi
- Kanazawa Excel Hotel Tokyu
- Toyoko Inn Kanazawa Kenroku
- Hotel Econo
Organising Committee
- Nao Hirokawa (JAIST)
- Hajime Ishihara (JAIST)
- Georg Moser (University of Innsbruck)
- Mizuhito Ogawa (JAIST)
- Norbert Preining (JAIST)
- Satoshi Tojo (JAIST)
Logic Related Events
- Computability Theory and Foundations of Mathematics, Tokyo Institute of Technology, Tokyo, Japan, February 18 - 20, 2013
- Prof. Futatsugi's Retirement Lecture, JAIST, Nomi, 15:30 - 17:30, March 8, 2013