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))
   3. Simply-typed lambda calculus/Natural deduction of intuitionistic propositional logic

2. Unityped theory of free monoids, i.e. theory of monoids with constants

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

4. Normalization by Evaluation (Haskell)

   1. Observation: normal forms support the monoid operations.
   2. Interpretation of the syntax of monoids
   3. Putting things together: normalization function

Resources

(TBA)

Bibliography

(TBA)