While I don't know much about Church numbers or the theory how lambda calculus works, taking a glance at the definitions on wikipedia they seem to be the math idea of how numbers works (at the meta level)

I forgot the name of this, but they seem the equivalent of successors in math In the low level math theory you represent numbers as sequences of successors from 0 (or 1 I forgot)

Basically you have one then sucessor of one which is two, sucessor of two and so on So a number n is n successor operations from one

To me it seems Church numbers replace this sucessor operation with a function but it's the same idea

▲ rtpg a day ago | parent [-]

Church ends up defining zero as the identity function, and N as "apply a function to a zero-unit N times"

While defining numbers in terms of their successors is decently doable, this logical jump (that works super well all things considered!) to making numbers take _both_ the successor _and_ the zero just feels like a great idea, and it's a shame to me that the papers I read from Church didn't intuit how to get there.

After the fact, with all the CS reflexes we have, it might be ... easier to reach this definition if you start off "knowing" you could implement everything using just functions and with some idea of not having access to a zero, but even then I think most people would expect these objects to be some sort of structure rather than a process.

There is, of course, the other possibility which is just that I, personally, lack imagination and am not as smart as Alonzo Church. That's why I want to know the thought process!

	▲	itishappy 11 hours ago \| parent [-]
		> Church ends up defining zero as the identity function Zero is not the identity function. Zero takes a function and calls it zero times on a second function. The end result of this is that it returns the identity function. In Haskell it would be `const id` instead of `id`. `zero := λf.λx.x one := λf.λx.fx two := λf.λx.ffx id := λx.x` I suspect that this minor misconception may lead you to an answer to your original question! Why isn't the identity function zero? Given that everything in lambda calculus is a function, and the identity function is the simplest function possible, it would make sense to at least try! If you try, I suspect you'll quickly find that it starts to break down, particularly when you start trying to treat your numerals as functions (which is, after all, their intended purpose). Church numerals are a minimal encoding. They are as simple as it possibly gets. This may not speak to Church's exact thought process, but I think it does highlight that there exists a clear process that anyone might follow in order to get Church's results. In other words, I suspect that his discover was largely mechanical, rather than a moment of particularly deep insight. (And I don't think this detracts from Church's brilliance at all!)