14
$\begingroup$

Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in terms of all typed relations. In an impredicative system (like CiC/Coq) that's fine, but it seems to be impossible in a predicative system (like Agda).

How can this be done? For example, how would you prove normalization for System F in Agda? Do you have to build your own impredicative universe?

$\endgroup$
14
$\begingroup$

In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent types as a ($n$-ary) relation $R \subseteq \cal A^n$.

This works perfectly fine for all kinds of type theories, including dependently typed theories, see e.g. Shürmann and Sarnat: Structural Logical Relations where a predicative logic (that of Twelf) is used to prove a certain property (decidability of equality) for a predicative calculus (simply typed $\lambda$-calculus) using logical relations.

As you may have suspected, however, it is not possible to prove normalization of system F in Agda (if Agda isn't secretly stronger than expected, i.e. about the strength of Martin-Löf type theory with a bunch of universes). This is because normalization of system F implies consistency of 2nd order arithmetic ($\mathrm{PA}_2$) which is stronger than M-L type theory with any number of (predicative) universes.

It's instructive to work out exactly where the proof goes wrong in Agda, though. It indeed occurs when you try to define the logical relations interpretation of the impredicative quantification. The interpretation of the non-impredicative connectives though (including "dependent" quantification) is kosher in a theory like Agda.

$\endgroup$
  • 1
    $\begingroup$ Wow, really? You can't prove System F normalizes in Agda? Do you have a citation for that? $\endgroup$ – Max New Oct 20 '15 at 18:09
  • 2
    $\begingroup$ @MaxNew: This is actually quite difficult to find a citation for. The closest I can find is The Strength of Some Martin-Löf Type Theories which definitely settles the question for a predicative theory with a single universe and some kind of induction. But Agda has the terrifying induction recursion which makes it vastly more powerful. $\endgroup$ – cody Oct 20 '15 at 19:41
  • 1
    $\begingroup$ I should add though, that induction recursion is known to be weaker than impredicative quantification in certain cases, as is nicely explained here: fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html $\endgroup$ – cody Oct 22 '15 at 14:49
  • 1
    $\begingroup$ @cody Unfortunately, the link does not work any more. Are you able to find this content again? Are you aware of new publications in the area of formalizing impredicativity? $\endgroup$ – Łukasz Lew Jun 8 '18 at 4: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.