IWC+WST schedule and local information

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: Conway’s Game of Life and other orthogonal rewrite systems (invited talk)

      We show how Conway’s Game of Life (GoL) can be modelled by means of orthogonal graph rewriting. More precisely, we model GoL by means of a graph rewrite system where each cell of the grid is represented by a node having 8 ports, each linked to one of its 8 neighbouring nodes. A rewrite rule then lets a node cyclically rotate its principal port to the next (either widdershins or deosil) port while updating its alive-neighbour-count. After a full rotation, its state is updated accordingly. We show this yields a graph rewrite system (GRS) where computing the next GoL-iteration may be achieved in 8 ticks by means of what we call ©locksteps better known in rewriting as full multisteps contracting all redex-patterns in the graph in parallel. The GRS being orthogonal liberates one from having to perform ©locksteps only, to always contract all redex-patterns: orthogonality makes that redex-patterns may be contracted asynchronously, even one at the time, need not be contracted in lockstep. There are no clogsteps (so to speak), making the modelling ideally suited for implementation on GPUs.

      In the second part of the presentation we show in what sense the graph rewrite system used to model GoL in the first part is orthogonal. We show it constitutes a so-called Interaction Net (IN) and that a (single) step from graph G to graph H with respect to rule rule ρ : L → R can be decomposed into three phases:

      1. the matching phase, an SC-expansion GSC↞ C[L] exhibiting the to-be-replaced substructure L within G;
      2. the replacement C[L] → C[R] of the exihibited substructure L, left-hand side of rule ρ, by its right-hand side R;
      3. the substitution phase, an SC-reduction C[R] ↠SC H plugging-in the substructure R yielding H.

      Here SC stands for Substitution Calculus, the calculus used for abstracting subgraphs into variables and substituting for them again (matching and substitution). In the case of INs the SC is particularly simple, and consists essentially in managing indirection nodes. We exemplify this decomposition extends to term rewrite systems (TRSs; having the simply typed λαβη-calculus as SC) and to term graph rewrite systems (TGRSs; having an SC, the ж-calculus, based on sharing), putting INs on a par with orthogonal TRSs and orthogonal TGRSs, thereby unlocking the theory of orthogonality to GoL and other cellular automata. For instance, that INs are confluent, even has least upperbounds, is an immediate consequence of orthogonality (confluence-by-parallelism).

      References: there being an abundance of literature on Game of Life and on Interaction Nets, we only give references to the lesser-known approach to structured rewriting by means of Substitution Calculi:

  • 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: Confluence of Conditional Rewriting Modulo (invited talk) 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
  • 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)
      • climb Mount Fockeberg (map)
    • 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:25 - 11:45 IWC Session 6 = WST Session 1 (session chair: Johannes Waldmann)

    • 10:25 Lutz Engisch (Vice Dean, Fakultät Informatik und Medien, HTWK): Welcome Address
    • 10:30 Aart Middeldorp: Termination and Confluence: Remembering Hans Zantema (invited talk) 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 (session chair: Aart Middeldorp)

    • 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, slides

  • 13:00 lunch

  • 14:30 - 15:30 WST Session 3 (session chair: Pierre Lescanne)

    • 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 (session chair: Salvador Lucas)
    • 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, slides
    • 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 (session chair: Carsten Fuhs)
    • 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 (session chair: Jürgen Giesl)
    • 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, slides
    • 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 (session chair: Dieter Hofbauer)
    • 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)