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,927
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,499
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,176
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,176
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.7k
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$, ...
- 815
3
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.7k
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 ...
- 31.2k
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.♦
- 166k
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