Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [church-numerals]

Church numerals are an encoding of integers in the lambda calculus

1
vote
2answers
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 ...
2
votes
1answer
38 views

Church numerals without functions

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} ...
3
votes
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 ...
4
votes
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 $n$ times to the second. Then I have the successor and ...
6
votes
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 ...
4
votes
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 ...
1
vote
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 ...
0
votes
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. \...
1
vote
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 $\...
10
votes
1answer
482 views

A lambda calculus evaluation involving Church numerals

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