The curry-howard isomorphism gives you mapping between formal logic and programming language type systems. There are many different kinds of formal logic, all of which correspond to different type systems.
Logic is all about what you can prove, and so type systems based on logic are all about properties that you can prove about the programs that are typeable in that system. In particular, you're usually interested in 1) whether a program can be typed at all (i.e. whether it obeys the rules of the logic), and 2) what kinds of things you can say about typeable program (e.g. can it "go wrong" by, say, accessing a null pointer).
I'm wondering whether there's a similar isomorphism between something like number theory and type systems. Unlike logic, the point of number theory isn't so much about making sure you follow valid rules of inference. The point of number theory is more about encoding, and discovering, structure. As a simple example, I could imagine using multiplication of primes to represent cross products of types. If you did that, then what does it mean to say that factoring of primes is hard? Is that the same as saying that it's hard to automatically split a data structure into two orthogonal data structures with meaningful operations on them in isolation? In other words, that it's hard to come up with an automated meta-divide-and-conquer algorithm?
My question is whether there are useful insights from number theory that could be applied to programs. For example I just came across quadratic reciprocity. It's a truly strange theorem. If the components of the theorem (primes, squares, modular arithmetic, congruence) could be given a programming language interpretation, what would quadratic reciprocity mean in that interpretation?
This is the same kind of question as asking what gaussian elimination means in terms of a geometric interpretation.
It seems likely that a program interpretation of number theory wouldn't be like a type system at all. Maybe it would be about computable functions, or runtime complexity, or whether an algorithm can be automatically parallelized.
I only picked number theory for this example because 1) it seems concerned with structure and I like structure, and 2) there many many surprising results in it since it's been around for so long. I could equally well have picked differential equations, or topology.
Posted on March 7, 2006 09:40 PM
More languages articles
The Curry-Howard isomorphism has been extended into philosophy, see the links to Michael Dummet and Charles Stewart on Ontic, Epigram - Unifying Functions and Types. I wonder if this points to a convergence in formal logics? Even if they're all roughly equivalent, I wonder what tools or processes the philosophers, etc have discovered that can be ported to CS, or ported from CS to philosophy?
I've wondered about number theory as optimization of proof-derived programs.
I've always viewed category theory as the science of structure, though maybe group theory is more easily recognized as such. Maybe one solution is to describe software via category theory or group theory, and then generate executable code from that?
Here's one connection between number theory and programs: according to Matiyasevich's theorem, all recursively enumerable sets are Diophantine. This theorem therefore connects equations like x^2+y^2=z^2, with undecideable programs.
Posted by: Kim at March 13, 2006 01:01 PM