Abstracts.2021.NbE

Normalization-by-Evaluation by Example

by Carlos Tomé Cortiñas

Abstract

1. Examples of normal forms:

   1. Multiplication on natural numbers with variables: x2 * (x3 * (x58 * (x102 * 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 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

Exercises

1. NbE for free monoids using difference lists
2. Free commutative monoids
3. Free monoids with variables
4. (TBD)

Resources

(TBA)

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.