Skip to main content
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 ...
Dan Doel's user avatar
  • 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. ...
Anton Trunov's user avatar
  • 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 ...
Draconis's user avatar
  • 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$, ...
Natalie Clarius's user avatar
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 ...
Draconis's user avatar
  • 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 ...
chi's user avatar
  • 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), ...
Anton Trunov's user avatar
  • 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 ...
Andrej Bauer's user avatar
  • 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\...
chi's user avatar
  • 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 ...
D.W.'s user avatar
  • 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 ...
Bergi's user avatar
  • 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). ...
czheo's user avatar
  • 177

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