7
$\begingroup$

It's been suggested in an answer to this question 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?

$\endgroup$
  • 1
    $\begingroup$ 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 $\endgroup$ – Jake Sep 8 at 16:44
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? Or perhaps it is similar to the erasure used in self-types paper? $\endgroup$ – Łukasz Lew Sep 25 at 4:10
  • 1
    $\begingroup$ @Ł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! $\endgroup$ – cody Sep 30 at 13:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.