History of Declarative Programming (2021)

> Church ends up defining zero as the identity function

Zero is not the identity function. Zero takes a function and calls it zero times. 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!)

Probably not possible unless you have academic credentials to back up your request like being a historian writing a book on the history of logic & computability.

The idea of Church numerals is quite similar to induction. An induction proof extends a method of treating the zero case and the successor case, to a treatment of all naturals. Or one can see it as defining the naturals as the numbers reachable by this process. The leap to Church numerals is not too big from this.

I own the Shen books, which were difficult to come by. This is different. I moved on as has nearly everyone else. Looking forward to someone picking up a project with the same goals as Shen without the drama. <fin>

Fair point, but I think it's a lot more true of functional ones.

The problem is pretty easy to see in a C-style for loop:

    for (int i = 0; i < 5; i++) {
        printf("%d\n", i);
        if (i % 2 == 0) i++;
    }

The index variable depends on it's value in previous versions of the loop and can be modified in the loop body! Can't parallelize that!

Side effects and mutation break many of the promises provided by functional constructs. Hybrid languages can illustrate this:

    # pure, parallelizable
    [2 * item for item in items]

    # side effect! order matters!
    [print(item) for item in items]

    # side effect! order matters!
    [arr.append(item) for item in items]