In system F, is every closed term $M$, which is of $\forall \alpha . \left( \alpha \rightarrow \alpha \right)$, $\alpha \beta \eta$-equivalent to $\Lambda \alpha. \lambda x^{\alpha} . x$?

I have believed that this is true and have tried to prove it by using the equation

$\forall \alpha. \forall \beta. \forall f^{\alpha \rightarrow \beta} . \forall x^{\alpha} . M \beta \left( f x \right) = f \left( M \alpha x \right)$

, which I think is a consequence of theorems for Free, but couldn't prove it.

Thanks to read my question.

  • 1
    $\begingroup$ Yes, you are on the right track. It does have a proof using theorems for Free or logical relations/parametricity. Try building the appropriate relation. Amal Ahmed’s lectures in OPLSS does a good job of explaining the setup. $\endgroup$ – Apoorv Feb 14 at 4:24
  • $\begingroup$ Let $y : \beta$ be arbitrary, and replace $f$ with $\lambda z^{\alpha} . y$. Then $M \beta y = y$. $\endgroup$ – KiJeong Lim Feb 15 at 4:30

Your Answer

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

Browse other questions tagged or ask your own question.