Numbers + Programs as Proofs

18 07 2006

I wanna cover things many people take for granted from an angle they are not used to. For example, I used to think vectors are directed line segments. Then i thought of them as members of an abstract vector space. Neither of these are correct because they both are…I plan to cover this by going over equivalence classes in a geometry in very clear english that requires no background in math beyond knowing how to count and basic geometry.

I also plan to continue by constructing the integers, rationals and then the reals. Go over interesting numbers like the “Number of Infinite Knowledge” and Unaccessible numbers and how to construct a number that cannot be constructed. And finally the hyperreals, which if youll notice I am trying to write on..they are quite useful for calculus.

I also hope to be motivated enough to cover the surreal numbers (drop back from hyperreals and extend reals with surreals), p-adic numbers (drop back to rationals and complete the rationals in a new way) and a new method i just read about which constructs a system isomorphic (equivallent) to the reals but skips the rationals and proceeds directly from the integers in its construction.
Numbers, numbers , numbers!!

_                ----->  "Eudoxus" numbers equivalent to reals
Naturals --> Integers --> Rationals --> Reals --> Complex
                               |          |
                               |          |====>Hyperreals  <- both contain infinitesimals and infinite numbers
                               |          |===> Surreals
                               |---> p-adic

Programs as Proofs

In other news Im learning Coq, where you construct maths much the same way you write programs. In essence you are programming math theorems. Not only that, your mathematical proofs are guranteed to be logically correct and perfect if they are verified sucessfully (compile properly). This is a major bonus for peer review since they just need to briefly look over your proof (code) to make sure you didnt cheat in definitions (stuff like that) as opposesed to the weeks to sometimes months it takes now. I like this because I have always been enamored of Intuitionsitic logics and constructivism (which applies in this case).

Thanks to this Ive been learning alot about type theory and constructive logics so Im understanding alot of what those people in the Software engineering forums are saying more and more! Further on, thanks to curry-howard isomorphism your programs are identical to proofs. That means that you can write programs as a proof and Coq will extract OCaml (or scheme or haskell) code. Now, not only will your algorithim be guranteed to be syntatically correct, it will also be logically correct. Not only that, the Coq environment is a proof assister and can actually help you out and auto prove simple sections. And because you are working at a very highlevel with incredibly rich mathematical types, the going is just unimaginably fast (im talking many magnitudes here). Imagine it..proving your complete scenegraph in less than an hour (or more dependending on your skills) vs. implementing it in C++. Ill be sure to go over my experience. My first pet project may be a simple matrix library extracted to Ocaml which should work in F# too. I plan to take adavantage of this isomorphism extensively with my main project, prolly improve my effieciency by at least a factor of 20 :D. Hopefully I make up the time im losing learning this.

The only thing about Coq is that there is very little documentation on it. The only book on it costs £40 and there is only 1 tutorial on it on the entire internet. So im mostly having to learn off the reference manual and developments in its standard library. Its tough and slow going.

Some n00b proofs from a tutorial im following. One proves a simple proposition and the other proves that a transitive and symmetric relation is reflective. :


Section Tr.
Variable A B C: Prop.Lemma d_a : A -> B /\ C -> (A -> B) /\ (A -> C).
elim H0.intros. exact H1. elim H0. intros. exact H2. Qed.

Require Import utf8.
Section rr.

Variable A B: Set.

Variable f: A -> B.
Variable D: Set. Variable R : D -> D -> Prop.

Section R_sym_trans.
Hypothesis R_sym : ∀x y:D, R x y → R y x.
Hypothesis R_trans : ∀x y z:D, R x y → R y z→ R x z.

Lemma refl: ∀x:D, (∃y, R x y) → R x x.
intros. elim H.intros. apply R_trans with x0. assumption. apply R_sym.

Also check out this link which contains lots of interesting interviews with great people. Lots of stuff to learn from there People’s Archive




Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: