Quantitative and Metric Rewriting: Abstract and Linear Systems
Rewriting theory is the discipline that studies the computational (and operational) content of notions of equality and equality-preserving symbolic manipulations. As such, rewriting plays a crucial role in the study of programming languages, both for what concerns their semantic theory and their implementation. Recent advances in theoretical computer science, however, have questioned the central role played by equality in semantics, arguing for more quantitative and approximated forms of equivalence. Prompted by that, several theories of semantic equality have been refined giving rise to quantitative theories of semantic differences, prime examples being general theories of program and system distances and the theory of quantitative algebras and quantitative equational reasoning. All these theories, however, focus on quantitative notions of equality (i.e. distances) at a definitional (oftentimes even denotational) level, mostly ignoring their operational and computational content. This is unfortunate, as understanding the operational content of notions of differences and distances is of paramount importance to developing a general quantitative theory of programming language semantics. In this talk, we will introduce the theory of quantitative and metric rewriting systems as a first step towards a general theory of the computational content of quantitative symbolic manipulations. We will introduce notions of quantitative abstract and term rewriting systems, as well as their general theory. In particular, we will present quantitative notions of confluence and termination, showing how the latter play a central role in the solution of what we shall call metric word problems, the latter being refinements of the well-known word problem to a quantitative setting. We will show quantitative and metric refinements of cornerstone results in the theory of rewriting systems, such as the Newman, Hindley-Rosen, and Critical Pair Lemma, as well as their applications to nontrivial examples of quantitative systems. The talk will be example-driven, with a special focus on quantitative systems coming from the field of algorithms (notably edit distances on strings), quantitative algebras and algebraic effects (e.g. quantitative barycentric algebras), programming language theory (quantitative combinatory logic), and combinations thereof.