Abstracts.2021.NbE

Normalization-by-Evaluation by Example

by Carlos Tomé Cortiñas

Abstract

In this talk I will present the technique of Normalization by Evaluation through the somewhat simple example of normalization for the theory of free monoids. Below you can find a detailed outline of the talk.

1. Examples of normal forms:

   1. Multiplication on natural numbers with variables: x2^2 * (x3^1 * (x58^4 * (x102^1 * 57)))
   2. Disjunctive normal forms of classical propositional logic: (A ∧ B) ∨ ((¬A ∧ B) ∨ (¬A ∧ ¬B)) (full) or ¬A ∨ B (prime)
   3. Natural deduction for noncommutative multiplicative conjunction ⊗ of linear propositional logic
   4. Simply-typed lambda calculus/Natural deduction for intuitionistic propositional logic

2. The unityped theory of free monoids, i.e. the unityped theory of monoids with constants (but no additional equations)

3. Normal forms: either unit or a right-associated nonempty list of constants; alternatively: left-associative, or nonempty lists of constants ending with unit

4. Normalization by evaluation (Haskell)

   1. Observation: normal forms support/are closed under the monoid operations
   2. Interpretation of the syntax/language of monoids in an arbitrary monoid
   3. Putting things together: a normalization function for formal monoid expressions

Material

• Haskell code

Exercises

In a programming language of your choice, implement normalization by evaluation for:

1. Free monoids using difference lists
2. Free commutative monoids
3. Free monoids with variables
4. Simple arithmetic expressions with variables
5. Free Boolean algebras
   • Ayberk's extension suggestion: normalize up to equisatisfiability instead of (logical) equivalence
   • Andreas' extension suggestion: normalize to (acyclic directed) graphs that are not necessarily trees to allow for sharing of subterms

Template

In case it might be helpful, here's again the template that the talk followed: First of all pick

0. your choice of theory T (perhaps redo the one from the talk, or give one of the exercises a try)

then start with

1. the type class of models of T (given by sorts, operations and equations; note that the theories from the talk and the exercises actually talk about just a single sort *)
2. the data type of terms of T (generated by the operations)
3. the evaluation function eval of terms in a given a model

and continue with

4. your data type of normal forms (perhaps skip this step on the first attempt),
5. your model 𝒩,
6. your reification function reify of elements in 𝒩 to normal forms (or to arbitrary terms if step 4 was skipped on this attempt)
7. your normalization function norm = reify ∘ eval

before ending with

8. your proof of correctness, i.e. ∀ t, u. t =T u ⟺ norm(t) = norm(u) (perhaps skip this step on the first and second attempt, it was not presented in detail and should be split up into smaller steps)

Related Talks

• Nachiappan Valliappan, Reduction-based Normalization

Bibliography

1. Joachim Lambek. Deductive Systems and Categories I. Syntactic Calculus and Residuated Categories. Math. Syst. Theory 2(4), pp. 287-318, 1968.
2. Michael Hedberg. Normalising the Associative Law: An Experiment with Martin-Löf's Type Theory. Formal Aspects Comput. 3(3), pp. 218-252, 1991.
3. Ilya Beylin, Peter Dybjer. Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids. TYPES 1995, pp. 47-61, 1995.
4. Thorsten Altenkirch, Martin Hofmann, Thomas Streicher. Categorical Reconstruction of a Reduction Free Normalization Proof. Category Theory and Computer Science 1995, pp. 182-199, 1995.
5. Peter Dybjer. Normalization by Evaluation. Notes: Slides for a course at Midlands Graduate School in the Foundations of Computing Science (MGS) 2009, Leicester, UK.