Sign in to follow this  
  • entries
  • comments
  • views


Sign in to follow this  


ApochPiq, didnt work. I wrote it out in a language in which each letter consists of a unique infinite sequence of subletters : e.g. A = "aakak233343!23...". Nyaaa. :P

So it seems my last entry was liked. It was the first entry with > 0 replies in a while. So i think I will continue on the same trend for a bit. 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 generate OCaml 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 GBP40 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
Sign in to follow this  

1 Comment

Recommended Comments

Actually, you did no such thing. If you had actually written out/thought out the full infinite sequence, you would have required an infinite amount of time, and therefore you would not be here to write this entry. On the other hand, if each of your sequences was reducible to a single value (say, a limit, Taylor sum, etc.) then you would still be subject to my system.

So pffbtbbb [razz]

(Oh, good stuff in this entry, too, btw. I've been mucking around a bit with provable programs and such for the Epoch project; it's interesting stuff but hard to find good materials on outside of academia. I really need to renew my college library membership soon.)

Share this comment

Link to comment

Create an account or sign in to comment

You need to be a member in order to leave a comment

Create an account

Sign up for a new account in our community. It's easy!

Register a new account

Sign in

Already have an account? Sign in here.

Sign In Now