The well-known Church encoding of natural numbers can be generalized to use an arbitrary (covariant) functor `F`. The result is the type, call it `C`, defined by ``` data C = Cfix { run :: forall r. (F r -> r) -> r } ``` Here and below, for simplicity, we will assume that `F` is a fixed, already defined functor. It is widely known and stated that the type `C` is a fixpoint of the functor `F`, and also that `C` is an initial `F`-algebra. For example, if the functor `F a` is defined by ``` data F a b = Empty | Cons a b ``` then a fixpoint of `F a` is `[a]` (the list of values of type `a`). Also, `[a]` is the initial algebra. The Church encoding of lists is well known. But I could not find a rigorous proof of either of these statements (`C` is a fixpoint, and `C` is the initial algebra). The question is, how to prove rigorously one of the two statements: - The type `C` is a fixpoint of the type isomorphism `F C ≅ C`. In other words, we need to prove that there exist two functions, `fix :: F C -> C` and `unfix :: C -> F C` such that `fix . unfix = id` and `unfix . fix = id`. - The type `C` is the initial algebra of the functor `F`; that is, the initial object in the category of `F`-algebras. In other words, for any type `A` such that a function `p :: F A -> A` is given (that is, `A` is an `F`-algebra), we can find a unique function `q :: C -> A` which is an F-algebra morphism. This means, `q` must be such that the law `q . fix = p . fmap q` holds. We need to prove that, given `A` and `p`, such `q` exists and is unique. These two statements are not equivalent; but proving (2) implies (1). (Lambek's theorem says that an initial algebra is an isomorphism.) The code of the functions `fix` and `unfix` can be written relatively easily: ``` fix :: F C -> C fix fc = Cfix (forall r. \g -> g . fmap (\h -> h g) fc ) unfix :: C -> F C unfix c = (run c) (fmap fix) ``` Given a function `p :: F A -> A`, the code of the function `q` is written as ``` q :: C -> A q c =

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 this reduces to: $(g (g (g (g (g (g (g\ z)))))))$ ... but why? $g$ is a free variable in each expression, and my understanding is that you must ${\alpha}$-convert free standing variables in unrelated expressions. Shouldn't we instead end up with something like $(g (g (g (g_2 (g_2 (g_2 (g_2\ z)))))))$?

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 addition functions, both of which I managed to derive and understand: $$\begin{align} \mathrm{succ} &:= \lambda nsz.s (n s z) \\ (+) &:= \lambda nm.n\ succ\ m \\ \end{align} $$ But multiplication is where I'm stuck. I understand that we can define a multiplication function $(*)$ by adding the number $m$ to $0$ exactly $n$ times. After all, $3 \times 2$ is simply $2 + 2 + 2 + 0$. So that could mean that $(*)$ looks like this: $$(*) := \lambda nm.n\ ((+)\ m)\ 0$$ This appears to be a somewhat intuitive definition of a lambda calculus multiplication function to me, and if I try it out with $2$ and $3$, after some messy reductions, the result seems correct and $(*)\,2\,3 \rightarrow 6$. But then elsewhere I found this definition for multiplication: $$\mathrm{mult} := \lambda xya.x (y a)$$ Now I don't see how you arrive at this function $\mathrm{mult}$. My definition $(*)$, which takes two arguments, seems intuitive enough to me. But his here, which takes two arguments, one for the $x$ and $y$ respectively, which are the numbers to be multiplied, and then a third one $a$, just seems impenetrable to me—and I cannot figure out why it works, or how you would derive it. Can somebody help me understand the reasoning and derivation of this $\mathrm{mult}$ function?

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 ``` ZERO := λf. λx. x ONE := λf. λx. f x TWO := λf. λx. f (f x) THREE:= λf. λx. f (f (f x)) ``` Why is the original one better?

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 successor function: $\lambda sz.z = 0$ $\lambda sz.s(z) = 1$ $\lambda wyx.y(wyx) = succ$ Suppose I were to evaluate $succ\ succ\ 1$. As I evaluate this expression, it is becoming clear to me that it's not 3 as I might naively expect, but I do not truly grasp "why." Even as I go through the motions of evaluating the expression, I do not understand the nature of the turn of events and why certain expressions produce a certain result due to their structure and construction. A question I might ask would be something like, why does $succ$ have that form, and is there an alternative form for $succ$ that produces the same result? If it is unique, what makes it special? I don't know how to answer these questions well yet, so I am seeking guidance. Is there a method by which I can better visualize or understand the evaluation of expressions and how it affects the "class" of their output? I am very new to lambda calculus, so please excuse me. Edit: I think I understand the rules for evaluation of lambda calculus (substitution, prevention of name collisions, etc.), but I have a hard time understanding the arbitrary rules by which one can construct lambda calculus' equivalent forms for the natural numbers, the successor functions, and the addition and multiplication functions. It's how these parallels to these concepts were mapped over to lambda calculus that I am interested in. For example, why are the functions for "choose second," "false," and "discard next argument," and "0" have the same form and thus equivalent? There exists systems in which applying the zero function to a list of object does not result in returning a list with the front-most argument removed. Even if it is a convention, is there a reason why it is structured as such? For example, why is does the suc

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 possible definition of the $\mathtt{times}$ function is the following: $\mathtt{times} = \lambda m. \lambda n. \lambda s. m \; (n\; s)$. Looking at the body, I understand the logic behind the function. However, when I start evaluating, I get stuck. I will illustrate it with an example: $$\begin{align*} (\lambda m. \lambda n. \lambda s. m \; (n\; s))(\lambda s.\lambda z.s\;s\;z)(\lambda s.\lambda z.s\;s\;s\;z) \mspace{-4em} \\ \to^*& \lambda s. (\lambda s.\lambda z.s\;s\;z) \; ((\lambda s.\lambda z.s\;s\;s\;z)\; s)) \\ \to^*& \lambda s. (\lambda s.\lambda z.s\;s\;z) \; (\lambda z.s\;s\;s\;z) \\ \to^*& \lambda s. \lambda z.(\lambda z.s\;s\;s\;z)\;(\lambda z.s\;s\;s\;z)\;z \end{align*}$$ Now in this situation, if I first apply $(\lambda z.s\;s\;s\;z)\;z$, I get to the desired result. However, if I apply $(\lambda z.s\;s\;s\;z)\;(\lambda z.s\;s\;s\;z)$ first, as I should because application is associative from the left, I get a wrong result: $\lambda s. \lambda z.(\lambda z.s\;s\;s\;z)\;(\lambda z.s\;s\;s\;z)\;z \to \lambda s. \lambda z.(s\;s\;s\;(\lambda z.s\;s\;s\;z))\;\;z$ I can no longer reduce this. What am I doing wrong? The result should be $\lambda s. \lambda z.s\;s\;s\;s\;s\;s\;z$