<p>The fact that $\mathsf{Add}\ u\ v = \mathsf{Add}\ v\ u$ is not provable for arbitrary $u$ and $v$ does indeed follow from the Church-Rosser property.</p>

<p>Write $u =_\beta v$ if $u \mathrel{({}_\beta\!\!\leftarrow\cup\rightarrow_\beta)^\ast} v$, where $\rightarrow_\beta$ is $\beta$-reduction in System F and $(\cdot)^\ast$ is the reflexive-transitive closure operator (this is a possible definition of $\beta$-equality, which Breazu-Tannen and Coquand denote simply by $=$. Here I will use the $\beta$ subscript and keep the $=$ symbol for strict equality, i.e., $\alpha$-equivalence if you like).  It follows immediately from the definition that if two terms have a common reduct, i.e., $u\rightarrow_\beta^\ast w$ and $v\rightarrow_\beta^\ast w$, then $u=_\beta v$. The Church-Rosser theorem states that the converse also holds:
$$u=_\beta v \quad \textrm{implies}\quad \exists w.\ u\rightarrow^\ast w\textrm{ and }v\rightarrow^\ast w.$$
It follows that $\beta$-equivalent normal forms are necessarily identical:
$$u,v\textrm{ normal and }u=_\beta v\textrm{ implies }u=v.$$</p>

<p>Read contrapositively, the above says that different normal forms can never be $\beta$-equivalent. Now, suppose $\mathsf{Add}\ u\ v=_\beta\mathsf{Add}\ v\ u$ for arbitrary $u$, $v$. In particular, this holds when $u=x$ and $v=y$ are distinct variables of type $polyint$. But it is easy to show (just apply a couple of steps of $\rightarrow_\beta$) that $\mathsf{Add}\ x\ y=_\beta u'$ and $\mathsf{Add}\ y\ x=_\beta v'$ with $u'$ and $v'$ distinct normal forms. Contradiction.</p>

CC BY-SA 3.0
2014-11-24T21:03:07.133Z
2014-11-25T09:34:02.070Z
2014-11-25T09:34:02.070Z
Damiano Mazza
<p>In the article "Extensional models of polymorphism" by Breazu-Tannen and Coquand, natural numbers are presented using a Church-like encoding:</p>

<p>$polyint = \forall t . (t \to t) \to t \to t$</p>

<p>Addition for this encoding is introduced as:</p>

<p>$\mathsf{Add} = \lambda u,v : polyint . \Lambda t . \lambda f : t \to t . \lambda x : t . u t f (v t f x)$</p>

<p>Then they say that commutativity of addition cannot be proved, and they say that $\mathsf{Add} u v = \mathsf{Add} v u$ does not follow from polymorphic lambda calculus theory by a simple Church-Rosser argument. What's this Church-Rosser argument? Is it related to the Church-rosser property? How can I prove it?</p>

<p>EDIT: the exact statement is:</p>

<p>"However, the pure $\lambda^{\forall}$ is not sufficient for that, as it cannot even prove, for example, that the operation of addition is commutative:</p>

<p>$\mathsf{Add}\ u\  v = \mathsf{Add}\ v\ u$</p>

<p>with arbitrary $u, v : polyint$ is not provable in $\lambda^{\forall}$ (by a simple Church-Rosser argument)".</p>

CC BY-SA 3.0
2014-11-24T13:15:04.860Z
I would imagine they are talking about the fact that the polymorphic $\lambda$-calculus is strongly normalizing.
Andrej Bauer
CC BY-SA 3.0
2014-11-24T13:20:50.080Z
How would strong normalization imply the assertion?
lambda2
CC BY-SA 3.0
2014-11-24T13:48:59.797Z
It wouldn't, and that's what they are saying, as you write yourself: "does *not* follow from the Church-Rosser argument". Other things do follow, for example the fact that $\mathsf{Add}\,u\,z = u$ where $z = \Lambda t \lambda f x . x$ is "zero" is obtained by reducing all $\beta$-redexes on the left-hand side.
Andrej Bauer
CC BY-SA 3.0
2014-11-24T13:52:22.823Z
Sorry, I meant the assertion that says that "it does not follow that ...". How is that $\mathsf{Add} u v = \mathsf{Add} v u$ contradicts strong normalization?
lambda2
CC BY-SA 3.0
2014-11-24T15:38:14.750Z
It doesn't *contradict* CR, it just doesn't "trivially follow" from it. In general, to prove commutativity, you need some kind of characterization of *all* possible normal forms of each argument. It is possible to build models in which, for example, there are some elements of type $polyint$ that are not of the form $S(S(\ldots S(0)\ldots)$, and so the equation may not hold in those models.
cody
CC BY-SA 3.0
2014-11-24T17:22:02.783Z
I've edited the question to cite exactly the authors. They affirm that commutativity is not provable in polymorphic lambda calculus. I understand that they say that that it can be shown not to be provable by a simple Church-Rosser argument. How do they prove the non-provability of commutativity?
lambda2
CC BY-SA 3.0
2014-11-24T21:03:52.370Z
@AndrejBauer, just a remark: it seems to me that you are confusing Church-Rosser (which is essentially the transitivity of $\beta$-equality) with (strong) normalization.
Damiano Mazza
CC BY-SA 3.0
2014-11-24T21:10:53.163Z
@cody: what you say is absolutely true but I think is not what Breazu-Tannen and Coquand are saying. Their point (which has been made explicit by the OP's last comment) is that the fact that the equality is *not* provable is itself provable using Church-Rosser.
Damiano Mazza
CC BY-SA 3.0
2014-11-25T08:17:45.013Z
Ah yes, sorry. Count me as confused.
Andrej Bauer
<lambda-calculus><type-systems><polymorphism><typed-lambda-calculus>
Commutativity of addition in polymorphic lambda calculus
lambda2
# Commutativity of addition in polymorphic lambda calculus

(Asked by: username_0 on 2014-11-24)

In the article "Extensional models of polymorphism" by Breazu-Tannen and Coquand, natural numbers are presented using a Church-like encoding:

$polyint = \forall t . (t \to t) \to t \to t$

Addition for this encoding is introduced as:

$\mathsf{Add} = \lambda u,v : polyint . \Lambda t . \lambda f : t \to t . \lambda x : t . u t f (v t f x)$

Then they say that commutativity of addition cannot be proved, and they say that $\mathsf{Add} u v = \mathsf{Add} v u$ does not follow from polymorphic lambda calculus theory by a simple Church-Rosser argument. What's this Church-Rosser argument? Is it related to the Church-rosser property? How can I prove it?

EDIT: the exact statement is:

"However, the pure $\lambda^{\forall}$ is not sufficient for that, as it cannot even prove, for example, that the operation of addition is commutative:

$\mathsf{Add}\ u\ v = \mathsf{Add}\ v\ u$

with arbitrary $u, v : polyint$ is not provable in $\lambda^{\forall}$ (by a simple Church-Rosser argument)".

**Tags:** lambda-calculus, type-systems, polymorphism, typed-lambda-calculus

> **Comments:**
> **username_1**: I would imagine they are talking about the fact that the polymorphic $\lambda$-calculus is strongly normalizing.  
> **username_0**: How would strong normalization imply the assertion?  
> **username_1**: It wouldn't, and that's what they are saying, as you write yourself: "does *not* follow from the Church-Rosser argument". Other things do follow, for example the fact that $\mathsf{Add}\,u\,z = u$ where $z = \Lambda t \lambda f x . x$ is "zero" is obtained by reducing all $\beta$-redexes on the left-hand side.  
> **username_0**: Sorry, I meant the assertion that says that "it does not follow that ...". How is that $\mathsf{Add} u v = \mathsf{Add} v u$ contradicts strong normalization?  
> **username_2**: It doesn't *contradict* CR, it just doesn't "trivially follow" from it. In general, to prove commutativity, you need some kind of characterization of *all* possible normal forms of each argument. It is possible to build models in which, for example, there are some elements of type $polyint$ that are not of the form $S(S(\ldots S(0)\ldots)$, and so the equation may not hold in those models.  
> **username_0**: I've edited the question to cite exactly the authors. They affirm that commutativity is not provable in polymorphic lambda calculus. I understand that they say that that it can be shown not to be provable by a simple Church-Rosser argument. How do they prove the non-provability of commutativity?  
> **username_3**: @AndrejBauer, just a remark: it seems to me that you are confusing Church-Rosser (which is essentially the transitivity of $\beta$-equality) with (strong) normalization.  
> **username_3**: @username_2: what you say is absolutely true but I think is not what Breazu-Tannen and Coquand are saying. Their point (which has been made explicit by the OP's last comment) is that the fact that the equality is *not* provable is itself provable using Church-Rosser.  
> **username_1**: Ah yes, sorry. Count me as confused.  

---

## 1 answers

### Answer by username_3 on 2014-11-24. Score: 4 | Accepted answer

The fact that $\mathsf{Add}\ u\ v = \mathsf{Add}\ v\ u$ is not provable for arbitrary $u$ and $v$ does indeed follow from the Church-Rosser property.

Write $u =\_\beta v$ if $u \mathrel{({}\_\beta\!\!\leftarrow\cup\rightarrow\_\beta)^\ast} v$, where $\rightarrow\_\beta$ is $\beta$-reduction in System F and $(\cdot)^\ast$ is the reflexive-transitive closure operator (this is a possible definition of $\beta$-equality, which Breazu-Tannen and Coquand denote simply by $=$. Here I will use the $\beta$ subscript and keep the $=$ symbol for strict equality, i.e., $\alpha$-equivalence if you like). It follows immediately from the definition that if two terms have a common reduct, i.e., $u\rightarrow\_\beta^\ast w$ and $v\rightarrow\_\beta^\ast w$, then $u=\_\beta v$. The Church-Rosser theorem states that the converse also holds:
$$u=\_\beta v \quad \textrm{implies}\quad \exists w.\ u\rightarrow^\ast w\textrm{ and }v\rightarrow^\ast w.$$
It follows that $\beta$-equivalent normal forms are necessarily identical:
$$u,v\textrm{ normal and }u=\_\beta v\textrm{ implies }u=v.$$

Read contrapositively, the above says that different normal forms can never be $\beta$-equivalent. Now, suppose $\mathsf{Add}\ u\ v=\_\beta\mathsf{Add}\ v\ u$ for arbitrary $u$, $v$. In particular, this holds when $u=x$ and $v=y$ are distinct variables of type $polyint$. But it is easy to show (just apply a couple of steps of $\rightarrow\_\beta$) that $\mathsf{Add}\ x\ y=\_\beta u'$ and $\mathsf{Add}\ y\ x=\_\beta v'$ with $u'$ and $v'$ distinct normal forms. Contradiction.


---

