I realized that the idea of the previous post of factoring normalization as a translation to and from a syntactic model of normal forms is explored very nicely in a JFP article by Altenkirch and Chapman, indeed with a concrete environment semantics, albeit without a connection to focusing:
Thorsten Altenkirch and James Chapman
Traditionally, decidability of conversion for typed λ-calculi is established by showing that small-step reduction is conﬂuent and strongly normalising. Here we investigate an alternative approach employing a recursively defined normalisation function which we show to be terminating and which reﬂects and preserves conversion. We apply our approach to the simply-typed λ-calculus with explicit substitutions and βη-equality, a system which is not strongly normalising. We also show how the construction can be extended to System T with the usual β-rules for the recursion combinator. Our approach is practical, since it does verify an actual implementation of normalisation which, unlike normalisation by evaluation, is ﬁrst order. An important feature of our approach is that we are using logical relations to establish equational soundness (identity of normal forms reﬂects the equational theory), instead of the usual syntactic reasoning using the Church-Rosser property of a term rewriting system.
Attachment ambiguity of the week
4 hours ago