Thursday, 16th of November 2017, 12:00 – 1:00

Tiling with decreasing diagrams and explicit sharing

SR 1, ICT Building,
Technikerstraße 21a, 6020 Innsbruck


Vincent van Oostrom
Researcher at CL group, University of Innsbruck


Term rewriting is a model of computation in which (functional) programs can be implemented at a natural level of abstraction. For example,  the factorial function can be implemented using two simple term rewrite rules, one for the zero-case and one for the successor-case. Repeatedly applying these rules until none applies anymore, yields the result.

We discuss two aspects of this modelling:
How to establish that a given term rewriting system implements a function (irrespective of what the function actually is)?
Will a result be obtained (existence, termination), and is the result independent of the order of applying rules (uniqueness, confluence)?

We present one of the core-methods of the CSI confluence tool, based on tiling the plane with so-called decreasing diagrams.
How to guarantee to do only needed work, i.e. how to avoid doing non-necessary or duplicate steps? This is usually resolved by
(sharing) graph rewriting. We present three basic operations involved, sharing, deletion, and boxing, and discuss the pitfalls
of implementing these lazily.