<p>Since the CoC has dependent types and system <span class="math-container">$F$</span> does not, I'll assume you mean a function whose <em>types</em> is in system <span class="math-container">$F$</span>, but whose <em>definition</em> can only be written in CoC. Luckily in this case we can restrict to system <span class="math-container">$F_\omega$</span>, which can express the same non-dependent functions as CoC, by some erasure argument.</p>

<p>In general, a rule of thumb to construct such functions is to consider systems <span class="math-container">$F$</span> and <span class="math-container">$F_\omega$</span> as the language of realizers of theorems of 2-nd and higher-order arithmetic, respectively, and to prove a theorem of the form <span class="math-container">$\forall x, \exists y, P$</span> in one not provable in the other, which by extraction should be a function definable in one and not the other.</p>

<p>One such theorem is the proof of normalization of system <span class="math-container">$F$</span> itself, which is provable in higher-order arithmetic using the "standard" proof, and not in 2nd order arithmetic by a simple diagonalization argument (though it is instructive to see where the standard proof fails).</p>

<p>Extracting this gives a normalization function for encodings of system <span class="math-container">$F$</span> terms, definable in system <span class="math-container">$F_\omega$</span>, but not in system <span class="math-container">$F$</span>.</p>

<p>I've explained this a bit in a <a href="https://cstheory.stackexchange.com/a/30522/3984">related answer</a>.</p>

CC BY-SA 4.0
2019-09-25T04:10:03.067Z
Hey cody, thanks for your answer. Would you be able to elaborate on erasure argument? Is it somehow related to what Philip Wadler calls [Girard-Reynolds isomorphism](https://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf)? Or perhaps it is similar to the erasure used in [self-types paper](https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf)?
Łukasz Lew
CC BY-SA 4.0
2019-09-30T13:08:59.110Z
@ŁukaszLew Definitely similar to the Wadler paper! But in general, there is a simple function that erases all the dependencies from CoC, targeting $F_\omega$, which is explained in e.g. Barendregt's Lambda Calculi with Types. It preserves normalization, and *reflects* it!
cody
CC BY-SA 4.0
2019-09-10T05:20:26.660Z
2019-09-10T05:20:26.660Z
cody
<p>It's been suggested in an answer to <a href="https://cstheory.stackexchange.com/questions/36054/how-do-you-get-the-calculus-of-constructions-from-the-other-points-in-the-lambda">this question</a> that the Calculus of Constructions has more computational strength than System-F. What are examples of functions that you express in CoC that you cannot write in System-F?</p>

CC BY-SA 4.0
2019-09-08T16:44:00.723Z
Hmm that's tricky. The Ackerman function should be definable in both which hints we'll need an extremely fast growing function to distinguish them. Perhaps another avenue to explore is using something like a power tree as an inductive type. Large elimination would be the only hope for system-F omega
Jake
<type-systems><calculus-of-constructions>
Example of a function that you can write in Calculus of Constructions but not in System-F
Labbekak
# Example of a function that you can write in Calculus of Constructions but not in System-F

(Asked by: username_0 on 2019-09-07)

It's been suggested in an answer to [this question](https://cstheory.stackexchange.com/questions/36054/how-do-you-get-the-calculus-of-constructions-from-the-other-points-in-the-lambda) that the Calculus of Constructions has more computational strength than System-F. What are examples of functions that you express in CoC that you cannot write in System-F?

**Tags:** type-systems, calculus-of-constructions

> **Comments:**
> **username_1**: Hmm that's tricky. The Ackerman function should be definable in both which hints we'll need an extremely fast growing function to distinguish them. Perhaps another avenue to explore is using something like a power tree as an inductive type. Large elimination would be the only hope for system-F omega  

---

## 1 answers

### Answer by username_2 on 2019-09-10. Score: 7 | Accepted answer

Since the CoC has dependent types and system $F$ does not, I'll assume you mean a function whose *types* is in system $F$, but whose *definition* can only be written in CoC. Luckily in this case we can restrict to system $F\_\omega$, which can express the same non-dependent functions as CoC, by some erasure argument.

In general, a rule of thumb to construct such functions is to consider systems $F$ and $F\_\omega$ as the language of realizers of theorems of 2-nd and higher-order arithmetic, respectively, and to prove a theorem of the form $\forall x, \exists y, P$ in one not provable in the other, which by extraction should be a function definable in one and not the other.

One such theorem is the proof of normalization of system $F$ itself, which is provable in higher-order arithmetic using the "standard" proof, and not in 2nd order arithmetic by a simple diagonalization argument (though it is instructive to see where the standard proof fails).

Extracting this gives a normalization function for encodings of system $F$ terms, definable in system $F\_\omega$, but not in system $F$.

I've explained this a bit in a [related answer](https://cstheory.stackexchange.com/a/30522/3984).

> **Comments:**
> **username_3**: Hey username_2, thanks for your answer. Would you be able to elaborate on erasure argument? Is it somehow related to what Philip Wadler calls [Girard-Reynolds isomorphism](https://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf)? Or perhaps it is similar to the erasure used in [self-types paper](https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf)?  
> **username_2**: @ŁukaszLew Definitely similar to the Wadler paper! But in general, there is a simple function that erases all the dependencies from CoC, targeting $F_\omega$, which is explained in e.g. Barendregt's Lambda Calculi with Types. It preserves normalization, and *reflects* it!  

---

