Location
workshops at Gutenberg Building (Gustav-Freytag-Straße
40) (street
map, building
map, campus
views), in these rooms (all on the first floor):
- Gu 110: registration, coffe breaks
- Gu 101: talks
- Gu 102: available for self-study and meetings
lunch at Mensa Academica (across Gustav-Freytag
street)
Monday September 1st
19:00 informal pre-workshop meeting, Restaurant Connstanze, map.
I (JW) book a table, everyone pays for themselves. If you
want to join, tell me by email.
Tuesday September 2nd
(IWC)
- 08:30 registration
- 09:00 - 10:00 IWC Session 1
09:00 Vincent van Oostrom (invited talk): Conway’s Game
of Life and other orthogonal rewrite systems
- 10:00 coffee
- 10:30 - 12:30 IWC Session 2
10:30 Jonas Schöpf and Aart Middeldorp: Improving
Confluence Analysis for LCTRSs
We lift two well-known confluence techniques—the
redundant rules technique and the reduction method—from term
rewrite systems to logically constrained term rewrite
systems. We establish sufficient criteria for both
techniques in the constrained setting, increasing
flexibility of confluence analysis.
11:00 Johannes Niederhauser and Aart Middeldorp: Towards
Confluence of Deterministic Higher-Order Pattern Rewrite
Systems by Critical Pairs
We generalize the concept of critical pairs from
Nipkow’s pattern rewrite systems to higher-order rewrite
systems where the left-hand sides of rules can be
deterministic higher-order patterns.
11:30 Makoto Hamana and Koko Muroya: Term Evaluation
Systems with Refinements for Contextual Improvement by
Critical Pair Analysis
For a programming language, there are two kinds of
term rewriting: run-time rewriting (“evaluation”) and
compile-time rewriting (“refinement”). Whereas refinement
resembles general term rewriting, evaluation is commonly
constrained by Felleisen’s evaluation contexts. While
evaluation specifies a programming language, refinement
models optimisation and should be validated with respect to
evaluation. Such validation can be given by Sands’ notion of
contextual improvement. We formulate evaluation in a
term-rewriting-theoretic manner for the first time, and
introduce Term Evaluation and Refinement Systems (TERS). We
then identify sufficient conditions for contextual
improvement, and provide critical pair analysis for local
coherence that is the key sufficient condition. As case
studies, we prove contextual improvement for a computational
lambda-calculus and its extension with effect handlers.
12:00 Rémy Cerda and Lionel Vaux Auclair: Confluence of
001- and 101-infinitary λ-calculi by linear
approximation
The introduction of infinitary rewriting and in
particular of infinitary λ-calculi created a syntactic
bridge between the dynamics of rewriting systems and their
semantics. Confluence, already a highly desirable property
for a finitary rewriting system, becomes even more important
in this setting as it ensures uniqueness of infinitary
normal forms. A seemingly orthogonal line of work led to the
advent of a linear approximation of the λ-calculus based on
Taylor expansion, which allowed for a renewal and a
refinement of the classic approach based on continuous
approximation, and for a whole range of new, elegant proofs
of key results in λ-calculus. In previous work (Cerda and
Vaux Auclair, LMCS, 2023), we demonstrate how infinitary
λ-calculus appears to be the “missing ingredient” thanks to
which we could give a general, canonical presentation of the
linear approximation of the λ-calculus. In this talk, we
take a somehow dual perspective and explain what linear
approximation brings to infinitary λ-calculi. In particular,
we present a linear “Simulation” theorem for the 001- and
101-infinitary λ-calculi, and detail how confluence of the
given infinitary λ-calculi can be deduced. We also evoke the
remaining infinitary λ-calculi, stating a negative result
preventing the construction of a suitable linear
approximation.
- 12:30 lunch
- 14:00 - 15:30 IWC Session 3
14:00 Salvador Lucas (invited talk): Confluence of
Conditional Rewriting Modulo
Sets of equations E play an important
computational role in rewriting-based systems R
by defining an equivalence relation =E
inducing a partition of terms into E-equivalence
classes on which rewriting computations, denoted
→R/E and called
rewriting modulo E, are issued. This paper
investigates confluence of
→R/E, usually called
E-confluence, for conditional
rewriting-based systems, where rewriting steps are
determined by conditional rules. We rely on Jouannaud and
Kirchner’s framework to investigate confluence of an
abstract relation R modulo an abstract
equivalence relation E on a set A. We
show how to particularize the framework to be used with
conditional systems. Then, we show how to define appropriate
finite sets of conditional pairs to prove and
disprove E-confluence. Our results apply to
well-known classes of rewriting-based systems. In
particular, to Equational (Conditional) Term Rewriting
Systems.
15:00 René Thiemann and Akihisa Yamada: Deciding pattern
completeness in non-deterministic polynomial time
Pattern completeness is the property that the
left-hand sides of a functional program or term rewrite
system cover all cases w.r.t. pattern matching. This or
related properties are required, if one wants to perform
ground confluence proofs by rewriting induction. In order to
certify such confluence proofs, we develop a novel algorithm
that decides pattern completeness. The algorithm has an
asymptotic optimal complexity, as it belongs to the
complexity class co-NP. It has been verified in Isabelle/HOL
and outperforms existing algorithms, even including the
pattern completeness check of the GHC Haskell compiler.
- 15:30 coffee
- 16:00 - 17:30 IWC Session 4
- Confluence Competition
- Business Meeting
Recommendations for exploring the city (on your own)
- locally: from Connewitz Kreuz/HTWK, walk
Karl-Liebknecht-Straße (north), or Bornaische Straße
(south),
- enjoy pubs (style: student, alternative)
- watch Löffelfamilie
(map)
near Südplatz (south from city, but north from here)
- city center:
- restaurants in Barfußgäßchen, Gottschedstraße (style:
tourist, business)
- cyclops ring the bells at Kroch-Hochhaus
- rooftop viewing platform (31st floor) at Panorama
Tower
Wednesday
September 3rd (IWC and WST)
08:30 registration
09:00 - 10:00 IWC Session 5
9:00 Raúl Gutiérrez and Salvador Lucas: Proving and
disproving feasibility with infChecker
Given a first-order theory Th, we say that
a boolean combination F of atoms is
Th-feasible if there is a substitution σ such
that σ(F) is deducible from Th, i.e.,
Th ⊢ σ(F) holds. Otherwise,
F is infeasible. In the realm of (conditional)
term rewriting, many interesting problems can be treated as
(in)feasibility problems: joinability of terms (and critical
pairs), reachability, reducibility, etc. This paper shows
how general feasibility problems can be handled now with the
new version of the tool infChecker.
9:30 Vincent van Oostrom: Redeeming Newman;
orthogonality in rewriting - Past, present and future in a
1-algebraic setting
Despite sixty percent of Newman’s seminal 1942 paper
being devoted to residual theory, that remains obscure due
to that his instantiation of the theory there to the
(non-erasing) λβ-calculus was fatally flawed. We redeem the
approach showing: 1) any rewrite system instantiating his
theory induces a so-called 1-ra, an axiomatically orthogonal
rewrite system, entailing co-initial reductions have least
upperbounds; 2) the rewrite system underlying any
(non-erasing) syntactically orthogonal TRS instantiates his
theory.
10:00 coffee
10:30 - 11:45 IWC Session 6 = WST Session 1
Aart Middeldorp (invited talk): Termination and
Confluence: Remembering Hans Zantema
In this presentation I give an incomplete overview of
the many contributions of Hans Zantema to
termination and confluence. Several of these were presented
at earlier workshops on termination
and confluence
and I include a biased overview of the development of these
workshops and associated competitions (CoCo, termcomp).
paper
11:45 short break
12:00 - 13:00 WST Session 2
12:00 Ulysse Le Huitouze and René Thiemann: Core matrix
interpretations for proving termination of term rewrite
systems
Matrix interpretations are powerful techniques for
proving termination of term rewrite systems. Among them, the
original paper that introduced the matrix interpretation
technique, originally aimed at string rewriting, also
described sets of matrices that inherently provide a
well-founded relation and its required monotonic properties,
simplifying proofs. To the extent of our knowledge, these
special sets of matrices have not yet explicitly been used
in a term rewriting setting. We report on the generalisation
of these sets of matrices to a term rewriting setting. All
results have been formalised in Isabelle/HOL and are
integrated in the CeTA certifier. paper
12:30 Reinis Cirpons, James D. Mitchell and Finn L. Smith:
Off with the head: termination provers and the word
problem for 1-relation monoids
In this talk I will showcase a new set of SRS
termination problems arising from the word problem in
1-relation monoids. The word problem is a central object of
study in combinatorial semigroup theory. Despite being
undecidable in general, its decidability is open when
restricted to 1-relation monoids. Motivated by recent
efforts in solving this problem, we launched a quantitative
investigation with the goal of formally proving as many
small instances of the 1-relation monoid word problem as
possible. This naturally lead us to utilize termination
provers to solve SRS arising from many challenging
instances. This is joint work with Florent Hivert
(Université Paris Saclay), Assia Mahboubi (Nantes
Université), Guillaume Melquiond (Université Paris Saclay),
James D. Mitchell (University of St Andrews) and Finn L.
Smith (University of St Andrews). paper
13:00 lunch
14:30 - 15:30 WST Session 3
14:30 Carsten Fuhs, Liye Guo and Cynthia Kop: Dependency
Pairs for Innermost Constrained Higher-Order Rewriting
Logically constrained simply-typed term rewriting
systems (LCSTRSs) provide a form of rewriting geared towards
analysis of programs with higher-order features and both
algebraic and primitive data types. Termination of LCSTRSs
has been studied for full rewriting without strategy
assumptions. This extended abstract adapts the higher-order
constrained Dependency Pair framework for innermost
termination, which implies termination under call-by-value
evaluation. The DP framework for innermost termination
effectively handles universal computability. This provides a
foundation for open-world termination analysis of programs
using call-by-value evaluation via LCSTRSs. paper
15:00 Johannes Niederhauser and Aart Middeldorp: NCPO
goes Beta-Eta-Long Normal Form
We adapt our recently introduced higher-order
reduction order NCPO to beta-eta-long normal forms which
makes it directly applicable to Nipkow’s higher-order
rewrite systems. paper
15:30 coffee
16:00 IWC + WST excursion and dinner
Thursday September 4th
(WST)
- 9:00 - 10:30 WST Session 4
9:00 Vincent van Oostrom: Disjunctive Termination for
Affluent Families
We introduce affluence, a condition on composition
that entails a finite family of rewrite relations is
terminating iff its is disjunctive termination, and relate
it to jumping. Our proofs transform infinite reductions in
the family union into such in family members, by induction
on family size. paper
9:30 Etienne Payet: Non-Termination of Term Rewrite
Systems Using Pattern Unfolding
We present a revisit, based on a new unfolding
technique, of an approach introduced in term rewriting for
the automatic detection of non-looping non-termination from
patterns of rules. paper
10:00 Jan-Christoph Kassing, Grigory Vartanyan and Jürgen
Giesl: A Dependency Pair Framework for Relative
Termination of Term Rewriting
Problem 106 of the RTA List of Open Problems asks for
an adaption of dependency pairs for relative termination of
term rewrite systems (TRSs). Here, infinite rewrite
sequences are allowed, but one wants to prove that a certain
subset of the rewrite rules cannot be used infinitely often.
Dependency pairs were recently adapted to annotated
dependency pairs (ADPs) to prove almost-sure termination of
probabilistic TRSs. In this talk, we present an adaption of
ADPs for relative termination. We implemented our relative
ADP framework in our tool AProVE and evaluate it in
comparison to other tools for relative termination of TRSs.
paper
- 10:30 coffee
- 11:00 - 12:30 WST Session 5
11:00 Jan-Christoph Kassing and Jürgen Giesl: Modularity
of Termination in Probabilistic Term Rewriting
We investigate the modularity of probabilistic
notions of termination in term rewriting. In the
probabilistic setting, there are several interesting
termination properties: Almost-sure termination (termination
with probability 1), positive almost-sure termination
(finite expected runtime of each rewrite sequence), and
strong almost-sure termination (expected runtime is bounded
by a constant for each start term). A property is called
modular if it is preserved for certain unions of
probabilistic term rewrite systems. We show that these three
termination properties have different modularity behavior
for innermost rewriting. Utilizing known relations between
innermost and full probabilistic rewriting allows us to
obtain modularity results for full probabilistic rewriting
as well. paper
11:30 Éléanore Meyer and Jürgen Giesl: Deciding
Termination of Simple Randomized Loops
We show that universal positive almost sure
termination (UPAST) is decidable for a class of simple
randomized programs, i.e., it is decidable whether the
expected runtime of such a program is finite for all inputs.
Our class contains all programs that consist of a single
loop, with a linear loop guard and a loop body composed of
two linear commuting and diagonalizable updates. In each
iteration of the loop, the update to be carried out is
picked at random, according to a fixed probability. We show
the decidability of UPAST for this class of programs, where
the program’s variables and inputs may range over various
sub-semirings of the real numbers. In this way, we extend a
line of research initiated by Tiwari in 2004 into the realm
of randomized programs. paper
12:00 Nils Lommen, Éléanore Meyer and Jürgen Giesl:
Control-Flow Refinement for Complexity Analysis of
Probabilistic Programs
Recently, we showed how to use control-flow
refinement (CFR) to improve automatic complexity analysis of
integer programs. While up to now CFR was limited to
classical programs, we extend CFR to probabilistic programs
and show its soundness for complexity analysis. To
demonstrate its benefits, we implemented our new CFR
technique in our complexity analysis tool KoAT. paper
- 12:30 lunch
- 14:00 - 15:30 WST Session 6
14:00 Alfons Geser: On Closures in String Rewriting
The set of overlap closures can be characterized as
the semantics of composition trees. Rewrite systems for
composition trees can be used to prove that the existence of
loops entails the existence of looping forward closures, or
to prove the correctness of a characterization of the set of
right-hand sides of closures. We show that, for a
quasi-terminating string rewrite system, the existence of
cycles is equivalent to the existence of looping forward
closures. This improves upon a result of Guttag et al. 1983.
paper
14:30 René Thiemann: A New Proof for Soundness of
Right-Forward Closures for Termination Analysis
We consider the termination problem of term rewrite
systems (TRSs). Dershowitz proved that termination starting
from arbitrary terms is equivalent to termination starting
from all terms in the right-forward closure (RFC), provided
that the TRS is right-linear or orthogonal. In this paper we
provide a new proof of this result, and also include a later
result that one can weaken orthogonality to locally
confluent overlay TRSs. All proofs have been verified in
Isabelle/HOL. paper
15:00 Dieter Hofbauer and Johannes Waldmann: Cetera:
Certified Termination with Agda
We report on Cetera, a program and library for
checking termination certificates for string rewriting. The
library is certified in the dependently typed proof language
Agda, and we extract Haskell code for the program. For now,
Cetera contains well-founded monotone monoids (instantiated
to weights and standard matrices) and allows modular removal
of rules (by relative termination). We are currently working
on the RFC (right hand sides of forward closures) theorem.
Proofs in Agda are constructive, so they sometimes differ
from standard presentation. paper
15:15 Raúl Gutiérrez and Salvador Lucas: MU-TERM GTRS: A
Tool for Proving Termination of Generalized Term Rewriting
Systems
We present MU-TERM GTRS, a tool designed to prove
termination of Generalized Term Rewriting Systems (GTRSs).
In these systems, rewriting computations are defined by
rules that may include conditions expressed using atoms
defined by Horn clauses—particularly conditions involving
reachability, joinability, and conversion. Termination
control is enhanced through the use of a replacement map,
which explicitly specifies the argument positions of
function symbols where rewriting is allowed. GTRSs offer a
powerful framework for modeling computations in advanced
reduction-based languages such as Maude. paper
- 15:30 coffee
- 16:00 - 17:30 WST Session 7
16:00 Florian Frohn, Carsten Fuhs, Jürgen Giesl,
Jan-Christoph Kassing and Nils Lommen: AProVE: Becoming
Open Source and Recent Improvements
AProVE (Automated Program Verification Environment)
is a tool for fully automatic program verification. More
precisely, AProVE is able to analyze termination,
complexity, and safety of different programming languages,
e.g., Java, C, Haskell, and Prolog. To ensure the
correctness of its analysis, AProVE can generate
certificates that can be checked by external certification
tools. paper
16:15 Nils Lommen, Éléanore Meyer and Jürgen Giesl:
KoAT: An Automatic Complexity Analysis Tool for
(Probabilistic) Integer Programs
KoAT is an automated tool for inferring runtime and
size bounds – and proving termination – of (probabilistic)
integer programs by analyzing program fragments in a modular
way and combining their bounds. It uses multiphase linear
ranking functions to capture execution ``phases’’ of loops
and a technique for so-called triangular weakly non-linear
loops (twn-loops), enabling the analysis of programs with
non-linear arithmetic. paper
- 16:30 Termination Competition
- 17:15 WST Business Meeting
- next WST: when and where? Bring proposals for
hosting!
More Recommendations
Concerts at Thomaskirche
(where Johann Sebastian Bach worked as cantor from 1723 to
1750):
- September 4: 19:00 Michael Wollny (you need
tickets)
- September 5: 18:00 Thomanerchor (no pre-sale tickets, be
there early)