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

NbE for:

1. Free monoids using difference lists
2. Free commutative monoids
3. Free monoids with variables
4. Arithmetic expressions with variables

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.