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

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.