Author: Mike Shulman Format: MarkdownItexCreated page, mainly to record my understanding of the issue involving strong normalization, or lack thereof, for explicit substitutions.
<a href="https://ncatlab.org/nlab/revision/explicit+substitution/1">v1</a>, <a href="https://ncatlab.org/nlab/show/explicit+substitution">current</a>
Created page, mainly to record my understanding of the issue involving strong normalization, or lack thereof, for explicit substitutions.
Author: Mike Shulman Format: MarkdownItexAdded some discussion about the linear substitution calculus, mostly quoted from Damiano Mazza on zulip.
<a href="https://ncatlab.org/nlab/revision/diff/explicit+substitution/5">diff</a>, <a href="https://ncatlab.org/nlab/revision/explicit+substitution/5">v5</a>, <a href="https://ncatlab.org/nlab/show/explicit+substitution">current</a>
Added some discussion about the linear substitution calculus, mostly quoted from Damiano Mazza on zulip.