1

I'm slightly confused by the successor function for Church numerals.

Written down in my textbook it is defined as follows:

$$succ = \lambda n. \lambda f. \lambda x. n \;f \; (f \; x) $$

Therefore incrementing a number $n$ by one works as follows:

$$ (\lambda n. \lambda f. \lambda x. n \; f \; (f \; x)) \; (\lambda f. \lambda x. f_n \; x)$$ $$ \rightarrow \lambda f. \lambda x. \; (\lambda f. \lambda x. f_n \; x) \; f \; (f \; x)$$ $$ \rightarrow \lambda f. \lambda x. (\lambda x. f_n \; x) \; (f \; x)$$ $$ \rightarrow \lambda f. \lambda x. (f_n \; (f \; x) $$ $$ = \lambda f. \lambda x. f_{n+1} \; x $$

where $n$ is represented as $\lambda f. \lambda x. f_{n} \; x$

My question is why would the following $succ$ formula not work:

$$ succ = \lambda n. (\lambda x. n) \; (f \; x)$$

I believe incrementing a number $n$ by one would work as follows using this formula:

$$ (\lambda n. (\lambda x. n) \; (f \; x)) \; (\lambda f. \lambda x. f_n \; x)$$ $$ \rightarrow (\lambda x. (\lambda f. \lambda x. f_n \; x)) \; (f \; x) $$ $$ \rightarrow \lambda f. \lambda x. f_n \; f \; x $$ $$ = \lambda f. \lambda x. f_{n+1} \; x$$

Does this formula not work because when I am performing $\beta$-reduction on the $x$ variable I am replacing the $x$ with $(f \; x)$ when I should not—possibly because it is bound by the inner abstraction?

George Herbert
  • 11
  • 1
    That formula has an $f$ as a free variable on the right hand side. That seems problematic to me, even though I know nothing about this topic really. – John Hughes Jan 01 '21 at 14:58
  • @JohnHughes Thanks. I've noticed the $x$ is also a free variable. Probably two of the multiple issues with it. Thanks. – George Herbert Jan 01 '21 at 15:21

1 Answers1

1

Here

$$ \underline{f} = (\lambda x. (\lambda fx. f^n x))(fx) $$

$(\lambda fx.f^n x)$ has its own scope and $x$ in it is bound by it.

So

$$ \underline{f} = (\lambda x. (\lambda fx. f^n x))(fx) = \lambda fx.f^n x = \underline{n} $$

And yes, your function gives wrong result.

Logan Lee
  • 249