Bubbles_glow

≡ Literary Systems ≡

 
Corner_fold
  • Citation
  • Extension
  • Response
  • Comment
Hopo_catalog
 
Flowchart_grey_24

Going Meta in Formal Systems

If this essay is going to be successful in convincing you that it's a useful practice to study code as literature, then we're going to have to address one of the fundamental breaks between programming languages and natural languages: their relationship to paradox. English has no difficulty with speaking of impossible things. I can simply say, "I am lying," a statement about which it is impossible to evaluate on the grounds of being true or false. If it's true, we think, then he's lying, so he's lying, which means he's telling the truth, so he can't possibly be truthful. And at about that point, we stop, satisfied at the recognition of a paradox. Novels introduce subtle paradoxes and ambiguities at many points, often in the service of character development. They range from Holden Caulfield's petty misdirections to Faulkner's truly unsettling habit of having characters mention things that they could not possibly have experienced.

With code, such inconsistencies, being logically impossible, are simply unable to be expressed by the language. Programming languages are examples of formal systems, so called because their stiff (prim, proper) rules forbid any such impossibilities. The dream of formal systems, especially for researchers at the start of the past century, was to create a complete and consistent formal system. Complete in the sense of being able to express every logical truth that exists, that there would be nothing true that the system was incapable of representing. Consistency meant that the system would have to be logically sound, keeping impossibilities and paradoxes well outside. There have even been dreams of extending the rule of formal systems to human thought: Gottfried Leibniz dreamed of assigning a number to every concept, and then resolving philosophical issues by manipulating these numbers within a formal system.

One of the most serious attempts to create such a complete and consistent system was made by the philosopher and mathematician Bertrand Russel, in his Principia Mathematica. Russell had recently come up with a major paradox in Set Theory, by proposing the existence of a set whose members were the sets that are not members of themselves. If you try to follow it's logic, it's another infinite loop: if the set does not include itself, then it must, if it must then it can't possibly. Russell (correctly) determined that the problem with paradox in formal systems is self-reference. If a system starts to talk about itself, then paradoxes come easy — note the form of the earlier English paradox, "I am lying." So Russell's Principia was specially designed to keep self-reference out of formal systems. He intended to do this by establishing a hierarchy of types (a potentially infinite one), and at each level, you were only allowed to refer to the types of the level beneath you. This theory of types turned out to be little more than a Maginot Line against self-reference.

The man who neatly side-stepped it was Kurt Gödel, and he did so at the tender age of 25 with his incompleteness theorem. Gödel attacked the Principia by proving that inside of every sufficiently powerful formal system, once can encode the equivalent of the statement: "This statement cannot be proven by use of this system!" Because of the manner in which the statement is encoded, the system must validate it as true, or else fall into inconsistency. If the statement is indeed true, then the system cannot prove it, which demonstrates that an unprovable truth exists, and that the system must necessarily be incomplete. This works on any formal system that is powerful enough to describe basic arithmetic. A beautiful result — it's not the weak systems that fall vulnerable to paradox, but the strong ones. It's the very strength of the Principia Mathematica that makes it vulnerable to the Incompleteness Theorem.

Perhaps because self-referentiality is both the official nemesis and inescapable fate of formal systems, the literary qualities of these formal texts are often wrapped in it. For the reader of proofs, theorems, and code, the meaning is less locked in the mechanical necessities of the surface math, and more in the meta-level ideas about the significance and consequences of what the code might do. As programming languages develop, an ever increasing number are beginning to use meta-programming techniques, where your explicit intent for the shape of the actual code becomes written into the meta-code itself. Naturally, as the meta-level capabilities of a programming language increase, and the text develops tangles of self-reference, the code itself becomes less tractable mathematically, less formal, less certain.




 
However, every programming language, no matter how rudimentary, has limits on its mathematical tractability. Curiously enough, the fundamental limits are the same as (or directly analogous to) the limits that Gödel's theorems place on formal systems. In Computer Science, this limit is known as the halting problem, and the effort to define it led to the definition of what computation really is.

In order to demonstrate the halting problem, Alan Turing had to invent a conceptual machine that could solve any computable problem:

The Universal Turing Machine . . .
Contains a finite repertoire of symbols.
Has a potentially infinite tape to store and read those symbols.
Has a device which can erase the symbols from the tape.
Has a device which can read symbols from and write symbols onto the tape.
Can move the tape forwards or backwards.
Maintains an internal state table, which defines the next action that the machine will take.
Has a control unit, which is capable of identifying the symbols and applying them.

Turing used this (at the time theoretical) machine to prove that one could never tell, formally, if a given computer program would ever finish execution, or if it would loop endlessly. The proof that he developed to demonstrate this is a direct relative of Gödel's. It's another delicious argument that consumes itself: Imagine a program, H, that could solve the halting problem by telling you, given the source to another program, if it would halt or not. The way to prove that H is impossible is the following: Create a second program P, which takes no input, feeds its own source code to H, and then does the opposite of what H predicts it should do. If H says that it will halt, it loops forever. If H says that it will loop, it halts. This program P must necessarily break H, proving that H cannot exist.