-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2021.Reduction
by Nachiappan Valliappan
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.
- Code from talk
- Prove Newman's diamond lemma: Any locally confluent well-founded relation is confluent.
- Franz Baader and Tobias Nipkow, Term Rewriting and All That (Chapters 1-3)
- Ronald Garcia, Reduction (or Contextual) Semantics
- 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