# Questions tagged [church-numerals]

Church numerals are an encoding of integers in the lambda calculus

10 questions
48 views

### lambda calculus with church numerals

today I found this term in our exercises: ((^fx.f(f(f x)) ^gy.g(g y )) ^z.z + 1) (0) I am quit unaware how to solve this type of question. I know this is the church numeral 3 , 2 , the identity ...
This is really a second part to my first question, but I felt that this was different enough from the first part that it merited its own question. So, using Church numerals, we define $3 = {\lambda} ... 2answers 46 views ### Is there a systematic way to know when to alpha-transform free variables? So, using Church numerals, we define$3 = {\lambda} f. {\lambda}x.f(f(f(x)))$, and$4 = {\lambda} f. {\lambda}x.f(f(f(f(x))))$. We can then add with an expression like$3\ g\ (4\ g\ z)$And ... 1answer 702 views ### How do I arrive at the multiplication function in lambda calculus? I'm familiar with how Church numerals are defined in the lambda calculus, i.e. as functions that take two arguments and apply the first argument$ntimes to the second. Then I have the successor and ... 4answers 171 views ### Why don't we encode church numerals like this? I think the following encoding also works. ZERO := λf. λx. x ONE := λf. f TWO := λf. f f THREE:= λf. f (f f) Note: the original encoding is ... 1answer 103 views ### How can I study the nature of the structure of evaluation of function in lambda calculus? I am specifically focusing on lambda calculus, following this paper: A Tutorial Introduction to the Lambda Calculus. Suppose we have three functions that represent the natural numbers 0 and 1, and a ... 1answer 90 views ### Recognizing primitive recursion I am trying to write a program to recognize if a given lambda calculus expression is primitive recursive. I believe that a general algorithm to do this does not exist, but I am interested in the most ... 1answer 27 views ### Can the lambda functions in Church numbers be swapped? I've learned that one can represent natural numbers with lambda calculus like this: \begin{align*} c_0 &= \lambda s. \lambda z. z\\ c_1 &= \lambda s. \lambda z. s~z\\ c_2 &= \lambda s. \... 1answer 170 views ### What's wrong with my beta reduction of pred c_0 on Church numerals? I'm trying to calculate\text{pred}\, c_0$, where$\text{pred}$is the previous church encoded number and$c_0$is the number$0$($\lambda s. \lambda z. z$). The formula for$\text{pred}$is$\...
I understand that a Church numeral $c_n$ looks like $\lambda s. \lambda z. s$ (... n times ...) $s\;z$. This means nothing more than "the function $s$ applied $n$ times to the function $z$". A ...