Skip to main content

# Tag Info

## Hot answers tagged church-numerals

7 votes
Accepted

### How to prove that the Church encoding, forall r. (F r -> r) -> r, gives an initial algebra of the functor F?

$\newcommand{\fix}{\mathsf{fix}}$ $\newcommand{\fold}{\mathsf{fold}}$ $\newcommand{\map}{\mathsf{map}}$ Here is, I believe, how one would use parametricity to prove your last lemma. I'm going to ...
• 2,707
6 votes
Accepted

### How do I arrive at the multiplication function in lambda calculus?

You know that $(\bar{n}\ s)$ corresponds to $s^{(n)}$, i.e. function $s$ applied $n$ times to its argument. You want to obtain a function that iterates some function $s$ exactly $n \cdot m$ times. ...
• 3,479
5 votes

### Is there a systematic way to know when to alpha-transform free variables?

The answer here is the same as in the other question: one thing is missing here! Your addition result should be: $$3 + 4 = \lambda g . \lambda z . 3 g (4 g z) = \lambda g . \lambda z . 7 g z$$ Note ...
• 7,148
4 votes
Accepted

### lambda calculus with church numerals

Your term is the application $3\ 2\ succ\ 0$, where $succ$ is the successor function. If you task is to reduce this term to a beta normal form: First we can observe that for terms $M$ and $N$, ...
4 votes
Accepted

### Church numerals without functions

This is just a shorthand, leaving off some things that aren't really needed to understand the concepts. If you want your $7$ to be written as a function again, all you need are a couple more implicit ...
• 7,148
4 votes

### Is there a systematic way to know when to alpha-transform free variables?

Free variables never get $\alpha$-converted, only bound variables can. In the term $(\lambda x.\ xy)$ we can rename the bound variable $x$ to any other variable (except $y$, since that would cause a ...
• 14.6k
4 votes
Accepted

### How can I study the nature of the structure of evaluation of function in lambda calculus?

I'll try addressing only some of the questions. Church numerals are defined to be functions (abstractions in $\lambda$-calculus speech) that take two arguments: a base argument $z$ (stands for zero), ...
• 3,479
3 votes

### Why don't we encode church numerals like this?

I think what you really are asking for are criteria for judging correctness of coding. Once you have got these, you can answer your question on your own. Correctness of coding of some structure ...
• 30.9k
2 votes

### lambda calculus with church numerals

Essentially your term is the application $3\ 2\ {\sf succ}\ 0$. So we start performing beta reduction steps. Since $3\ f\ x = f(f(f x))$, we get $2\ (2\ (2\ {\sf succ}))\ 0$. From here, we get \$(2\ (2\...
• 14.6k
1 vote

### Is there a hierarchy of computational expressivity that is sensitive to evaluation strategies?

Most (or all) reasonable programming are Turing-complete, and thus can be used to compute exactly the computable functions, i.e., to decide the decidable languages, nothing more and nothing less. So ...
• 162k
1 vote

### Why don't we encode church numerals like this?

TWO := λf. f f THREE:= λf. f (f f) This looks like a type error to me. TWO and THREE ...
• 608
1 vote

### Why don't we encode church numerals like this?

I am the guy who posted this question. I somehow figure this out. In the original form, consider the succ operation is defined as below (+1). ...
• 177

Only top scored, non community-wiki answers of a minimum length are eligible