I am studying David Christiansen's tutorial on implementing a dependently typed language, where it says:
Typed normalization by evaluation is far from the only way to implement conversion checking for dependent types. Indeed, normalization by evaluation has a number of characteristics that make it only suitable for certain theories: it η-expands expressions as many times as possible, but η-expansion is not valid for some theories (including Coq’s Calculus of Constructions)
- May I have a reference to why
ηexpansion is invalid for CoC? Is there some "moral" by which one can see the rules of CoC and realise that
ηexpansion is invalid?
- The rules for implementing CoC in ATAPL Chapter 2 look to my naive eye like NBE (Normalization by Evaluation). The rules for CoC are given as an extension to the equivalence rules of
LF, augmented with extra rules that govern how
Prf(the encoding mechanism of
Propinteract. The rules
QA-NABS-1, QA-NABS-2seem to be implementing
ηexpansion for stuck terms? Why do these rules not describe NBE?
- Is there a name for the rules given in ATAPL to implement type checking for CoC? They seem ad-hoc to me, and I don't understand how I would come up with them. I would appreciate a reference to the framework that is used to create the reduction rules for CoC (for clarity, by a framework, I refer to ideas such as NBE or hereditary substitution)
I have included the rules for CoC as given in ATAPL, Chapter 2, for reference: