PreprintCC BY 4.0arXiv
Normalization by Evaluation with Substitutions as Operations
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.
Related
- The Thue-Morse substitutions and self-similar groups and algebras
- Automaticity of structural defects in fixed points of block substitutions
- Polytopal substitutions and conformal dimension
- When Majority-Vote Fails: Sequence Reconstruction under Fixed-Weight Substitutions
- On the Ordering and Injectivity of Lagrange Constants Associated with Certain Substitutions
BibTeX
@misc{hu2026normalization,
title = {{Normalization by Evaluation with Substitutions as Operations}},
author = {Jason Z. S. Hu},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.21131},
eprint = {2610.21131},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.21131},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Normalization by Evaluation with Substitutions as Operations
AU - Jason Z. S. Hu
PY - 2026
DA - 2026/10/15
PB - arXiv
DO - 10.48550/arxiv.2610.21131
UR - https://arxiv.org/abs/2610.21131
AB - 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.
ER -