Gödel, Escher, Bach Wiki
(a brief comparison of "good old-fashioned AI" and modern trends in AI)
Tag: Visual edit
(→‎Banishing Strange Loops (p. 21): mention the Curry-Howard correspondence, published in 1980)
Tag: Visual edit
(One intermediate revision by one other user not shown)
Line 57: Line 57:
 
=== Banishing Strange Loops (p. 21) ===
 
=== Banishing Strange Loops (p. 21) ===
 
Don't let Hofstadter's dismissal of type theory on p. 22 discourage you from learning about type theory. It's an active field of math that has been getting some exciting results recently, especially in its mind-bending new forms such as {{wikipedia|homotopy type theory}}.
 
Don't let Hofstadter's dismissal of type theory on p. 22 discourage you from learning about type theory. It's an active field of math that has been getting some exciting results recently, especially in its mind-bending new forms such as {{wikipedia|homotopy type theory}}.
  +
  +
We may have a considerably different perspective now. In fact, the {{wikipedia|Curry-Howard correspondence}} was first described in 1980, the year after GEB was written. This is an astonishing isomorphism between proofs and programs, between theorems and types. It's a lot like the kind of mathematical analogy that GEB thrives on.
   
 
Hofstadter does have a reason to dismiss type theory ''within GEB'', however, because the price of admission to type theory is that you have to ban all forms of self-reference, or even ''potential'' self-reference, no matter how indirect. Even Turing-complete programming languages break the rules.
 
Hofstadter does have a reason to dismiss type theory ''within GEB'', however, because the price of admission to type theory is that you have to ban all forms of self-reference, or even ''potential'' self-reference, no matter how indirect. Even Turing-complete programming languages break the rules.
Line 62: Line 64:
 
Type theory has given us interesting mathematically-inspired programming languages, such as {{wikipedia|Haskell}} (which has to break the rules sometimes), and interactive theorem provers, such as {{wikipedia|Coq}} and {{wikipedia|Agda}}. Within type theory, not only can computers verify your programs and your proofs, they can help you write them.
 
Type theory has given us interesting mathematically-inspired programming languages, such as {{wikipedia|Haskell}} (which has to break the rules sometimes), and interactive theorem provers, such as {{wikipedia|Coq}} and {{wikipedia|Agda}}. Within type theory, not only can computers verify your programs and your proofs, they can help you write them.
   
We may have a considerably different perspective now than in 1979. Type theory isn't as "extremely academic" as it once was, now that you can program with it. If Hofstadter were writing [[Metamagical Themas]] today, he might even overcome his distaste for type theory and end up talking about these languages with the same excitement he had in his articles about {{wikipedia|Lisp}}.
+
Type theory isn't as "extremely academic" as it once was, now that you can program with it. If Hofstadter were writing [[Metamagical Themas]] today, he might even overcome his distaste for type theory and end up talking about these languages with the same excitement he had in his articles about {{wikipedia|Lisp}}.
   
 
Still, there are things you can't do without self-reference, and several of them are key ideas in this book. it's clear that type theory isn't a good fit for the meta-mathematics in ''GEB''.
 
Still, there are things you can't do without self-reference, and several of them are key ideas in this book. it's clear that type theory isn't a good fit for the meta-mathematics in ''GEB''.
Line 107: Line 109:
 
:Here's a comparison I found too silly to include in the text above:
 
:Here's a comparison I found too silly to include in the text above:
 
:In the ''Scott Pilgrim'' series of graphic novels, vegans have superpowers, which they lose if they consume any animal products. In math, it seems like type theorists have superpowers, which they lose if they allow any kind of self-reference. And just like many people could never give up meat, Douglas Hofstadter could never give up meta. --[[User:Rspeer|Rspeer]]
 
:In the ''Scott Pilgrim'' series of graphic novels, vegans have superpowers, which they lose if they consume any animal products. In math, it seems like type theorists have superpowers, which they lose if they allow any kind of self-reference. And just like many people could never give up meat, Douglas Hofstadter could never give up meta. --[[User:Rspeer|Rspeer]]
  +
: The presence of that "''Author:''" provides the impetus for a very interesting exercise with the book: reading it twice in a row. This is particularly interesting when reading the [[Little Harmonic Labyrinth]]. --[[User:hacksoncode|hacksoncode]]

Revision as of 03:34, 23 December 2014

Overview

A Musico-Logical Offering

The book opens with the story of Bach’s Musical Offering. Bach made an impromptu visit to King Frederick the Great of Prussia, and was requested to improvise upon a theme presented by the King. His improvisations formed the basis of that great work. The Musical Offering and its story form a theme upon which I “improvise” throughout the book, thus making a sort of “Metamusical Offering”. Self-reference and its interplay between different levels in Bach are discussed; this leads to a discussion of parallel ideas in Escher’s drawings and then Gödel’s Theorem. A brief presentation of the history of logic and paradoxes is given as background for Gödel’s Theorem. This leads to mechanical reasoning and computers, and the debate about whether Artificial Intelligence is possible. I close with an explanation of the origins of the book – particularly the why and wherefore of the Dialogues. (p. viii)

Topics

The Introduction covers a large number of topics, very briefly, giving a taste of what the book is about. Each of these topics will be covered in greater detail later on.

Bach (p. 3)

Musical_Offering_-_The_Royal_Theme

Musical Offering - The Royal Theme

Frederick the Great asked Bach to improvise on this difficult theme.

The video to the right visualizes the Royal Theme, the melody that Frederick the Great asked Bach to improvise upon. Bach went beyond that, and made it the basis of his entire Musical Offering (BWV 1079), parts of which will appear throughout GEB. The Royal Theme is difficult to work with, including a long sequence of consecutive chromatic notes, and not exactly pleasant on its own, which makes it quite impressive that Bach was able to make a suite of good music out of it.

Something odd about the Musical Offering is that Bach seems to have designed it to be appreciated as sheet music first, and as an audible performance second. Bach never specifies what instruments should perform each piece, and many of the pieces within it are notated as puzzles. The tricks involving putting too many clefs on one staff, indicating that you play the same part multiple ways, aren't just an invention of GEB. This is how Bach really notated the music.

You can find the sheet music for the Musical Offering in various forms, both in Bach's original handwriting and in cleaned-up typesetting, on IMSLP. This PDF, for example, is Bach's manuscript for five of the canons plus one fugue.

Canons and Fugues (p. 8)

Canon_on_"Good_King_Wenceslas"

Canon on "Good King Wenceslas"

Hofstadter describes this canon by inversion at the top of p. 9.

At the top of page 9, Hofstadter uses "Good King Wenceslas" as an example of a canon, a musical piece where one part is an exact transformation of another part. The bottom part (in blue) mirrors the familiar melody (in green), but upside-down and two beats later.

An Endlessly Rising Canon (p. 10)

Bach_-_Musical_Offering_-_Endlessly_Rising_Canon_(Karl_Richter)

Bach - Musical Offering - Endlessly Rising Canon (Karl Richter)

Karl Richter conducts this performance of the "Endlessly Rising Canon", which in fact rises 6 times before ending.

The Musical Offering's "Canon 5 a 2", often called the "Endlessly Rising Canon", is a bit of a paradox in itself. How can a piece of music rise endlessly, when this means that eventually the notes will be too high for the instruments performing it? Any performance of this canon must end sometime, and most of them end after six repetitions. Because each repetition raises the pitch by a whole step, and six whole steps make an octave, six repetitions will bring the music back to its original key, but it's one octave higher. Some recordings repeat 12 times, ending two octaves higher with an overwhelmingly high-pitched sound.

The top voice performs the melody that's based on the Royal Theme, although it's in rearranged fragments.

A clever modern idea called the Shepard scale makes it possible to loop this music so that it "rises endlessly", without actually getting any higher in pitch in the long run. This appears much later in the book. If you're impatient, it's in Chapter 20, pages 717-719.

Escher (p. 10)

Escher - Print Gallery

Escher's "Print Gallery" (1956)

This section mentions Escher's "Print Gallery", which appears to the right.

What happens at the very center of this picture? Some geometry is too confusing even for Escher, so he covered it up with a white circle and his signature.

Recently, however, some mathematicians at Leiden University came up with a transformation of the plane that reproduces the self-engulfing effect that Escher drew. Now you can see what happens at the center. Be sure to zoom in! Escher and the Droste effect

Gödel (p. 15)

After introducing Epimenides' famous statement, "All Cretans are liars", Hofstadter quickly replaces it with the more straightforward statements "I am lying" and "This statement is false".

There's a good reason to do this: Epimenides' original statement is actually not much of a paradox! It could be described as confusing and self-defeating, and furthermore it could be described as false. This is different from the liar paradox, "This statement is false", which is paradoxical because it cannot be consistently called true or false. This difference catches even experienced mathematicians by surprise.

If you assert that the Epimenides statement is true, then you're agreeing that Epimenides is a liar and that his statement should therefore be false, which is a contradiction. Sounds just like the liar paradox, right? But it doesn't work the other way. The Epimenides statement can be false, because its negation is "It's not true that all Cretans are liars", or "Some Cretans are not liars", or "A Cretan has told the truth at some point". This is true [citation needed], so it is consistent to say that Epimenides' statement is false.

Epimenides may be a liar, but against all intuition, he's a logically consistent one.

See also: ➟ Liar paradox

Mathematical Logic: A Synopsis (p. 19)

On non-Euclidean geometry: "How could there be many different kinds of 'points' and 'lines' in one single reality? Today, the solution to the dilemma may be apparent, even to some nonmathematicians -- but at the time, the dilemma created havoc in mathematical circles."

Here's one way that the solution is apparent. ➟ Spherical geometry can be as much a part of our reality as Euclidean geometry is, even though most of Euclid's postulates don't apply to it. Perhaps it even has a better claim to the name "geometry", which after all originally meant "measuring the Earth".

The book will eventually cover more forms of non-Euclidean geometry, including some that happen to be used within Escher's drawings.

Banishing Strange Loops (p. 21)

Don't let Hofstadter's dismissal of type theory on p. 22 discourage you from learning about type theory. It's an active field of math that has been getting some exciting results recently, especially in its mind-bending new forms such as ➟ homotopy type theory.

We may have a considerably different perspective now. In fact, the ➟ Curry-Howard correspondence was first described in 1980, the year after GEB was written. This is an astonishing isomorphism between proofs and programs, between theorems and types. It's a lot like the kind of mathematical analogy that GEB thrives on.

Hofstadter does have a reason to dismiss type theory within GEB, however, because the price of admission to type theory is that you have to ban all forms of self-reference, or even potential self-reference, no matter how indirect. Even Turing-complete programming languages break the rules.

Type theory has given us interesting mathematically-inspired programming languages, such as ➟ Haskell (which has to break the rules sometimes), and interactive theorem provers, such as ➟ Coq and ➟ Agda. Within type theory, not only can computers verify your programs and your proofs, they can help you write them.

Type theory isn't as "extremely academic" as it once was, now that you can program with it. If Hofstadter were writing Metamagical Themas today, he might even overcome his distaste for type theory and end up talking about these languages with the same excitement he had in his articles about ➟ Lisp.

Still, there are things you can't do without self-reference, and several of them are key ideas in this book. it's clear that type theory isn't a good fit for the meta-mathematics in GEB.

Consistency, Completeness, Hilbert's Program (p. 23)

Babbage, Computers, Artificial Intelligence... (p. 24)

We're often going to have a very different perspective on AI than Hofstadter did when he was writing in 1979. For example, Hofstadter will write about chess as a difficult AI problem. Now computers are the undisputed champions of chess, and the way they got to be that good is so straightforward that we hardly even consider it AI anymore.

But GEB also describes things about AI that we still haven't accomplished, and still might.

The kind of AI described in GEB is a field we now call "good old-fashioned AI", or GOFAI. The name makes it seem quaint, and the field has largely been hibernating for decades. The problem with GOFAI is that it's really, really hard, and there are relatively easier ways to get results, including modern branches of AI that we give names such as "machine learning".

With machine learning, we can get computers to solve specific problems that might have seemed to require intelligence, such as sorting spam from non-spam e-mail, recognizing faces in images, and predicting what movies people will like. But this only solves part of the problem of making computers "intelligent".

Consider the list on p. 26 of things that computers should be able to do. Current trends in AI accomplish some of them:

  • to make sense out of ambiguous or contradictory messages
  • to recognize the relative importance of different elements of a situation
  • to find similarities between situations despite differences which may separate them
  • to draw distinctions between situations despite similarities which may link them

We might be accomplishing this one in some game AIs, but we could probably do a lot more:

  • to take advantage of fortuitous situations

And on some points, we're not much farther along than we were in 1979:

  • to respond to situations very flexibly
  • to synthesize new concepts by taking old concepts and putting them together in new ways
  • to come up with ideas which are novel

Sometimes an idea from GOFAI will re-surface, and become an idea that we use in modern practical AI. But GOFAI is still waiting for a breakthrough, and defeating many people who try it.

...and Bach (p. 27)

Gödel, Escher, Bach (p. 27)

Further reading

Easter eggs

Author (p. 3)
The first word in the book is easy to miss. It's "Author:".
This odd self-reference serves two purposes. One of them is to point out the level of dialogue that's "outside the system". He labels the lines that Tortoise and Achilles say with "Tortoise:" and "Achilles:", as that's the entirely traditional convention that tells you which character is saying them. He wouldn't normally be expected to label the entire book with "Author:", because you just assume that a non-fiction book is what the author is saying. But he does, probably because looking for assumptions that come from "outside the system" is a major theme in the book.
The other purpose is setting up for a payoff that will be delivered much, much later.

Commentary

(This section is for adding your thoughts about the chapter. Sign what you write with your user name. Others may edit this section for length later. More free-form, unedited discussion can take place in the comment section below.)

Banishing Strange Loops (p. 21)
Here's a comparison I found too silly to include in the text above:
In the Scott Pilgrim series of graphic novels, vegans have superpowers, which they lose if they consume any animal products. In math, it seems like type theorists have superpowers, which they lose if they allow any kind of self-reference. And just like many people could never give up meat, Douglas Hofstadter could never give up meta. --Rspeer
The presence of that "Author:" provides the impetus for a very interesting exercise with the book: reading it twice in a row. This is particularly interesting when reading the Little Harmonic Labyrinth. --hacksoncode