<blockquote>
<p>May I have a reference to why η expansion is invalid for CoC?</p>
</blockquote>
<p>It's not invalid. It's up to choice whether <span class="math-container">$\eta$</span>-conversion for functions (or other types) is included. The original <a href="https://reader.elsevier.com/reader/sd/pii/0890540188900053?token=199BB4913E9DBEA3C6C67646A097CDE608C670A4BB62D715D8BAA8DE24C8A2492245016592C1C26A1F5EA2BB16CDC00C&amp;originRegion=eu-west-1&amp;originCreation=20210516090826" rel="noreferrer">CoC paper</a> seems to omit it, but as you see ATAPL includes it. I'm not certain, but <span class="math-container">$\eta$</span> may have been omitted from the original source because it was difficult to handle in the strong normalization arguments, back in the days. Nowadays normalization proofs are more likely to be based on NbE themselves, and have <a href="https://arxiv.org/abs/1810.09367" rel="noreferrer">no issues</a> with <span class="math-container">$\eta$</span>-rules. Modern Coq definitely has <span class="math-container">$\eta$</span> for functions, and it is generally considered a highly useful basic feature.</p>
<blockquote>
<p>The rules QA-NABS-1, QA-NABS-2 seem to be implementing η expansion for stuck terms? Why do these rules not describe NBE?</p>
</blockquote>
<p>They do specify <span class="math-container">$\eta$</span> for functions. It's not really NbE though. ATAPL only describes how to compare weak head normal forms for conversion in an iterated fashion, it does not say how to efficiently compute to whnf. The essential part of NbE is the separation of syntax and values; this is missing from the ATAPL exposition.</p>
<blockquote>
<p>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</p>
</blockquote>
<p>This is incorrect. NbE is not necessarily type-directed, and does not necessarily include <span class="math-container">$\eta$</span>-expansion. If you look at <code>QA-NABS-1</code>, <code>QA-NABS-2</code> and the other rules in ATAPL, they can be adapted to a conversion checking algorithm on NbE values, which is a) purely syntax-directed b) does not require <span class="math-container">$\eta$</span>-expansion in evaluation c) decides <span class="math-container">$\eta$</span>-conversion for functions.</p>
<blockquote>
<p>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.</p>
</blockquote>
<p>I'm not aware of any rigorous and generic way for specifying conversion checking algorithms. I would summarize the rules of thumbs as follows.</p>
<p>The specification of values is obtained from the specification of syntax by replacing binders with metalanguage functions or closures. Evaluation goes from syntax to values and performs <span class="math-container">$\beta$</span>-reduction (but not necessarily <span class="math-container">$\eta$</span>-conversions). Then, conversion checking can be implemented on values, proceeding purely structurally, except where we want syntax-directed <span class="math-container">$\eta$</span>-checking in the manner specified in ATAPL.</p>

CC BY-SA 4.0
2021-05-16T09:43:13.247Z
2021-05-16T10:59:18.280Z
2021-05-16T10:59:18.280Z
András Kovács
<p>I have a shorter answer: normalization is usually used in conversion check of terms (aka definitional equality), and CoC has untyped conversion check.
In conversion check, we normalize terms and compare 'em syntactically (think of it as comparing the ASTs). This probably means the normalization process doesn't have access to the types of terms, so it may not be able to expand the terms into eta-long normal forms.</p>
<p>OTOH, the intuitionistic type theory by Martin Lof has typed conversion check. IMO this is also the reason why homotopy type theory chose intuitionistic type theory as the type theory framework it uses.</p>

CC BY-SA 4.0
2021-05-17T00:06:06.493Z
2021-05-17T00:18:09.353Z
2021-05-17T00:18:09.353Z
ice1000
<p>I am studying <a href="http://davidchristiansen.dk/tutorials/nbe/#%28part._.Other_.Approaches%29" rel="nofollow noreferrer">David Christiansen's tutorial on implementing a dependently typed language</a>, where it says:</p>
<blockquote>
<p>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 <strong>η-expansion is not valid for some theories (including Coq’s Calculus of Constructions)</strong></p>
</blockquote>
<ol>
<li>May I have a reference to why <code>η</code> expansion is invalid for CoC? Is there some &quot;moral&quot; by which one can see the rules of CoC and realise that <code>η</code> expansion is invalid?</li>
<li>The rules for implementing CoC in <a href="https://www.cis.upenn.edu/%7Ebcpierce/attapl/" rel="nofollow noreferrer">ATAPL Chapter 2</a> look to my naive eye like NBE (Normalization by Evaluation). The rules for CoC are given as an extension to the equivalence rules of <code>LF</code>, augmented with extra rules that govern how <code>Prf</code> (the encoding mechanism of <code>Pi</code> types) and <code>Prop</code> interact. The rules <code>QA-NABS-1, QA-NABS-2</code> seem to be implementing <code>η</code> expansion for stuck terms? Why do these rules <em>not</em> describe NBE?</li>
<li>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 <em>framework</em> 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)</li>
</ol>
<p>I have included the rules for CoC as given in ATAPL, Chapter 2, for reference:</p>
<p><a href="https://i.sstatic.net/0ZYOs.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/0ZYOs.png" alt="enter image description here" /></a>
<a href="https://i.sstatic.net/cULJa.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/cULJa.png" alt="enter image description here" /></a></p>

<type-theory><dependent-type><calculus-of-constructions><normalization>
What technique is used to implement type checking for CoC?
Siddharth Bhat
# What technique is used to implement type checking for CoC?

(Asked by: username_0 on 2021-05-16)

I am studying [David Christiansen's tutorial on implementing a dependently typed language](http://davidchristiansen.dk/tutorials/nbe/#%28part._.Other_.Approaches%29), 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)**

1. 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?
2. The rules for implementing CoC in [ATAPL Chapter 2](https://www.cis.upenn.edu/%7Ebcpierce/attapl/) 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 `Pi` types) and `Prop` interact. The rules `QA-NABS-1, QA-NABS-2` seem to be implementing `η` expansion for stuck terms? Why do these rules *not* describe NBE?
3. 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:

[![enter image description here](https://i.sstatic.net/0ZYOs.png)](https://i.sstatic.net/0ZYOs.png)
[![enter image description here](https://i.sstatic.net/cULJa.png)](https://i.sstatic.net/cULJa.png)

**Tags:** type-theory, dependent-type, calculus-of-constructions, normalization

---

## 2 answers

### Answer by username_1 on 2021-05-16. Score: 6 | Accepted answer

> May I have a reference to why η expansion is invalid for CoC?

It's not invalid. It's up to choice whether $\eta$-conversion for functions (or other types) is included. The original [CoC paper](https://reader.elsevier.com/reader/sd/pii/0890540188900053?token=199BB4913E9DBEA3C6C67646A097CDE608C670A4BB62D715D8BAA8DE24C8A2492245016592C1C26A1F5EA2BB16CDC00C&originRegion=eu-west-1&originCreation=20210516090826) seems to omit it, but as you see ATAPL includes it. I'm not certain, but $\eta$ may have been omitted from the original source because it was difficult to handle in the strong normalization arguments, back in the days. Nowadays normalization proofs are more likely to be based on NbE themselves, and have [no issues](https://arxiv.org/abs/1810.09367) with $\eta$-rules. Modern Coq definitely has $\eta$ for functions, and it is generally considered a highly useful basic feature.

> The rules QA-NABS-1, QA-NABS-2 seem to be implementing η expansion for stuck terms? Why do these rules not describe NBE?

They do specify $\eta$ for functions. It's not really NbE though. ATAPL only describes how to compare weak head normal forms for conversion in an iterated fashion, it does not say how to efficiently compute to whnf. The essential part of NbE is the separation of syntax and values; this is missing from the ATAPL exposition.

> 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

This is incorrect. NbE is not necessarily type-directed, and does not necessarily include $\eta$-expansion. If you look at `QA-NABS-1`, `QA-NABS-2` and the other rules in ATAPL, they can be adapted to a conversion checking algorithm on NbE values, which is a) purely syntax-directed b) does not require $\eta$-expansion in evaluation c) decides $\eta$-conversion for functions.

> 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'm not aware of any rigorous and generic way for specifying conversion checking algorithms. I would summarize the rules of thumbs as follows.

The specification of values is obtained from the specification of syntax by replacing binders with metalanguage functions or closures. Evaluation goes from syntax to values and performs $\beta$-reduction (but not necessarily $\eta$-conversions). Then, conversion checking can be implemented on values, proceeding purely structurally, except where we want syntax-directed $\eta$-checking in the manner specified in ATAPL.


---

### Answer by username_2 on 2021-05-17. Score: 1

I have a shorter answer: normalization is usually used in conversion check of terms (aka definitional equality), and CoC has untyped conversion check.
In conversion check, we normalize terms and compare 'em syntactically (think of it as comparing the ASTs). This probably means the normalization process doesn't have access to the types of terms, so it may not be able to expand the terms into eta-long normal forms.

OTOH, the intuitionistic type theory by Martin Lof has typed conversion check. IMO this is also the reason why homotopy type theory chose intuitionistic type theory as the type theory framework it uses.


---

