Hans Zantema

Infinitary rewriting and streams

Hans Zantema (Eindhoven University of technology)

Find the material for this lecture here.

Infinitary rewriting consists of rewriting of possibly infinite terms in possibly infinitely many steps. Streams are infinite sequences; they can be specified as normal forms in infinitary rewriting, but also in many other ways. We will give an overview of them, and also present rewriting based techniques to answer basic questions on well-definedness, productivity and equality of streams, and also ways to visualize them.

Outline of the lecture

Infinitary rewriting

Term rewriting is usually defined by applying a term rewriting system (TRS) on finite terms, but the same TRS can also be applied on infinite terms in a natural way. But then it is natural to consider reductions of infinitely many steps, having some converging behaviour. This view changes some of the natural basic properties like termination and confluence. We will present some preliminaries of infinitary rewriting, as is also presented in [1, 2, 3].

Streams

Streams are infinite sequences over some alphabet, and can be seen as infinitary terms in which the alphabet symbols are unary symbols, and there are no other symbols. Many streams can be defined as infinitary normal forms of some finite starting term with respect to some finite TRS, but they can also be defined by a number of equations. For instance, the Fibonacci stream fib = 010010100100101… is the fixed point of the operation f replacing every 0 by 01 and every 1 by 0, and can be defined by the three equations

fib = f(fib); f(0(x)) = 0(1(f(x))); f(1(x)) = 0(f(x)).

Several techniques have been developed to check whether a set of equations uniquely defines a stream ([5, 4, 6]), or whether the equations produce all elements of the stream one by one ([9], or whether two sets of equations define the same stream ([8]). For all of these techniques the focus is on doing this fully automatically: just type in the specification, and let the tool automatically find a proof based on the techniques developed in these papers.

Visualization

Typically, streams defined by equations are non-periodic, but often have a self-similar character. Sometimes this is nicely shown by turtle graphics: process the stream by which by every symbol a particular action is performed, like drawing a segment and turning the drawing direction. This is elaborated in [7]. Doing this for the fixed point of the morphism mapping 0 to 001100 and 1 to 001101, choosing appropriate turning angles yields the following self-similar turtle visualization:



Exercises or experiments

These lectures will not only consist of presenting the topics and underlying theory, but also of doing exercises in applying the underlying proof principles.

Bibliographical references

  1. R. Kennaway and F.-J. de Vries. Infinitary rewriting. In Term Rewriting Systems, by Terese, pages 668–711. Cambridge University Press, 2003.
  2. R. Kennaway, P. Severi, R. Sleep, and F.-J. de Vries. Infinitary rewriting: From syntax to semantics. In A. Middeldorp, V. van Oostrom, F. van Raamsdonk, and R. de Vrijer, editors, Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday, volume 3838 of Lecture Notes in Computer Science, pages 148–172. Springer, 2005.
  3. H. Zantema. Normalization of infinite terms. In A. Voronkov, editor, Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA), volume 5117 of Lecture Notes in Computer Science, pages 441–455. Springer, 2008.
  4. H. Zantema. A tool proving well-definedness of streams using termination tools. In A. Tarlecki A. Kurz, M. Lenisa, editor, Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, volume 5728 of Lecture Notes in Computer Science, pages 449–456. Springer, 2009.
  5. H. Zantema. Well-definedness of streams by termination. In R. Treinen, editor, Rewriting Techniques and Applications, 20th International Conference, RTA 2009, volume 5595 of Lecture Notes in Computer Science, pages 164–178. Springer, 2009.
  6. H. Zantema. Well-definedness of streams by termination. Logical Methods in Computer Science, 6(3), 2010. paper 21, 27 pages.
  7. H. Zantema. Turtle graphics of morphic sequences. Fractals, 24(1), 2016. preversion available at http://www.win.tue.nl/~hzantema/turtle.pdf.
  8. H. Zantema and J. Endrullis. Proving equality of streams automatically. In M. Schmidt-Schlauss, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, volume 10 of Leibniz International Proceedings in Informatics (LIPIcs), pages 393–408, Dagstuhl, Germany, 2011. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
  9. Hans Zantema and Matthias Raffelsieper. Proving productivity in infinite data structures. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 401–416, Dagstuhl, Germany, 2010. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.

Comments are closed.