Abstracts.2021.Reduction

Reduction-based Normalization

by Nachiappan Valliappan

Abstract

Normalization is typically achieved for terms in a language by reducing them in accordance with a set of rewrite rules. What is reduction? What is a rewrite rule? How does one implement a normalizer using reduction? Why would anybody implement a normalizer (let alone using reduction)? The goal of this session is to answer these questions, and provide a recap on reduction-based normalization (*) and basic concepts in term rewriting. We will use a language for simple arithmetic expressions as the object of study and implement a normalizer for it in Agda.

(*) Often simply called "normalization". The emphasis "reduction-based" goes to highlight the difference from the so-called "reduction-free" technique Normalization-by-Evaluation.

Material

• Code from talk

Exercises

1. Prove Newman's diamond lemma: Any locally confluent well-founded relation is confluent.
2. Give an example of a locally confluent relation that is not confluent.
3. Prove that a relation is confluent if and only if it satisfies the Church-Rosser property, which says that two terms t and u reduce to the same term (t ↓ u) if and only if they are connected by a zigzag of reduction steps (t ⃰↔ u).
4. Prove that a weakly normalizing and confluent relation need not be terminating.
5. Prove that being well-founded/terminating/strongly normalizing/noetherian and accessibility are equivalent properties.
6. Consider the arithmetic axioms (x + y) + z = x + (y + z), 0 + x = x, and s(x) + y = s(x + y). Prove the right unit law for numerals n ⩴ 0 | s(n) and, more generally, for closed arithmetic expressions. Give a countermodel for the general statement x + 0 = x.
7. Consider the group axioms (x + y) + z = x + (y + z), 0 + x = x, and −x + x = 0. Prove the right inverse and unit laws for group expressions.
8. Prove the normalization function for arithmetic expressions terminating.

Related Talks

• Carlos Tomé Cortiñas, Normalization-by-Evaluation by Example

References

• Franz Baader and Tobias Nipkow, Term Rewriting and All That (Chapters 1-3)
• Ronald Garcia, Reduction (or Contextual) Semantics

Bibliography

• Olivier Danvy, From Reduction-Based to Reduction-Free Normalization
• A. Jeremy J. Dick, An Introduction to Knuth-Bendix Completion
• Gérard P. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems