Infinitary term rewriting provides a tool for reasoning about infinite computations and infinite data as we conceptually find them in lazy functional programs. Term graph rewriting, on the other hand, captures the other defining aspect of lazy functional programming: sharing. With the goal of unifying both paradigms, we generalise the infinitary term rewriting theory to term graphs. We follow two approaches known from infinitary term rewriting: one based on a metric and another based on a partial order on term graphs.

In the literature, infinitary term graph rewriting has been dismissed as not being complete w.r.t. infinitary term rewriting. Our results show, however, that partial order infinitary term graph rewriting is sound and complete w.r.t. infinitary term rewriting. Moreover, we show that the partial order-based calculus forms a conservative extension of the metric-based one similarly to the setting of infinitary term rewriting. Using this correspondence between the partial order-based calculus and the metric-based calculus, we are able to derive soundness and a weakened form of completeness for metric infinitary term graph rewriting.

The CRSX system, a functional programming language particularly designed to specify compilers, can be seen as a formalism of higher-order term rewriting. I will discuss this formalism, its peculiarities, and its relation to other higher-order term rewriting formalisms.

The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed λ-calculus is combined with algebraic reduction. Using this theory, we define higher-order polynomial interpretations, and show how the implementation challenges of this technique can be tackled. A full implementation is provided in the termination tool WANDA.

This talk is based on joint work with Cynthia Kop.

We investigate the relationship between finite terms in lambda-letrec, the lambda calculus with `letrec', and the infinite lambda terms they express. As there are easy examples of infinite lambda terms that, intuitively, are not unfoldings of terms in lambda-letrec, we consider the question: How can those infinite lambda terms be characterised that are lambda-letrec-expressible in the sense that they can be obtained as infinite unfoldings of terms in lambda-letrec?

For `observing' infinite lambda terms through repeated `experiments' carried out at the head of the term we introduce two rewrite systems (with rewrite relations) -reg-> and -reg+-> that decompose the term structure, and produce `generated subterms' in two notions. Thereby the sort of the step can be observed as well as its target, a generated subterm. In both systems there are four sorts of decompo- sition steps: -lambda-> steps (decomposing a lambda-abstraction), -@_0-> and -@_1-> steps (decomposing an application into its function and argument), and respectively, -del-> steps (delimiting the scope of an abstraction, for -reg->), and -S-> (delimiting of scopes, for -reg+->). These steps take place on infinite lambda-terms furnished with a leading prefix of abstractions for gathering previously encountered lambda-abstractions and keeping the generated subterms closed. We call an infinite lambda term `regular'/ `strongly regular' if its set of -reg-> -reachable/-reg+-> -reachable generated subterms is finite. Furthermore, we analyze the binding structure of infinite lambda terms with the concept of `binding-capturing chain'.

Utilizing these concepts, we answer the question above by providing two characterizations of lambda-letrec-expressibility. For all infinite lambda terms M, the following statements are equivalent:
(i): M is lambda-letrec expressible;
(ii): M is strongly regular;
(iii): M only has finite binding-capturing chains.

Rewriting notions like termination, normal forms, and confluence can be described in an abstract way referring to rewriting only by a binary relation. Several theorems on rewriting, like Newman's lemma, can be proved in this abstract setting. For investigating possible generalizations of such theorems, it is fruitful to have counter examples showing that particular generalizations do not hold. In this talk a technique is presented to find such counter examples fully automatically by the tool CARPA.

The basic idea is to fix the number of objects of the abstract rewrite system, and to express required conditions in a satisfiability (SAT) formula, and then call a current SAT solver. We give several examples of finite abstract rewrite systems having remarkable properties that are found in this way fully automatically.

We introduce a technique to prove non-termination of term rewrite systems automatically. In contrast to most previous approaches, our technique is also able to detect non-looping non-termination.

This is joint work with Fabian Emmes and Tim Enger.