Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Completeness proof for a polymorphic lambda calculus

Alejandro Díaz-Caro (Feb 10 2025 at 16:05):

I am trying to reproduce a completeness proof for System F with respect to a categorical model. (Well, I am actually doing just an “adequacy” proof since I do not have eta-rules, so it will not be complete).

The idea is to prove that whenever $\llbracket\Gamma \vdash t:A\rrbracket= \llbracket\Gamma \vdash r:A\rrbracket$, then $t$ and $r$ are computationally equivalent (meaning that they behave the same in any context). In a proof for simply typed lambda calculus, I would do this by induction on $A$. However, with a universal quantification, I quickly run into problems in the polymorphic case when the type is $\forall X.A$. Indeed, using progress, subject reduction, and soundness, I can conclude that since $\llbracket\Gamma \vdash t:\forall X.A\rrbracket= \llbracket\Gamma \vdash r:\forall X.A\rrbracket$ we have $\llbracketΓ \vdash \Lambda X.t_0:\forall X.A\rrbracket= \llbracket\Gamma\vdash\Lambda X. r_0:\forall X.A\rrbracket$ and thus, $\llbracket\Gamma\vdash t_0:A\rrbracket= \llbracket\Gamma\vdash r_0:A\rrbracket$.

From this, by the induction hypothesis, I conclude that $t_0$ is computationally equivalent to $r_0$. Now, to prove that $\Lambda X.t_0$ is computationally equivalent to $\Lambda X.r_0$ I need to "test it" in any contexts, so I use a substitution lemma to deduce that for any $B$, $\llbracket\Gamma\vdash t_0[B/X]:A[B/X]\rrbracket= \llbracket\Gamma\vdash r_0[B/X]:A[B/X]\rrbracket$.

This is where, of course, I get stuck since I cannot use the induction hypothesis to conclude $t_0[B/X]$ computationally equivalent to $r_0[B/X]$ because $A[B/X]$ may be larger than $A$.

I do not know how to apply the standard solution introduced by Girard to prove the strong normalization of System F, which consisted of, instead of using the problematic $\llbracket A[B/X]\rrbracket$ to define the interpretation of types, using a substitution $\theta$ and parameterizing the interpretations with it, using $\llbracket A\rrbracket_{\theta,X\mapsto\llbracket B\rrbracket_\theta}$.

He solved the problem of the inductive definition of types not being well-founded, and I want to solve the problem of the induction hypothesis not being applicable in my case.

Can somebody point me in the right direction suggesting me where to look? I could not find any proof of completeness or adequacy for System F that explicitly explains how to circumvent this problem.

Ryan Wisnesky (Feb 10 2025 at 16:15):

every proof I've seen of anything nontrivial about system F involved using a "logical relations argument": https://cs.au.dk/~birke/papers/AnIntroductionToLogicalRelations.pdf to circumvent some problem with a substitution making a term too big to apply the inductive hypothesis to.

Alejandro Díaz-Caro (Feb 10 2025 at 16:23):

Thanks. As far as I can see, that document describes in great detail the solution à la Girard that I mentioned in my post, but the problem remains of how to adapt it to an adequacy proof, where the issue is not the well-foundedness of the definition but the applicability of the induction hypothesis.

In any case, thanks for the link! I will read it in detail to see if I can get some insights from there.