patternMinor
Why is the type ∀t.t un-inhabited in System F?
Viewed 0 times
whythesysteminhabitedtype
Problem
How do you prove that there exists no term with the type $\forall t. t$ in System F?
I tried searching through Pierce's TAPL and Reynold's ToPL, but could not find anything. I suspect that the proof may involve some kind of model theoritic argument, but I fail to see where to start.
I tried searching through Pierce's TAPL and Reynold's ToPL, but could not find anything. I suspect that the proof may involve some kind of model theoritic argument, but I fail to see where to start.
Solution
The simplest proof is giving a model where types are interpreted as propositions, and terms as proofs, then observing that $\forall \alpha.\alpha$ is interpreted as the false proposition, so any $\cdot \vdash t : \forall \alpha.\alpha$ would be a proof of falsehood. It is important to remember that $\forall \alpha.\alpha$ is only uninhabited for sure in the empty context $\cdot$, in other contexts it may be trivially inhabited.
Concretely, first interpret each $A$ type with $n$ free type variables in the following way:
$$
\begin{alignat*}{2}
& [\![ A ]\!] && : \mathsf{Bool}^n \to \mathsf{Bool}\\
& [\![ \alpha ]\!]\,\gamma && := \text{$\alpha$-th component of $\gamma$}\\
& [\![ A \to B ]\!]\,\gamma && := [\![ A ]\!]\,\gamma \Rightarrow [\![ B ]\!]\,\gamma\\
& [\![ \forall \alpha.\,B]\!]\,\gamma && := [\![B]\!]\,(\mathsf{true},\,\gamma)\,\land\,[\![B]\!]\,(\mathsf{false},\,\gamma)
\end{alignat*}
$$
Interpret every typing context $\Gamma$ with $n$ free type variables as:
$$
\begin{alignat*}{2}
& [\![\Gamma]\!] : \mathsf{Bool}^n\to \mathsf{Bool}\\
& [\![\Gamma]\!]\,\gamma := \bigwedge\limits_{A\,\in\,\Gamma}\,[\![A]\!]\,\gamma
\end{alignat*}
$$
Then show for each $\Gamma \vdash t : A$ term, that for each truth valuation $\gamma : \mathsf{Bool}^n$, if $[\![\Gamma]\!]\,\gamma = \mathsf{true}$, then $[\![A]\!]\,\gamma = \mathsf{true}$. This can be done by induction on terms.
Now, $[\![\forall \alpha.\alpha]\!]$ with no free type variables evaluates to $\mathsf{false}$, since it's $\mathsf{true}$ when $\alpha$ is instantiated to $\mathsf{true}$, and $\mathsf{false}$ when it's instantiated to $\mathsf{false}$, and the conjunction of these is $\mathsf{false}$. Assuming $\cdot\vdash t : \forall \alpha.\alpha$, we have by the previous result that $[\![\forall \alpha.\alpha]\!]$ is $\mathsf{true}$, a contradiction, hence there is no $\cdot\vdash t : \forall \alpha.\alpha$.
Concretely, first interpret each $A$ type with $n$ free type variables in the following way:
$$
\begin{alignat*}{2}
& [\![ A ]\!] && : \mathsf{Bool}^n \to \mathsf{Bool}\\
& [\![ \alpha ]\!]\,\gamma && := \text{$\alpha$-th component of $\gamma$}\\
& [\![ A \to B ]\!]\,\gamma && := [\![ A ]\!]\,\gamma \Rightarrow [\![ B ]\!]\,\gamma\\
& [\![ \forall \alpha.\,B]\!]\,\gamma && := [\![B]\!]\,(\mathsf{true},\,\gamma)\,\land\,[\![B]\!]\,(\mathsf{false},\,\gamma)
\end{alignat*}
$$
Interpret every typing context $\Gamma$ with $n$ free type variables as:
$$
\begin{alignat*}{2}
& [\![\Gamma]\!] : \mathsf{Bool}^n\to \mathsf{Bool}\\
& [\![\Gamma]\!]\,\gamma := \bigwedge\limits_{A\,\in\,\Gamma}\,[\![A]\!]\,\gamma
\end{alignat*}
$$
Then show for each $\Gamma \vdash t : A$ term, that for each truth valuation $\gamma : \mathsf{Bool}^n$, if $[\![\Gamma]\!]\,\gamma = \mathsf{true}$, then $[\![A]\!]\,\gamma = \mathsf{true}$. This can be done by induction on terms.
Now, $[\![\forall \alpha.\alpha]\!]$ with no free type variables evaluates to $\mathsf{false}$, since it's $\mathsf{true}$ when $\alpha$ is instantiated to $\mathsf{true}$, and $\mathsf{false}$ when it's instantiated to $\mathsf{false}$, and the conjunction of these is $\mathsf{false}$. Assuming $\cdot\vdash t : \forall \alpha.\alpha$, we have by the previous result that $[\![\forall \alpha.\alpha]\!]$ is $\mathsf{true}$, a contradiction, hence there is no $\cdot\vdash t : \forall \alpha.\alpha$.
Context
StackExchange Computer Science Q#119775, answer score: 4
Revisions (0)
No revisions yet.