5
$\begingroup$

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)".

$\endgroup$
  • $\begingroup$ I would imagine they are talking about the fact that the polymorphic $\lambda$-calculus is strongly normalizing. $\endgroup$ – Andrej Bauer Nov 24 '14 at 13:15
  • $\begingroup$ How would strong normalization imply the assertion? $\endgroup$ – lambda2 Nov 24 '14 at 13:20
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Nov 24 '14 at 13:48
  • $\begingroup$ 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? $\endgroup$ – lambda2 Nov 24 '14 at 13:52
  • 1
    $\begingroup$ @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. $\endgroup$ – Damiano Mazza Nov 24 '14 at 21:10
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.