Term Rewriting Seminar
18 June 2019, Amsterdam, The Netherlands
The TeReSe meetings started with a festive meeting in Amsterdam celebrating the publication of the TeReSe book. Traditionally, the format of this meeting is an afternoon of presentations with room for discussions over dinner. Previous meetings were in Amsterdam, Eindhoven, Utrecht, Eindhoven, Aachen, Amsterdam, Utrecht, Eindhoven, Aachen, Amsterdam, Nijmegen, Utrecht, Aachen, Amsterdam, Eindhoven, Utrecht, Aachen, Amsterdam, Nijmegen, Aachen, Eindhoven, and Nijmegen.
Please send an email to Alexander Bentkamp if you would like to participate.
|13:00 – 13:15|
|13:15 – 13:50||
Reasoning about one-sided and two-sided infinite sequences.
We recapitulate first order inductive theorem proving in a general setting without requirements on the shape of the equations involved. We show how this applies to settings in which the terms on which induction is applied do not have a unique representation as constructor terms. In this way we can do induction over the integers rather than over the natural numbers. We show how this induction mechanism can be applied to prove equality of infinite sequences, and how this is closely related to circular coinduction. As one-sided sequences can be defined as mappings from natural numbers to some basic type, we can also consider two-sided infinite sequences being mappings from integers to the base type, and apply the induction principle over the integers to prove equality of these. In particular we consider a two-sided variant of morphic sequences.
|13:50 – 14:25||
Proving Non-Termination via Loop Acceleration
We present a new approach to prove non-termination of integer programs. It is based on a novel under-approximating loop acceleration technique, a new sufficient criterion to detect non-termination, and an SMT encoding to search for invariants. To evaluate our technique, we implemented it in our tool LoAT. A comparison with other leading termination analyzers for integer programs shows that it is competitive and can prove non-termination of some programs where existing tools fail.
|14:25 – 15:00||
Higher-order Polymorphic Polynomials
We generalise the termination method of higher-order polynomial interpretations to a setting with impredicative polymorphism. Instead of using weakly monotonic functionals, we interpret terms in a suitable extension of System Fω. This enables a direct interpretation of rewrite rules which make essential use of impredicative polymorphism. In addition, our generalisation eases the applicability of the method in the non-polymorphic setting by allowing for the encoding of inductive data types. As an illustration of the potential of our method, we prove termination of a substantial fragment of full intuitionistic second-order propositional logic with permutative conversions.
|15:00 – 15:30|
|15:30 – 16:05||
Constant Runtime Complexity of Term Rewriting is Semi-Decidable
We show that it is semi-decidable whether the runtime complexity of a term rewrite system is constant. Our semi-decision procedure exploits that constant runtime complexity is equivalent to termination of a restricted form of narrowing, which can be examined by considering finitely many start terms. We implemented our semi-decision procedure in the tool AProVE to show its efficiency and its success for systems where state-of-the-art complexity analysis tools fail.
|16:05 – 16:40||
The Embedding Path Order for Lambda-Free Higher-Order Terms
I will present a variant of RPO for higher-order terms without lambda-abstractions. Being a ground-total simplification order, it appears promising for higher-order superposition. I developed an algorithm to compute the order reasonably fast and implemented it in the Zipperposition theorem prover.
|16:40 – 17:00||
TeReSe Business Meeting
Afterwards there will be a joint TeReSe dinner at wagamama close to the Amsterdam Zuid station within walking distance of the university.
The workshop will take place on 18 June 2019 in the BelleVUe building of the Vrije Universiteit Amsterdam, room BV-0H36. The VU is easily accessible on foot from the Amsterdam Zuid station. See How to get to VU Amsterdam for details.