<p>Various people are interested in proving this sort of thing. Neel Krishnaswami mentioned this particular theorem <a href="http://lambda-the-ultimate.org/node/5011#comment-81851" rel="noreferrer">here</a>. I’ve also seen Frank Pfenning give some cool examples for ordered logics. For example, if you have $A, x : [A], y : [A] \vdash e : [A]$, then in an ordered type system, $e$ must append the lists $x$ and $y$.</p>

<p>The short answer is that yes, we can prove your first example. In the context of lambda calculi, a logical relations-based approach is described in <a href="https://dl.acm.org/citation.cfm?id=1947906" rel="noreferrer">this paper</a>. They would prove your theorem in two steps:</p>

<ol>
<li>Define a relational interpretation of types and use it to prove a conventional free theorem completely ignoring linearity i.e. essentially using the same reasoning you see in, for example, “Theorems for Free!”. Given $\vdash f : \forall A . [A] \multimap [A]$, the usual free theorem tells us that $f$ returns a list which contains only elements that were present in the list it was given. Given a list of distinct free linear variables $x_1 \ldots x_n$, we deduce that $f [x_1, ..., x_n]$ evaluates to some list $[y_1, ..., y_m]$ where $\{y_1, \ldots, y_m\} \subseteq \{x_1, ..., x_n\}$.</li>
<li>Notice that free linear variables must be preserved under evaluation. This lets us take advantage of linearity. If $[y_1, \ldots, y_m]$ were not a permutation of $[x_1, ..., x_n]$, then it would imply that some $x_i$ were lost or duplicated during evaluation, which cannot happen.</li>
</ol>

<p>But, these sorts of theorems get more interesting when we look at a language with effects and our ability to prove them for such languages is sadly limited. For example, consider the isomorphism $\tau \cong \forall A . (\tau \to A) \to A$ from System F. In a call-by-value setting, <a href="https://stackoverflow.com/a/45310975/568190">this isomorphism breaks</a> when we add non-termination. We should be able to recover a similar isomorphism, though, with linear types: $\tau \cong \forall A . (\tau \to A) \multimap A$. Unfortunately, we do not have operational logical relations that can prove this.</p>

<p>That said, there are also syntactic methods that can prove both this isomorphism and your theorem. This seems to be a particularly useful approach in a linear setting, and is much less of a burden than setting up a logical relation for proving simple theorems.</p>

<p><strong>Edit:</strong> Since you asked, here’s an example of a syntactic proof of a free theorem for the type $\forall A . (A \otimes A) \multimap A$ in a setting with a term $\bot$ that loops forever and is well-typed under any context at any type. The idea is to find a set of canonical terms of a type and use that to determine what the possible return values for a function are. We start with a soundness theorem for well-typed terms.</p>

<blockquote>
  <p><strong>Theorem (Canonicity).</strong> If $\Delta; \Gamma \vdash e : \tau$ then either</p>
  
  <ul>
  <li>$e \approx v$, which is a value such that $\Delta; \Gamma \vdash v : \tau$.</li>
  <li>$e \approx n$, a term which is stuck because it is trying to use a free variable in $\Gamma$, and $\Delta; \Gamma \vdash n : \tau$ OR</li>
  <li>$e \approx \bot$</li>
  </ul>
</blockquote>

<p>Here, $\approx$ is your favorite notion of equivalence for the language and $\Delta$ is an environment containing free type variables. I will consider free variables $x$ to be values. For simple languages, a straightforward progress &amp; preservation argument can be made to justify this theorem.</p>

<p>Now, given a value $\vdash f : \forall A . (A \otimes A) \multimap A$, we know that $f \approx \lambda x . e$ where $A; x : (A \otimes A) \vdash e : A$. From the type of e, we have a couple possible cases:</p>

<ul>
<li>$e$ is equivalent to a pair $A; x : (A \otimes A) \vdash (v_1, v_2) : A$. This case is impossible since $v_1$ and $v_2$ must be values of type $A$, which is a free type variable. There are no such values because there are no variables in the context of type $A$.</li>
<li>$e$ is equivalent to a term which tries to use the free variable $x$.</li>
<li>$e$ diverges. This case gives us one possible value for $f$: $\lambda x . \bot$.</li>
</ul>

<p>Since the second case is the only one left, we assume $e \approx\ \mathrm{let} (x_1, x_2) = x\ \mathrm{in}\ e’$ where $A; x_1 : A, x_2 : A \vdash e’ : A$. Thus far in the proof, we have established that $f \approx \lambda x . \mathrm{let }\ (x_1, x_2) = x\ \mathrm{ in }\ e’$. Finally, we apply our canonicity theorem one more time and find that $e’$ must diverge: the only values of type $A$ are variables but we have <strong>two</strong> variables in the context, so it cannot be the case that $e’ \approx x_i$.</p>

<p>Therefore, we have that the only inhabitant of $\forall A . (A \otimes A) \multimap A$ is $\lambda x . \bot \approx \lambda x . \mathrm{let }\ (x_1, x_2) = x\ \mathrm{ in }\ \bot$.</p>

<p>You asked for a reference for this sort of proof, but I’m not sure of a good one. This kind of reasoning is well-known in certain circles and goes back perhaps as far as Gentzen. I'm told that it is reminiscent of focused proof search for sequent calculus, but I don't know exactly what the connection is. </p>

<p>That said, I’m not aware of any modern published work that explains this relatively simple method well. Admittedly, it is a bit limited in its applicability to simpler languages. On the other hand, I think it has been overshadowed by “Theorems for Free!” et al and as a result even many senior researchers immediately think of logical relations when they hear the phrase “free theorem”, unaware that techniques like this can be a simpler alternative approach to such proofs (especially in the context of linear type systems).</p>

<p>As for your second example, I don’t think the free theorem you want actually holds. I could for example, instantiate $A$ with the integer type and then pass in a function that returns integers which are not in the list I give to $f$. Perhaps $\forall A. (\forall B. B \multimap (B, B)) \multimap [A] \multimap [A]$ is closer to the type you had in mind. But even then, no function of type $\forall B. B \multimap (B, B)$ exists since it would have to duplicate its input.</p>

CC BY-SA 4.0
2018-06-12T02:58:34.757Z
Can you give a reference for this syntactic method you speak of?
Łukasz Lew
CC BY-SA 4.0
2018-06-12T15:56:39.033Z
Not sure of a good reference, but I added an example to the post. Let me know if anything is unclear.
Nick Rioux
CC BY-SA 4.0
2018-06-12T18:17:09.837Z
Not linear, but here is a blog on using proof-theoretic analysis to obtain paramtricity-like theorems: http://prl.ccs.neu.edu/blog/2017/06/05/syntactic-parametricity-strikes-again/
Max New
CC BY-SA 4.0
2018-06-13T09:34:38.533Z
In addition to the Zhao et al paper linked in the post, Lars Birkedal and his coauthors extended also Reynolds' parametric model to the linear case in their paper [*Linear Abadi and Plotkin Logic*](https://arxiv.org/abs/cs/0611004).
Neel Krishnaswami
CC BY-SA 4.0
2018-06-14T10:12:45.300Z
This is interesting. But is $\approx$ meant to be beta-equivalence, beta-eta-equivalence or observational equivalence? To establish the theory of observational equivalence, you typically need logical relations even for many basic facts. A reference to which linear logic you're using would also be helpful — you use eta for pairs, but whether that's valid is usually subtle (at least in non-linear contexts).
Blaisorblade
CC BY-SA 4.0
2024-04-05T16:19:24.717Z
Are there any available resources that talk about the ordered logic examples that you mention Frank Pfenning giving?
David
CC BY-SA 4.0
2018-06-12T01:51:00.467Z
2018-06-12T16:04:09.627Z
2018-06-12T16:04:09.627Z
Nick Rioux
<p>Are we able to prove a free parametricity theorems about functions like $f : \forall A . [A] ⊸ [A]$? 
It is supposed to state that $f$ takes a list and always returns a permutation of it.</p>

<p>Another example: prove that function $f : \forall A . (A ⊸ (A, A)) ⊸ [A] ⊸ [A]$ will always return a permuted list with exactly one element copied.</p>

CC BY-SA 4.0
2018-06-10T10:50:21.120Z
Yes, that's possible. We have explored this theme in a slightly different setting (the [polymorphic, linear $\pi$-calculus](http://users.sussex.ac.uk/~mfb21/publications/fossacs03/fossacs03.pdf)).
Martin Berger
<linear-logic><parametricity>
Parametricity of Linear Logic
Łukasz Lew
# Parametricity of Linear Logic

(Asked by: username_0 on 2018-06-09)

Are we able to prove a free parametricity theorems about functions like $f : \forall A . [A] ⊸ [A]$?
It is supposed to state that $f$ takes a list and always returns a permutation of it.

Another example: prove that function $f : \forall A . (A ⊸ (A, A)) ⊸ [A] ⊸ [A]$ will always return a permuted list with exactly one element copied.

**Tags:** linear-logic, parametricity

> **Comments:**
> **username_1**: Yes, that's possible. We have explored this theme in a slightly different setting (the [polymorphic, linear $\pi$-calculus](http://users.sussex.ac.uk/~mfb21/publications/fossacs03/fossacs03.pdf)).  

---

## 1 answers

### Answer by username_2 on 2018-06-12. Score: 8 | Accepted answer

Various people are interested in proving this sort of thing. username_4 mentioned this particular theorem [here](http://lambda-the-ultimate.org/node/5011#comment-81851). I’ve also seen Frank Pfenning give some cool examples for ordered logics. For example, if you have $A, x : [A], y : [A] \vdash e : [A]$, then in an ordered type system, $e$ must append the lists $x$ and $y$.

The short answer is that yes, we can prove your first example. In the context of lambda calculi, a logical relations-based approach is described in [this paper](https://dl.acm.org/citation.cfm?id=1947906). They would prove your theorem in two steps:

1. Define a relational interpretation of types and use it to prove a conventional free theorem completely ignoring linearity i.e. essentially using the same reasoning you see in, for example, “Theorems for Free!”. Given $\vdash f : \forall A . [A] \multimap [A]$, the usual free theorem tells us that $f$ returns a list which contains only elements that were present in the list it was given. Given a list of distinct free linear variables $x\_1 \ldots x\_n$, we deduce that $f [x\_1, ..., x\_n]$ evaluates to some list $[y\_1, ..., y\_m]$ where $\{y\_1, \ldots, y\_m\} \subseteq \{x\_1, ..., x\_n\}$.
2. Notice that free linear variables must be preserved under evaluation. This lets us take advantage of linearity. If $[y\_1, \ldots, y\_m]$ were not a permutation of $[x\_1, ..., x\_n]$, then it would imply that some $x\_i$ were lost or duplicated during evaluation, which cannot happen.

But, these sorts of theorems get more interesting when we look at a language with effects and our ability to prove them for such languages is sadly limited. For example, consider the isomorphism $\tau \cong \forall A . (\tau \to A) \to A$ from System F. In a call-by-value setting, [this isomorphism breaks](https://stackoverflow.com/a/45310975/568190) when we add non-termination. We should be able to recover a similar isomorphism, though, with linear types: $\tau \cong \forall A . (\tau \to A) \multimap A$. Unfortunately, we do not have operational logical relations that can prove this.

That said, there are also syntactic methods that can prove both this isomorphism and your theorem. This seems to be a particularly useful approach in a linear setting, and is much less of a burden than setting up a logical relation for proving simple theorems.

**Edit:** Since you asked, here’s an example of a syntactic proof of a free theorem for the type $\forall A . (A \otimes A) \multimap A$ in a setting with a term $\bot$ that loops forever and is well-typed under any context at any type. The idea is to find a set of canonical terms of a type and use that to determine what the possible return values for a function are. We start with a soundness theorem for well-typed terms.

> **Theorem (Canonicity).** If $\Delta; \Gamma \vdash e : \tau$ then either
>
> * $e \approx v$, which is a value such that $\Delta; \Gamma \vdash v : \tau$.
> * $e \approx n$, a term which is stuck because it is trying to use a free variable in $\Gamma$, and $\Delta; \Gamma \vdash n : \tau$ OR
> * $e \approx \bot$

Here, $\approx$ is your favorite notion of equivalence for the language and $\Delta$ is an environment containing free type variables. I will consider free variables $x$ to be values. For simple languages, a straightforward progress & preservation argument can be made to justify this theorem.

Now, given a value $\vdash f : \forall A . (A \otimes A) \multimap A$, we know that $f \approx \lambda x . e$ where $A; x : (A \otimes A) \vdash e : A$. From the type of e, we have a couple possible cases:

* $e$ is equivalent to a pair $A; x : (A \otimes A) \vdash (v\_1, v\_2) : A$. This case is impossible since $v\_1$ and $v\_2$ must be values of type $A$, which is a free type variable. There are no such values because there are no variables in the context of type $A$.
* $e$ is equivalent to a term which tries to use the free variable $x$.
* $e$ diverges. This case gives us one possible value for $f$: $\lambda x . \bot$.

Since the second case is the only one left, we assume $e \approx\ \mathrm{let} (x\_1, x\_2) = x\ \mathrm{in}\ e’$ where $A; x\_1 : A, x\_2 : A \vdash e’ : A$. Thus far in the proof, we have established that $f \approx \lambda x . \mathrm{let }\ (x\_1, x\_2) = x\ \mathrm{ in }\ e’$. Finally, we apply our canonicity theorem one more time and find that $e’$ must diverge: the only values of type $A$ are variables but we have **two** variables in the context, so it cannot be the case that $e’ \approx x\_i$.

Therefore, we have that the only inhabitant of $\forall A . (A \otimes A) \multimap A$ is $\lambda x . \bot \approx \lambda x . \mathrm{let }\ (x\_1, x\_2) = x\ \mathrm{ in }\ \bot$.

You asked for a reference for this sort of proof, but I’m not sure of a good one. This kind of reasoning is well-known in certain circles and goes back perhaps as far as Gentzen. I'm told that it is reminiscent of focused proof search for sequent calculus, but I don't know exactly what the connection is.

That said, I’m not aware of any modern published work that explains this relatively simple method well. Admittedly, it is a bit limited in its applicability to simpler languages. On the other hand, I think it has been overshadowed by “Theorems for Free!” et al and as a result even many senior researchers immediately think of logical relations when they hear the phrase “free theorem”, unaware that techniques like this can be a simpler alternative approach to such proofs (especially in the context of linear type systems).

As for your second example, I don’t think the free theorem you want actually holds. I could for example, instantiate $A$ with the integer type and then pass in a function that returns integers which are not in the list I give to $f$. Perhaps $\forall A. (\forall B. B \multimap (B, B)) \multimap [A] \multimap [A]$ is closer to the type you had in mind. But even then, no function of type $\forall B. B \multimap (B, B)$ exists since it would have to duplicate its input.

> **Comments:**
> **username_0**: Can you give a reference for this syntactic method you speak of?  
> **username_2**: Not sure of a good reference, but I added an example to the post. Let me know if anything is unclear.  
> **username_3**: Not linear, but here is a blog on using proof-theoretic analysis to obtain paramtricity-like theorems: http://prl.ccs.neu.edu/blog/2017/06/05/syntactic-parametricity-strikes-again/  
> **username_4**: In addition to the Zhao et al paper linked in the post, Lars Birkedal and his coauthors extended also Reynolds' parametric model to the linear case in their paper [*Linear Abadi and Plotkin Logic*](https://arxiv.org/abs/cs/0611004).  
> **username_5**: This is interesting. But is $\approx$ meant to be beta-equivalence, beta-eta-equivalence or observational equivalence? To establish the theory of observational equivalence, you typically need logical relations even for many basic facts. A reference to which linear logic you're using would also be helpful — you use eta for pairs, but whether that's valid is usually subtle (at least in non-linear contexts).  
> **username_6**: Are there any available resources that talk about the ordered logic examples that you mention Frank Pfenning giving?  

---

