Normalization by evaluation with simpler substitution operations improves proofs
Normalization by Evaluation with Substitutions as Operations
Programming Languages
Summary
Normalization by evaluation (NbE) is a technique used in computer science to simplify expressions in programming languages. The authors studied how using substitutions as operations, instead of explicit substitutions, affects NbE. They found that this approach makes some parts of the proof easier, like showing that the method is sound, but it complicates proving that NbE is complete. Their work helps clarify the trade-offs involved in designing NbE methods.
What this means in practice
- •For functional programming language developers: Use substitution operations to simplify soundness proofs of normalization in language implementations.
- •For compiler engineers: Improve compiler correctness by adopting substitution-as-operations techniques in normalization routines.
A theory result. No direct application yet.
Authors
Jason Z. S. Hu
Abstract
In previous works on normalization by evaluation (NbE) with an untyped domain model, explicit substitutions are a major decision choice, which, in retrospect, is taken to simplify subsequent semantic proofs. This choice hence is taken for a purely technical reason. In addition, there is no obvious lemma to test the completeness of the definition or the laws for explicit substitutions. In this technical report, we investigate NbE in a typical setting, i.e. defining substitutions as operations. We show that this setting brings simplifications in proving syntactic properties and soundness of NbE, though complications are introduced in the completeness proof of NbE.