It’s been said that structured programming is programming without GOTO, and functional programming is programming without assignment statements. Is declarative programming then programming without the concept of linear time?
Very interesting historical document, though I don't have that much confidence in the precision of the explanation of the terms.
Related to this: does anyone know if there's any document that delves into how Church landed on Church numerals in particular? I get how they work, etc, but at least the papers I saw from him seem to just drop the definition out of thin air.
Were church numerals capturing some canonical representation of naturals in logic that was just known in the domain at the time? Are there any notes or the like that provide more insight?
Before Church there was Peano, and before Peano there was Grassmann
> It is rather well-known, through Peano's own acknowledgement, that Peano […] made extensive use of Grassmann's work in his development of the axioms. It is not so well-known that Grassmann had essentially the characterization of the set of all integers, now customary in texts of modern algebra, that it forms an ordered integral domain in which each set of positive elements has a least member. […] [Grassmann's book] was probably the first serious and rather successful attempt to put numbers on a more or less axiomatic basis.
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
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!
> 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 it was likely a mechanical discovery process, rather than any moment of particularly deep insight. (And I don't think this detracts from Church's brilliance at all!)
Their structural properties are similar to Peano's definition in terms of 0 and successor operation. ChatGPT does a pretty good job of spelling out the formal structural connection¹ but I doubt anyone knows how exactly he came up with the definition other than Church.
Yeah I've been meaning to send a request to Princeton's libraries with his notes but don't know what a good request looks like
The jump from "there is a successor operator" to "numbers take a successor operator" is interesting to me. I wonder if it was the first computer science-y "oh I can use this single thing for two things" moment! Obviously not the first in all of science/math/whatever but it's a very good idea
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.
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.
> Note that this material is here for reference and for sampling. Reading all of TBoS through this website is possible but not the intention. If you like the material and want to read the book conveniently then do buy either the latest hardcopy or e-version.
Unfortunately, I don’t think one can be linked given the author’s note.
Could this not be said for almost any computing system? I think "<x> is it's own worst enemy" has probably been said of everything from assembler to proof languages with hardware in-between.
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>
What you wrote makes me think more of the point free style
Related to this: does anyone know if there's any document that delves into how Church landed on Church numerals in particular? I get how they work, etc, but at least the papers I saw from him seem to just drop the definition out of thin air.
Were church numerals capturing some canonical representation of naturals in logic that was just known in the domain at the time? Are there any notes or the like that provide more insight?
> It is rather well-known, through Peano's own acknowledgement, that Peano […] made extensive use of Grassmann's work in his development of the axioms. It is not so well-known that Grassmann had essentially the characterization of the set of all integers, now customary in texts of modern algebra, that it forms an ordered integral domain in which each set of positive elements has a least member. […] [Grassmann's book] was probably the first serious and rather successful attempt to put numbers on a more or less axiomatic basis.
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
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!
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`.
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 it was likely a mechanical discovery process, rather than any moment of particularly deep insight. (And I don't think this detracts from Church's brilliance at all!)
¹https://chatgpt.com/share/693f575d-0824-8009-bdca-bf3440a195...
The jump from "there is a successor operator" to "numbers take a successor operator" is interesting to me. I wonder if it was the first computer science-y "oh I can use this single thing for two things" moment! Obviously not the first in all of science/math/whatever but it's a very good idea
Unfortunately, I don’t think one can be linked given the author’s note.
Images of text, even if it were a text size I'd be comfortable with, is something that just breaks how I read online.