Random thoughts about logic, computability, etc that I was pondering tonight while in the shower.
Complexity theory is concerned with measuring the distance between two things, if you are restricted to purely constructive techniques for getting from one to the other. If a technique is constructive, then it means one problem is "reachable" from another, where the meaning of reachable is similar to pointers in a program, or functions, or physical connectivity.
Complexity classes correspond to the shape of the space over which we measure the distance between the question and the answer. Do different problems (addition, shortest path, traveling salesman, halting problem) define different spaces, or is there only one space and the different questions only correspond to different locales in that space? I think the latter, since all constructive solutions consist of a sequence of small steps, and small steps are simple. Or maybe the steps are merely given as black-box tools (axioms), and their simplicity is not measurable from the point of view of the constructive algorithm.
In geometric or topological terms, what does this space look like? Are there axioms which kink the space in interesting, boring, or dubious ways? Parametric polymorphism feels like it defines the meaning of congruent -- computations which are the same except for their position. What about shared state? What geometrical notion does it define?
Type theory is concerned with making sure the combination of techniques you use is legal. The concept of even being able to use techniques illegally is very strange to ponder. It's like requiring a babysitter to make sure that you don't misuse a glass of water by pouring it on the floor instead of drinking it. Do we need such chaperones merely because our brains are stupid meat, or is there a fundamental reason why maintaining soundness is hard?
Is there a difference between questions that have constructive solutions and those that don't? Is it possible to describe a formal logic that precisely delineates which of these two classes a question belongs to, even if it can't tell you how to construct a solution? That is, is there a constructive method that would prove the provability of a question, without actually coming up with the proof itself? Is it possible for that technique to be complete? Would it inherently depend on the axioms available, or not? Is the class of decidable questions the same as the class of questions that have constructive solutions? Does this entire paragraph have any meaning, or have I just poured my glass of water on the floor?
Here is the reason I'm interested in the ability to prove provability: If you are given a problem and asked to search for a program that solves that problem, is the search space finite? What is a productive way of laying out the space of all possible programs? Is there a (sufficiently interesting) language for describing requirements such that if a requirement is expressible in that language then a program satisfying the requirement must exist, even if it may take arbitrarily long to find it? Is there a way to characterize how complete such a requirements language is (e.g. what classes of programs is it capable/incapable of summoning)?
Posted on May 31, 2006 08:31 PM
More languages articles
The "space" of computability, as you call it, is a mathematical category.
One example is the category EN of numbered sets. (For those playing at home, I'm going from Asperti and Longo, section 2.2.) Objects in EN are pairs A = (a,e_a) where a is a countable set and e_a : N -> a is an onto map from the natural numbers to a. That is, it's an _enumeration_ of a.
There is a morphism f : A -> B if and only if, for some total recursive f', e_b o f' = f o e_a.
A principal morphism in this category is basically a classical "reduction" from one set to another. An isomorphism is a congruence.
This stuff is developed in Ershov's "Theorie der numerierungen", but I have no idea if there's a good text about it in English.
Posted by: Pseudonym at June 1, 2006 01:59 AMThanks for the pointers. Yet another reason to really learn category theory (so far I've made a few half-hearted attempts, and never really succeeded).
Posted by: Kim at June 1, 2006 06:11 PMhttp://en.wikipedia.org/wiki/Wikipedia:Articles_for_deletion/Dissident_Voice
(feel free to delete this comment of course since its totally off topic.)
My suggestion is to read Lawvere and Schanuel's "Conceptual Mathematics" first.
This makes the basic ideas of category theory accessible to a smart high school student. It's a very gentle book, and most importantly, it will give you a good introduction to the basic ideas and terminology. Once you've finished this book, you'll be able to handle the faster pace of a "real" maths book.
I say this because "real" maths books on category theory tend to go extremely fast over the simple stuff, so it's very easy to get lost in a lot of new terminology. (I certainly found it so.) And more to the point, there's a lot of interesting ideas in the simple stuff, so it's worth spending more than one chapter on it.
Posted by: Pseudonym at June 4, 2006 07:17 PM