In Lectures on the Curry-Howard Isomorphism, by Sørensen and Urzyczin, it is informed that these two definitions of the successor function over the Church numerals aren't $\beta$-equal: $$ A_s = \lambda x. \lambda s. \lambda z. s\ (x\ s\ z) \\ A_s^{'} = \lambda x. \lambda s. \lambda z. x\ s\ (s\ z) $$

One can easily calculate that $$ A_s c_n =_\beta c_{n+1} \\ A_s^{'} c_n =_\beta c_{n+1} $$

And, from the definition of the $=_\beta$ relation, we have that it's symmetric and also transitive. So, one could argue $$ A_s c_n =_\beta c_{n+1}\ \land\ c_{n+1}=_{\beta} A_s^{'} c_n \implies A_s c_n =_\beta A_s^{'} c_n $$

But since the authors said this isn't the case, I don't see where I made the mistake.


1 Answer 1


The fact that $A_s$ and $A_s’$ give equal results when applied to Church numerals does not mean they are equal. It is true that for all $n \in \mathbb{N}$, $A_s c_n =_\beta A_s’ c_n =_\beta c_{n + 1}$. However, there is no rule of the lambda calculus saying this means $A_s =_\beta A_s’$; in fact, they are not $\beta$-equivalent, since they are both in normal form and are not $\alpha$ equivalent.

  • $\begingroup$ Hmm, I think was a misinterpretation of my part. I thought the authors were saying that both terms, when applied to the Church numeral $c_n$, were not $\beta$-equal. Apparently, they were saying that the terms by themselves (not applied to anyone, therefore not computing anything), are not $\beta$-equal which does indeed make sense. $\endgroup$
    – user1045405
    Commented Feb 23, 2023 at 0:25

You must log in to answer this question.