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 PMUgg
Ugg Boots
Cheap Ugg
New Ugg Boots
Ugg Boot
Ugg Classic Boots
Cheap Ugg Boots
Uggs on sale
Uggs
Ugg Boots
Cheap Ugg Boots
Ugg Classic Boots
Ugg Boots Sale
Supra Shoes
Mens Supra Cruizer Shoes ---Special
Men's Supra Cruizer Red Shoes
Mens Supra Cruizer Cool Shoes
Mens Supra Cruizer Shoes --Charming
Mens Supra Cruizer Pure black Shoes
Mens Supra Cruizer Shoes --Leisure
Man's Supra Cruizer Shoes
Men's Supra Muska Skytop Shoes
Men's Supra Skateboarding Shoes
Men's Supra Strapped Shoes
Men's Supra Suprano High Shoes
Women's Supra Muska Skytop Shoes
cheap ugg boots sale
uggs classic mini sale
UGG Ultra Tall Boots
Cheap Ugg Boots
UGG Classic Tall Boots
UGG Classic Cardy
UGG Classic Short Boots
UGG Bailey Button bootsis a new style in 2009.The classic cardy uggs boots is another hot boots that worth of buying.And the classic tall ugg boots will make your winter amusing.And now uggs on sale,if you are looking for such a boot,the ugg boots is good choice this year.
Posted by: uggs on sale at November 17, 2009 08:31 PMUggs on sale now.Classic cardy boots ugg is a special boot that makes you different from the other girls.And the Bailey Button UGGs is hot in 2009.If you want to get a warm shoe in cold winter,I think ugg classic tall boots is a good choice for you.
Posted by: ugg classic cardy boots at November 17, 2009 08:59 PMwww.enjoywholesale.com
china wholesale clothing,china wholesale shoes,china wholesale electronics,china wholesale suppliers,china manufacturers
china wholesale products,light in the box,wholesale lots,wholesale ipod
china direct,china dropship,china trade,made in china
electronics wholesaler,ebay wholesaler,financial wholesaler
fashion wholesaler,clothing wholesaler,wholesaler magazine
computer wholesaler,external wholesaler,dvd wholesaler,wholesaler definition,china wholesaler,mutual fund wholesaler,define wholesaler,insurance wholesaler
discount ugg boots
forture
ugg boots
Discount store
Supra Shoes
Supra Skytop Shoes
Supra Society
Supra Thunder
Supra Suprano Hi
Supra Strapped
Supra Trinity
Supra Skylow 1.5
Supra Dixon
Diablo 1.5
Supra Cruizer
Supra Vaider Shoes
Supra Cuban
We are the best online sales for the china wholesale . Here you can have a large of choices of kinds Ugg Boots,Converse Shoes,Timberland Boots,puma shoes,Nike Shox Shoes ,Nike Dunk SB Shoes,Nike Air Max，Links Of London,Tiffany Jewelry,Dior Handbags?,jimmy choo handbags ,Cartier Watches, 8GB Mp4 Players,Bluetooth Car DVDs. All our cheap online cheap goods are high quality and original packages, and best service. We offer our customers the best service, 7 days arrive at your door.Enjoy your easy and happy shopping with us.
Nike Men's AF1 Light-up Shoes
light up air force
light up mens shoes
air force lights-up
light up shoes mens
light up air force ones
light up air force
air force lights-up
light up shoes af1
discount nike air yeezy
china wholesale online
discount ugg boots
nike free shoes
furture
ugg boots
Discount store
Laptop Battery Laptop Battery Laptop Batteries
Laptop Batteries discount laptop battery
discount laptop battery
notebook battery notebook battery
computer battery computer battery
replacement laptop battery replacement laptop battery
notebook batteries notebook batteries
rongTiffany Jewelry Online - Discount Tiffany & Co Jewelry On Sale
Hot Sell Tiffany Jewelry - Tiffany Jewelry Online
Return To Tiffany Double Heart Detachable Pendant Necklace - Tiffany Jewelry Online
Tiffany&Co 1837 Titanium I.D. Bracelet - Tiffany Jewelry Online
Tiffany & Co Bead Bracelet - Tiffany Jewelry Online
Tiffany&Co Atlas Round Pendant Necklace - Tiffany Jewelry Online
Tiffany&Co Bar Pendant Necklace - Tiffany Jewelry Online
Tiffany&Co Bead Necklace(N242) - Tiffany Jewelry Online
Tiffany&Co Bean Pendant Necklace(N157) - Tiffany Jewelry Online
Tiffany&Co Elsa Peretti Apple Pendant Necklace - Tiffany Jewelry Online
Tiffany&Co Butterfly Pendant Necklace - Tiffany Jewelry Online
People all over the world know the abercrombie and fitch,but not everyone really knows how fashion the abercrombie is,hollister is the Legend maker. Everybody wears the hollister clothing would be the abercrombie mens and the abercrombie womens, if you want know you can search the Ruehl No.925 or abercrombie outlet in the www.google.com .
Posted by: fitch at November 25, 2009 10:07 PMChina Electronics Wholesale China
Phone Cheap Cell Phones
href="http://www.thechinaphone.com/index.php?main_page=advanced_search_result&keyword=China%20Wholesale">China Wholesale
replica handbags
Louis Vuitton Replica
Louis Vuitton handbags
fake Louis Vuitton bags
fake Louis Vuitton
replica rolex
replica rolex
fake rolex
buy cheap fake rolex
rolex Submariner
Just wanted to say great job with the blog, today is my first visit here and I’ve enjoyed reading your posts so far
ugg bailey button
Wow, my ugg classic mini will not be coming off now! I’ve had them on for 12hrs strait and I do not want to take them off. Thanks for everything, well worth the wait.
replica watch
Rolex Sea-Dweller watch for sale
Rolex Submariner watch for sale
replica Panerai
Maurice Lacroix replica
Tiffany & Co. Cuff Bangle
replica watch
Rolex Sea-Dweller watch for sale
Rolex Submariner watch for sale
replica Panerai
Maurice Lacroix replica
Tiffany & Co. Cuff Bangle
replica watches
oris watches
replica Montblanc
Maurice Lacroix watches
U-boat replica
replica Audemars Piguet