Like several others I read GEB during my undergrad days. I recall attending a local CogSci roundtable to announce my achievement, which I then viewed as something of a right of passage. When I told a prof I had just read GEB he laughed and said, "Oh no you haven't. You've just started."
Why I Don't Love Gödel, Escher, Bach
331–340 of 348 posts
Re: Why I Don't Love Gödel, Escher, Bach
#332I think there are at least two groups of people here, completely talking past each other. This happens a lot on HN. The two big groups seem to be (1) people talking about enjoying popular science writing, and (2) technical practitioners talking about what they do. The only thing we maybe forget as a community is that (1) and (2) are different genres that don't overlap very much.
One group is trying to read GEB as a popular science book and saying, wow, it's an unusually good one. The dialogs are a nice rest from the technical stuff and probably convey something.
Another group is trying to read GEB as an introductory technical book and saying it's a mixed bag. The dialogs are a distraction from the technical stuff and sometimes don't convey enough.
Re: Why I Don't Love Gödel, Escher, Bach
#333Earlier quoted context omitted.
Sometimes when my girlfriend and I are laying in bed after a long day and just aren't quite ready to unplug and sleep, we take turns reading randomly selected sections from IAASL. There's a couple other books in the rotation, but it's a fun one. The mini theater of it becomes kind of self referential as we try to mess up how the other person feels about the reality being thrown at them. You really can't do that with…
You're a lucky person to have a partner who appreciates this!
Yeah I'm jealous too
Re: Why I Don't Love Gödel, Escher, Bach
#334Earlier quoted context omitted.
> India doesn't really have a Zen tradition, India certainly has meditative/yogic practices and it seems unlikely to me that some bits of these wouldn't have travelled from India to China along with Buddhism and Sanskritic vocabulary.
Yes, of course India has a deep history of meditation and yoga and etymology does show relationship, but it is incorrect to say that it means the same thing in that place, most especially because the Sanskrit word itself wasn't purely preserved, it was mutated into a native sounding Chinese and Japanese word that took on a new, specific connotation reflecting the practice that evolved there in China. A simple example…
I do know how semantic change works, yes. And your pudding example shows that borrowing (and phonological adaptation) is likely beside the point. Words can change their meaning (and generally do) even when speakers are staying in the same geographic location (e.g. Sanskrit lokaḥ "world" became the Hindi plural marker log).
But all of this seems somewhat irrelevant to me for the topic at hand. Buddhism has a long history in India before reaching China, including meditative/concentration. Obviously there were significant developments in China (and Japan) which make Zen Buddhism distinct, but it seems odd to ignore the Indian Buddhist base it's built upon.
Re: Why I Don't Love Gödel, Escher, Bach
#335Earlier quoted context omitted.
Yes, of course India has a deep history of meditation and yoga and etymology does show relationship, but it is incorrect to say that it means the same thing in that place, most especially because the Sanskrit word itself wasn't purely preserved, it was mutated into a native sounding Chinese and Japanese word that took on a new, specific connotation reflecting the practice that evolved there in China. A simple example…
I do know how semantic change works, yes. And your pudding example shows that borrowing (and phonological adaptation) is likely beside the point. Words can change their meaning (and generally do) even when speakers are staying in the same geographic location (e.g. Sanskrit lokaḥ "world" became the Hindi plural marker log ). But all of this seems somewhat irrelevant to me for the topic at hand. Buddhism has a long his…
I'm not ignoring its foundation in India, only affirming that what we know of as Zen was critically developed in China and Japan. American English has roots in Britain, but it's distinctly American.
Re: Why I Don't Love Gödel, Escher, Bach
#336From the classic MIT-AI Lab humor directory: AI:HUMOR;GEB REVIEW
(I'm including a copy for reference and archiving since the web server publishing this link is written in MACLISP running under ITS on a PDP-10 emulator.)
http://up.update.uu.se/DSK%3AHUMOR%3BGEB%20REVIEW
The following review of "Godel, Escher, Bach: An Eternal Golden Braid," Douglas R. Hofstadter, New York: Basic Books, appeared in "Fusion", Magazine of the Fusion Energy Foundation, Oct. 1979, pp. 61.
"Douglas Hofstadter, author of "Godel, Escher, Bach," has not had such a vaired experience with the antiscience movement as Bateson [Bateson, Gregory, "Mind and Nature--A Necessary Unity", preceding review in Fusion], but his brief career, nevertheless, is a clue to the message of his book.
Hofstadter is a computer expert in the field of artificial intelligence. This dismal discipline, which emanates from the Bertrand Russell-Karl Korsch networks, has been used primarily to develop brainwashing programs. Hofstadter claims to be part of his network through his close association with Marvin Minsky who, in turn, works closely with linguistician Noam Chomsky at the Massachusetts Institute of Technology. Politically these "artificial intelligence" academics link up to the Bateson circles through the various radical groups they mutually support.
Artificial intelligence is as nasty a discipline as its use in brainwashing implies. It is based on the premise that the operations of the human mind are essentially compatible with formal Aristotelian logic and thus can be replicated by a sufficiently complex computer.
......
Douglas Hofstadter's interminable driveling (777 pages) reiterates Bateson's point from the perspective on an attack on Kurt Godel's 1931 proof that any system determined by a fixed lawfulness (axiomatic login) is necessarily incomplete, hence incapable of solving problems that can be posed within its limits. The obvious conclusion to be reached from this proof is that there is a higher order of lawfulness (reason) that determines successive, reason-determined locally lawful systems. The British oligarchy never forgave Godel for this insight, which negate Bertrand Russell's attempted destruction of Georg Cantor's introduction of the concept of the transfinite into mathematics.
Hofstadter simultaneously slanders Godel and the musical genius Johann Sebasian Bach--whose recognition of the same principle in musical composition made Beethoven's subsequent breakthroughs possible--by lumping them with the psychotic Dutch draftsman M.C. Escher.
The paradoxes of formal logic, Hofstadter contends--for example, Epimenides's statement that all Cretans are liars--are really Zen koans. There is nothing new here that the eastern mystics and their systematized irrationality did not discover in bygone millennia. In fact, he says, the solution is to imbed simple axiomatic systems in more complex ones in regress. Once this is accomplished, presto, mind and the universe can be programmed into a computer.
(Reviewed by: John Schoonover)
Re: Why I Don't Love Gödel, Escher, Bach
#337Earlier quoted context omitted.
of course I do - I misspoke after I missed your reference to prime numbers in the list of open/hard problems. I get why you're including it, but if we're just deciding whether the program halts then "f(x: int) => x is prime ? halt : loop" is clearly resolvable to "doesn't always halt" so I don't see your point.
> if we're just deciding whether the program halts then "f(x: int) => x is prime ? halt : loop" is clearly resolvable to "doesn't always halt" Yes, that's right. But that was not your original example. Your original example was: f(x: int) => x is even ? f(x + 1) : halt which is a much more interesting case. But the real point (as I am now repeating for the third time) is that the halting problem is equivalent to prov…
yeah I'm aware that I'm trying to build a platform that proves arbitrary theorems. I think where we're butting heads is that I'm wanting to approach such a platform from a constructive angle - starting with simple axioms and building up from there. The initial system may only be capable of interpreting natural number equality and addition.
My original question was around what theoretical approach best matches that goal - whether it's an axiomatic system based on Peano arithmetic, or a natural deductive system, or something based on type theory. From a non-academic perspective these fields all seem very similar and there seems to be a lot of crossover so I didn't know what best suited the problem I'm trying to solve. Of course even when the system is complete some functions will remain undecidable, but I'm totally OK with that. It may even be that something like a deductive classifier better suits the problem than a mathematical representation.
Re: Why I Don't Love Gödel, Escher, Bach
#338Earlier quoted context omitted.
a dependent typing engine is exactly how I was thinking of representing this - i.e "x: int => x + 1" would have a type signature of "x: int => x + 1". Further compositions would stack. If I e.g. converted the Collatz conjecture to a function I would get the following signatures: - collatz(x: 1) => halt - collatz(x: int where x > 0 && x % 2 = 0) => collatz(x / 2) - collatz(x: int where x > 0 && x % 2 = 1) => collatz(x…
A dependently typed system (or presumably anything else) which allows non-halting definitions is unsound. The classic example is an infinite loop: loop = loop What is the type of `loop`? We can infer it by starting with a completely generic type variable, e.g. `forall t. t`: loop : forall t. t loop = loop Then we can look at the type of the body to see which constraints it must satisfy, and perform unification with t…
hey, just so you're aware I am working my way through your answer. I appreciate the depth of your comment and will be coming back to reply once I've fully understood your answer. I don't know how long it takes for HN to lock a thread for replies, but if you want to discuss this further would you mind dropping me an email (my address is in my profile)? It might take a couple more days for me to formulate a response.
Re: Why I Don't Love Gödel, Escher, Bach
#339Earlier quoted context omitted.
> if we're just deciding whether the program halts then "f(x: int) => x is prime ? halt : loop" is clearly resolvable to "doesn't always halt" Yes, that's right. But that was not your original example. Your original example was: f(x: int) => x is even ? f(x + 1) : halt which is a much more interesting case. But the real point (as I am now repeating for the third time) is that the halting problem is equivalent to prov…
yeah I'm aware that I'm trying to build a platform that proves arbitrary theorems. I think where we're butting heads is that I'm wanting to approach such a platform from a constructive angle - starting with simple axioms and building up from there. The initial system may only be capable of interpreting natural number equality and addition. My original question was around what theoretical approach best matches that go…
> I'm aware that I'm trying to build a platform that proves arbitrary theorems.
OK, well, that was far from clear. Here's your original question:
> the question that fascinates me is - what is the property of a program that makes it undecidable? I've been playing around with the idea of trying to make a program that determines halts/doesn't halt/don't know, given some representation of a program. I'm running into some interesting implications when I incorporate dependent typing, but it feels like there must be something theoretical that's already out there.
You're right, there is "something theoretical that's already out there", and that "something theoretical" is Turing-equivalence (and a vast literature on automated theorem proving).
> My original question was around what theoretical approach best matches that goal - whether it's an axiomatic system based on Peano arithmetic, or a natural deductive system, or something based on type theory. From a non-academic perspective these fields all seem very similar and there seems to be a lot of crossover so I didn't know what best suited the problem I'm trying to solve.
You're right. All of those fields are very similar. In fact, they are equivalent because they are all Turing-complete. It is really hard to avoid Turing-completeness, and even there all of the possible options are well understood.
The bottom line is that you (AFAICT) are at the very beginning of an extremely well-worn path. Actually, not just one path, but many, many paths, all of which lead to the same place: undecidability (and meta-undecidability and meta-meta-undecidability...) No on has found a breakthrough in these woods, and there are good reasons to believe there is none to be found (though of course that can't be proved because undecidability!) The best you can hope for is to make reasonable engineering tradeoffs that work for some domain of interest. But at the end of the day, you're just doing math, and math is hard. Nowadays it's really, really hard because all the low-lying fruit was picked a long, long time ago.
But if you're really serious about this, the first step is to get a stack of textbooks on computability theory and automated theorem proving and read them.
Re: Why I Don't Love Gödel, Escher, Bach
#340Earlier quoted context omitted.
yeah I'm aware that I'm trying to build a platform that proves arbitrary theorems. I think where we're butting heads is that I'm wanting to approach such a platform from a constructive angle - starting with simple axioms and building up from there. The initial system may only be capable of interpreting natural number equality and addition. My original question was around what theoretical approach best matches that go…
> I'm aware that I'm trying to build a platform that proves arbitrary theorems. OK, well, that was far from clear. Here's your original question: > the question that fascinates me is - what is the property of a program that makes it undecidable? I've been playing around with the idea of trying to make a program that determines halts/doesn't halt/don't know, given some representation of a program. I'm running into som…
> OK, well, that was far from clear. Here's your original question:
Yeah, sorry about that - not being an academic myself makes it hard to put it across in the correct way.
> No on has found a breakthrough in these woods, and there are good reasons to believe there is none to be found
That's absolutely fine by me - I'm not looking to break through the undecidability barrier, only to implement an algorithm that can prove theorems we already know are decidable (well, group functions into the always halts/doesn't always halt/undecidable categories).
The numerous branching and totally equivalent fields is the thing I'm wary of - I don't want to have to invest 6 months learning category theory, only to find out that what I want to do is better expressed by type theory or second order logic or something else entirely. I guess in my mind it's similar to building a complex application in one programming language just to discover certain patterns can't be idiomatically expressed in that language, so you have to write horrible hacks to compensate for that lacking where you could have chosen a different language in the first place. From my own research I'm leaning towards axiom systems, perhaps utilising Zermelo-Fraenkel set theory as a basis. I don't know, it's early days yet. I'll keep reading and get a rough grasp on the principal fields before I make a definitive decision.