Elements of Quantitative Rewriting

on YouTube ↗22m

" summary

Defines rewriting over quantales and proves metric versions of Newman and Church‑Rosser plus critical‑pair lemmas, with concrete counterexamples showing duplication can double distances so naive lifting loses confluence. Introduces non‑expansive linear term rewriting systems (confluent) and graded term rewriting systems that attach sensitivity functions to symbols to control error amplification, and demonstrates modeling of string distances like Hamming and Levenshtein, plus applications to quantitative algebraic effects.

AI-written summary · about

" chapters (12)

1. 0:00Introduction
2. 1:25Equality to rewriting in PL
3. 2:29Limitations of equality
4. 4:34Extending rewriting to quantity
5. 5:58Quantitative rewriting theory
6. 7:21Quantitative confluence
7. 11:55Proving confluence
8. 14:45Naive distance propagation
9. 16:52Recovering confluence in linear
10. 17:55Graded refinements
11. 20:04Results and applications
12. 20:50Future directions