<p>I thought this might be tough, given the fact that the proof usually goes in the other direction (Parametricity <span class="math-container">$\Rightarrow$</span> Normalization), and the post by Gabriel is somewhat involved, but in system F one can do a relatively straightforward induction.</p>

<p>I'm going to assume you're somewhat familiar with the usual statement of parametricty, e.g. from the "Theorems for free!" paper, and I'll treat only binary relations for simplicity.</p>

<p>I'll also be working in the "Curry-style" calculus for brevity.</p>

<blockquote>
  <p>Theorem: if <span class="math-container">$T(X)$</span> is a type in system F with (only) the free type variable <span class="math-container">$X$</span>, then for any well-typed term
  <span class="math-container">$$ \vdash t : \forall X.T(X)$$</span>
  and any relation <span class="math-container">$\cal R$</span> between terms that respects <span class="math-container">$\beta\eta$</span>,
  <span class="math-container">$$ t\ T({\cal R})\ t$$</span>
  where <span class="math-container">$T(\cal R)$</span> is the parametricity relation defined in the usual way by induction on the structure of types.</p>
</blockquote>

<p>The proof requires a more general lemma, which will handle arbitrary amounts of type variables and term variables (rather than working in a closed context).</p>

<p>Let <span class="math-container">$\theta$</span> be a map from type variables to <span class="math-container">$\beta\eta$</span> respecting binary relations over terms, and if <span class="math-container">$\Gamma$</span> is a type context, then <span class="math-container">$\sigma$</span> is a map from variables <span class="math-container">$x$</span> to pairs of terms <span class="math-container">$(u_1, u_2)$</span> such that, if <span class="math-container">$x : U\in\Gamma$</span>, then <span class="math-container">$u_1\ U\theta\ u_2$</span>, i.e. <span class="math-container">$u_1$</span> and <span class="math-container">$u_2$</span> are related by the parametricity relation at the appropriate type (where <span class="math-container">$\theta$</span> is used to instantiate type variables).</p>

<p>Given this, the lemma then states:</p>

<blockquote>
  <p>Lemma: for any such <span class="math-container">$\theta, \Gamma, \sigma$</span>, if <span class="math-container">$\Gamma \vdash t : T$</span>, then <span class="math-container">$t\sigma_1\ T\theta\ t\sigma_2$</span>. (With the obvious interpretation of <span class="math-container">$\sigma_i$</span> as a plain substitution).</p>
</blockquote>

<p><strong>Proof</strong>. First we note that <span class="math-container">$T\theta$</span> is closed under <span class="math-container">$\beta\eta$</span> conversion, so we may take the <strong><span class="math-container">$\beta$</span>-normal <span class="math-container">$\eta$</span>-long normal form of <span class="math-container">$t$</span></strong>, and reason by induction on its <strong>size</strong>.</p>

<p>Now we reason by <strong>cases</strong> (not induction!) on the structure of <span class="math-container">$T$</span>.</p>

<p>Base case: suppose <span class="math-container">$T=X$</span>. The normal form of <span class="math-container">$t$</span> is also of type <span class="math-container">$X$</span> and the only possible form is <span class="math-container">$x\ t_1\ldots t_n$</span>, with the <span class="math-container">$t_i$</span> in normal forms.</p>

<p>If t is just <span class="math-container">$x$</span>, then <span class="math-container">$\sigma_1(x)\ X\theta\ \sigma_2(x)$</span> by construction.</p>

<p>Otherwise, by inversion the type of <span class="math-container">$x$</span> is <span class="math-container">$T'=T_1\rightarrow\ldots\rightarrow T_n\rightarrow X$</span>. Now by construction, <span class="math-container">$\sigma_1(x)\ T'\theta\sigma_2(x)$</span>, which means that <span class="math-container">$\sigma_1(x\ t_1\ldots t_n)\ \theta(X)\ \sigma_2(x\ t_1\ldots t_n)$</span> if <span class="math-container">$\sigma_1(t_i)\ T_i\theta\ \sigma_2(t_i)$</span>. But this is exactly the induction hypothesis.</p>

<p>Suppose now that <span class="math-container">$T=T_1\rightarrow T_2$</span>. We proceed similarly: take 2 arbitrary terms <span class="math-container">$u$</span> and <span class="math-container">$u'$</span> such that <span class="math-container">$u\ T_1\theta\ u'$</span>. We need to show that <span class="math-container">$t\sigma_1\ u\ T_2\theta\ t\sigma_2\ u'$</span>. But by inversion again, (and the definition of <span class="math-container">$\eta$</span>-long forms), <span class="math-container">$t$</span> must be of the form <span class="math-container">$\lambda x.t'$</span>, so <span class="math-container">$t'\sigma_1\ u\ =_{\beta\eta}\ t'\sigma_1'$</span>, where <span class="math-container">$\sigma_1'$</span> is <span class="math-container">$\sigma_1$</span> extended with the mapping <span class="math-container">$x\mapsto u$</span>, and similarly for <span class="math-container">$u'$</span>.</p>

<p>The induction hypothesis applies again, using <span class="math-container">$\sigma'$</span> instead of <span class="math-container">$\sigma$</span>.</p>

<p>Finally, if <span class="math-container">$T=\forall X.T'$</span>, then inversion tells us that <span class="math-container">$\Gamma\vdash t:T'$</span>, and <span class="math-container">$X$</span> does not appear free in <span class="math-container">$\Gamma$</span>. This means we can take <span class="math-container">$\theta'$</span> to be <span class="math-container">$\theta$</span> extended with an arbitrary binding for <span class="math-container">$X$</span>, which does not affect the correctness of <span class="math-container">$\sigma$</span>, since <span class="math-container">$X$</span> does not appear in the types of any of the variables.</p>

<p>This gives <span class="math-container">$t\sigma_1\ T'\theta'\ t\sigma_2$</span> for an arbitrary such extension, implying <span class="math-container">$t\sigma_1\ T\theta\ t\sigma_2$</span>, which concludes the proof.</p>

<hr>

<p>I'm not 100% certain, but I suspect this proof <em>can</em> be carried out in some weak form of 2nd order arithmetic, which would show that normalization does imply parametricity in some strong sense.</p>

CC BY-SA 4.0
2019-02-17T07:28:48.353Z
Cody, thank you for working that out, I appreciate that.
Łukasz Lew
CC BY-SA 4.0
2019-02-08T00:10:27.720Z
2019-02-08T00:10:27.720Z
cody
<p>I'd like to offer some pointers.</p>
<blockquote>
<p>Is there any research that goes along these lines and perhaps formalizes this intuition?</p>
</blockquote>
<p>Parametricity by analysis of the shape of (simply-typed) normal forms preceded by a normalisation argument was proposed by Girard, Scedrov, and Scott [1]. This connects parametricity, cut-elimination in logic, and a proof technique for coherence in category theory. Here, parametricity is understood as a property of dinaturality, originally proposed for system F in [2].</p>
<blockquote>
<p>Is this idea correct and strong enough to prove (by case analysis on the normal forms of the terms) 'free theorems' or more general parametricity results?</p>
</blockquote>
<p>In [1], it is noted that this includes the so-called &quot;free theorems&quot; as a special case. But the argument does not extend to all of system F, and dinaturality fails to capture relational parametricity (see e.g. [3]). On the other hand, a work by Paolo Pistone shows that one indeed obtains with a “syntactic” notion of dinaturality a characterisation of parametricity for <em>positive types</em> (system F types whose quantifiers are in positive positions), including your example: <em>“in the case of positive types, realizability, invariance with respect to logical relations, dinaturality and typability are equivalent properties for closed normal λ-terms”</em> [4, §7.1].</p>
<p>So there is indeed an elementary technique based on looking at shapes of normal forms, which provides a syntactic characterisation of some parametricity results including the &quot;free theorems&quot;, that also hints at a connection with categorical coherence.</p>
<p>[1]: Girard, J.-Y.; Scedrov, A. &amp; Scott, P. J. <em>Normal Forms and Cut-Free Proofs as Natural Transformations</em>. Logic From Computer Science, Mathematical Science Research Institute Publications 21, Springer-Verlag, 1992, 217-241.
<a href="http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.811" rel="nofollow noreferrer">http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.811</a></p>
<p>[2]: Bainbridge, E. S.; Freyd, P. J.; Scedrov, A. &amp; Scott, P. J. <em>Functorial polymorphism</em>. Theoretical computer science, Elsevier, 1990, 70, 35-64.
<a href="https://core.ac.uk/display/82270459" rel="nofollow noreferrer">https://core.ac.uk/display/82270459</a></p>
<p>[3]: De Lataillade, J. <em>Dinatural Terms in System F</em>. Logic in Computer Science, 24th Annual IEEE Symposium, 267-276, 2009. <a href="https://www.irif.fr/%7Edelatail/dinat.pdf" rel="nofollow noreferrer">https://www.irif.fr/~delatail/dinat.pdf</a></p>
<p>[4]: Pistone, P. <em>On completeness and parametricity in the realizability semantics of System F</em>.  Logical Methods in Computer Science, October 29, 2019, Volume 15, Issue 4. <a href="https://doi.org/10.23638/LMCS-15(4:6)2019" rel="nofollow noreferrer">https://doi.org/10.23638/LMCS-15(4:6)2019</a></p>

CC BY-SA 4.0
2022-09-30T09:20:42.633Z
The paper [3] proves dinaturality by the analysis of normal forms of lambda-terms. This is sufficient to prove that there is only one function of type $\forall X.\,X\to X$ in System F. However, as pointed out already, dinaturality is weaker than full relational parametricity. For example, dinaturality is insufficient to prove  that $\forall X.\,(X\to X)\to X\to X$ is equivalent to natural numbers. For that, you need something stronger. Short of full relational law, the property called "strong dinaturality" is sufficient for Church numbers. But it will be still insufficient for other cases.
winitzki
CC BY-SA 4.0
2022-10-02T20:30:30.437Z
Thanks, I have made some clarifications. First, I have restored the quote of [4] to mention like in my original answer the link with dinaturality (the original quote has changed between the preprint and the published version). Second, I have mentioned that [4] uses a so-called "syntactic" version of dinaturality for System F. This variant of dinaturality seems sufficent for Church numerals (Example 6.10 in [4]). With this in mind, we can still ask whether Theorem 6.16 in [4] (which generalizes the one in [1] to positive types) can be proved directly by looking at the shape of normal forms.
gadmm
CC BY-SA 4.0
2022-10-02T20:48:29.050Z
I meant Theorem 6.18 in [4].
gadmm
CC BY-SA 4.0
2023-01-06T18:33:25.773Z
I looked at Example 6.10 in [4]. The paper only shows that the Church numeral terms satisfy dinaturality. They do satisfy it. However, dinaturality is not sufficient for proving that the type of terms $\forall X.,(X\to X)\to X \to X$ is equivalent to the inductive type of natural numbers.
winitzki
CC BY-SA 4.0
2023-01-08T21:14:51.883Z
Right, my answer does not address the first question. It addresses the second one. It might be worthwhile developing your comment into a reply.
gadmm
CC BY-SA 4.0
2023-01-09T09:45:55.083Z
I refer to this question https://cs.stackexchange.com/questions/131901/how-to-prove-that-the-church-encoding-forall-r-f-r-r-r-gives-an-initi where I tried (and failed) to use dinaturality for proving that the Church-encoded natural numbers are equivalent to the inductive type of natural numbers. Dinaturality is too weak for that proof, one needs to use full relational parametricity. Relational parametricity in general does not follow from dinaturality.
winitzki
CC BY-SA 4.0
2019-02-12T19:21:21.170Z
2022-10-02T20:47:11.623Z
2022-10-02T20:47:11.623Z
gadmm
<p>There are many closed terms of a given type. For instance, both of these terms:</p>

<p><span class="math-container">$$ \lambda x . x $$</span>
<span class="math-container">$$ \lambda x . (\lambda y . y) x $$</span></p>

<p>have a type of a polymorphic identity function:</p>

<p><span class="math-container">$$ \forall X . X \rightarrow X$$</span></p>

<p>On the other hand, there is only one <em>normalized term</em> of that type i.e: <span class="math-container">$\lambda x . x$</span>.
Similarly, given the type of Church natural numbers:</p>

<p><span class="math-container">$$ \mathtt{Nat} = \forall X . (X \rightarrow X) \rightarrow X \rightarrow X $$</span> </p>

<p>one can argue that all the normal form terms of type <span class="math-container">$\mathtt{Nat}$</span> are in the form:</p>

<p><span class="math-container">$$\lambda s . \lambda z . s (\ldots (s\; z)) $$</span></p>

<p>Is there any research that goes along these lines and perhaps formalizes this intuition?  </p>

<p>Is this idea correct and strong enough to prove (by case analysis on the normal forms of the terms) 'free theorems' or more general parametricity results?</p>

<p>Clarification: The type system in question is System F</p>

CC BY-SA 4.0
2019-01-23T03:54:21.700Z
Note that the $\eta$-expansion has to be included in the definition of the normal form.
Łukasz Lew
CC BY-SA 4.0
2019-01-23T10:31:33.380Z
A small aside: You need to  specify the typing system you have in mind, because inhabitation strongly depend on the ambient typing system. Consider for example the (pure lambda-calculus versions of the) programs `let rec f x = f x` and `throw new Exception ("Hello Mum") `. What you have in mind is some variant of System F or F$\omega$.
Martin Berger
CC BY-SA 4.0
2019-01-23T13:25:52.083Z
I believe this is mostly folklore. See this blog post by Gabriel Scherer: http://prl.ccs.neu.edu/blog/2017/06/05/syntactic-parametricity-strikes-again/
Max New
CC BY-SA 4.0
2019-01-23T20:23:23.310Z
@MartinBerger indeed, I've meant System F.
Łukasz Lew
<lo.logic><type-theory><normalization><parametricity>
Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?
Łukasz Lew
# Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?

(Asked by: username_0 on 2019-01-23)

There are many closed terms of a given type. For instance, both of these terms:

$$ \lambda x . x $$
$$ \lambda x . (\lambda y . y) x $$

have a type of a polymorphic identity function:

$$ \forall X . X \rightarrow X$$

On the other hand, there is only one *normalized term* of that type i.e: $\lambda x . x$.
Similarly, given the type of Church natural numbers:

$$ \mathtt{Nat} = \forall X . (X \rightarrow X) \rightarrow X \rightarrow X $$

one can argue that all the normal form terms of type $\mathtt{Nat}$ are in the form:

$$\lambda s . \lambda z . s (\ldots (s\; z)) $$

Is there any research that goes along these lines and perhaps formalizes this intuition?

Is this idea correct and strong enough to prove (by case analysis on the normal forms of the terms) 'free theorems' or more general parametricity results?

Clarification: The type system in question is System F

**Tags:** lo.logic, type-theory, normalization, parametricity

> **Comments:**
> **username_0**: Note that the $\eta$-expansion has to be included in the definition of the normal form.  
> **username_1**: A small aside: You need to  specify the typing system you have in mind, because inhabitation strongly depend on the ambient typing system. Consider for example the (pure lambda-calculus versions of the) programs `let rec f x = f x` and `throw new Exception ("Hello Mum") `. What you have in mind is some variant of System F or F$\omega$.  
> **username_2**: I believe this is mostly folklore. See this blog post by Gabriel Scherer: http://prl.ccs.neu.edu/blog/2017/06/05/syntactic-parametricity-strikes-again/  
> **username_0**: @MartinBerger indeed, I've meant System F.  

---

## 2 answers

### Answer by username_3 on 2019-02-08. Score: 5 | Accepted answer

I thought this might be tough, given the fact that the proof usually goes in the other direction (Parametricity $\Rightarrow$ Normalization), and the post by Gabriel is somewhat involved, but in system F one can do a relatively straightforward induction.

I'm going to assume you're somewhat familiar with the usual statement of parametricty, e.g. from the "Theorems for free!" paper, and I'll treat only binary relations for simplicity.

I'll also be working in the "Curry-style" calculus for brevity.

> Theorem: if $T(X)$ is a type in system F with (only) the free type variable $X$, then for any well-typed term
> $$ \vdash t : \forall X.T(X)$$
> and any relation $\cal R$ between terms that respects $\beta\eta$,
> $$ t\ T({\cal R})\ t$$
> where $T(\cal R)$ is the parametricity relation defined in the usual way by induction on the structure of types.

The proof requires a more general lemma, which will handle arbitrary amounts of type variables and term variables (rather than working in a closed context).

Let $\theta$ be a map from type variables to $\beta\eta$ respecting binary relations over terms, and if $\Gamma$ is a type context, then $\sigma$ is a map from variables $x$ to pairs of terms $(u\_1, u\_2)$ such that, if $x : U\in\Gamma$, then $u\_1\ U\theta\ u\_2$, i.e. $u\_1$ and $u\_2$ are related by the parametricity relation at the appropriate type (where $\theta$ is used to instantiate type variables).

Given this, the lemma then states:

> Lemma: for any such $\theta, \Gamma, \sigma$, if $\Gamma \vdash t : T$, then $t\sigma\_1\ T\theta\ t\sigma\_2$. (With the obvious interpretation of $\sigma\_i$ as a plain substitution).

**Proof**. First we note that $T\theta$ is closed under $\beta\eta$ conversion, so we may take the **$\beta$-normal $\eta$-long normal form of $t$**, and reason by induction on its **size**.

Now we reason by **cases** (not induction!) on the structure of $T$.

Base case: suppose $T=X$. The normal form of $t$ is also of type $X$ and the only possible form is $x\ t\_1\ldots t\_n$, with the $t\_i$ in normal forms.

If t is just $x$, then $\sigma\_1(x)\ X\theta\ \sigma\_2(x)$ by construction.

Otherwise, by inversion the type of $x$ is $T'=T\_1\rightarrow\ldots\rightarrow T\_n\rightarrow X$. Now by construction, $\sigma\_1(x)\ T'\theta\sigma\_2(x)$, which means that $\sigma\_1(x\ t\_1\ldots t\_n)\ \theta(X)\ \sigma\_2(x\ t\_1\ldots t\_n)$ if $\sigma\_1(t\_i)\ T\_i\theta\ \sigma\_2(t\_i)$. But this is exactly the induction hypothesis.

Suppose now that $T=T\_1\rightarrow T\_2$. We proceed similarly: take 2 arbitrary terms $u$ and $u'$ such that $u\ T\_1\theta\ u'$. We need to show that $t\sigma\_1\ u\ T\_2\theta\ t\sigma\_2\ u'$. But by inversion again, (and the definition of $\eta$-long forms), $t$ must be of the form $\lambda x.t'$, so $t'\sigma\_1\ u\ =\_{\beta\eta}\ t'\sigma\_1'$, where $\sigma\_1'$ is $\sigma\_1$ extended with the mapping $x\mapsto u$, and similarly for $u'$.

The induction hypothesis applies again, using $\sigma'$ instead of $\sigma$.

Finally, if $T=\forall X.T'$, then inversion tells us that $\Gamma\vdash t:T'$, and $X$ does not appear free in $\Gamma$. This means we can take $\theta'$ to be $\theta$ extended with an arbitrary binding for $X$, which does not affect the correctness of $\sigma$, since $X$ does not appear in the types of any of the variables.

This gives $t\sigma\_1\ T'\theta'\ t\sigma\_2$ for an arbitrary such extension, implying $t\sigma\_1\ T\theta\ t\sigma\_2$, which concludes the proof.

---

I'm not 100% certain, but I suspect this proof *can* be carried out in some weak form of 2nd order arithmetic, which would show that normalization does imply parametricity in some strong sense.

> **Comments:**
> **username_0**: Cody, thank you for working that out, I appreciate that.  

---

### Answer by username_4 on 2019-02-12. Score: 7

I'd like to offer some pointers.

> Is there any research that goes along these lines and perhaps formalizes this intuition?

Parametricity by analysis of the shape of (simply-typed) normal forms preceded by a normalisation argument was proposed by Girard, Scedrov, and Scott [1]. This connects parametricity, cut-elimination in logic, and a proof technique for coherence in category theory. Here, parametricity is understood as a property of dinaturality, originally proposed for system F in [2].

> Is this idea correct and strong enough to prove (by case analysis on the normal forms of the terms) 'free theorems' or more general parametricity results?

In [1], it is noted that this includes the so-called "free theorems" as a special case. But the argument does not extend to all of system F, and dinaturality fails to capture relational parametricity (see e.g. [3]). On the other hand, a work by Paolo Pistone shows that one indeed obtains with a “syntactic” notion of dinaturality a characterisation of parametricity for *positive types* (system F types whose quantifiers are in positive positions), including your example: *“in the case of positive types, realizability, invariance with respect to logical relations, dinaturality and typability are equivalent properties for closed normal λ-terms”* [4, §7.1].

So there is indeed an elementary technique based on looking at shapes of normal forms, which provides a syntactic characterisation of some parametricity results including the "free theorems", that also hints at a connection with categorical coherence.

[1]: Girard, J.-Y.; Scedrov, A. & Scott, P. J. *Normal Forms and Cut-Free Proofs as Natural Transformations*. Logic From Computer Science, Mathematical Science Research Institute Publications 21, Springer-Verlag, 1992, 217-241.
<http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.811>

[2]: Bainbridge, E. S.; Freyd, P. J.; Scedrov, A. & Scott, P. J. *Functorial polymorphism*. Theoretical computer science, Elsevier, 1990, 70, 35-64.
<https://core.ac.uk/display/82270459>

[3]: De Lataillade, J. *Dinatural Terms in System F*. Logic in Computer Science, 24th Annual IEEE Symposium, 267-276, 2009. [https://www.irif.fr/~delatail/dinat.pdf](https://www.irif.fr/%7Edelatail/dinat.pdf)

[4]: Pistone, P. *On completeness and parametricity in the realizability semantics of System F*. Logical Methods in Computer Science, October 29, 2019, Volume 15, Issue 4. <https://doi.org/10.23638/LMCS-15(4:6)2019>

> **Comments:**
> **username_5**: The paper [3] proves dinaturality by the analysis of normal forms of lambda-terms. This is sufficient to prove that there is only one function of type $\forall X.\,X\to X$ in System F. However, as pointed out already, dinaturality is weaker than full relational parametricity. For example, dinaturality is insufficient to prove  that $\forall X.\,(X\to X)\to X\to X$ is equivalent to natural numbers. For that, you need something stronger. Short of full relational law, the property called "strong dinaturality" is sufficient for Church numbers. But it will be still insufficient for other cases.  
> **username_4**: Thanks, I have made some clarifications. First, I have restored the quote of [4] to mention like in my original answer the link with dinaturality (the original quote has changed between the preprint and the published version). Second, I have mentioned that [4] uses a so-called "syntactic" version of dinaturality for System F. This variant of dinaturality seems sufficent for Church numerals (Example 6.10 in [4]). With this in mind, we can still ask whether Theorem 6.16 in [4] (which generalizes the one in [1] to positive types) can be proved directly by looking at the shape of normal forms.  
> **username_4**: I meant Theorem 6.18 in [4].  
> **username_5**: I looked at Example 6.10 in [4]. The paper only shows that the Church numeral terms satisfy dinaturality. They do satisfy it. However, dinaturality is not sufficient for proving that the type of terms $\forall X.,(X\to X)\to X \to X$ is equivalent to the inductive type of natural numbers.  
> **username_4**: Right, my answer does not address the first question. It addresses the second one. It might be worthwhile developing your comment into a reply.  
> **username_5**: I refer to this question https://cs.stackexchange.com/questions/131901/how-to-prove-that-the-church-encoding-forall-r-f-r-r-r-gives-an-initi where I tried (and failed) to use dinaturality for proving that the Church-encoded natural numbers are equivalent to the inductive type of natural numbers. Dinaturality is too weak for that proof, one needs to use full relational parametricity. Relational parametricity in general does not follow from dinaturality.  

---

