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. :

Quote:


Section Tr.
Variable A B C: Prop.Lemma d_a : A -> B /\ C -> (A -> B) /\ (A -> C).
split.
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.
assumption.

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

Advertisements




Mathematical Landscapes

14 06 2006

How will this project turn out?

So I been talking about the game being based on logic and involving theorem proving in a limited sense. But how to do this? Well the general idea was to create a simple formal system and then figure out a way to port the system to a graphical logic representation. The methodology I am thinking of following is that laid out in this paper. This would be for spell creation of which there will be two types. General spells and creation of planes. Spells will be first implemented and it will be my first experimentation of this concept. Spells will be based on my simple formal system and there will be a mapping of theorems to spell aspects and will be a way to get my feet wet for the proper hardcore aspect of the project.

The other type, planes, allow one to map theorems and properties to textures, landscape creatures of an area… You may create a mapping for the system yourself or simply use the default one I provide. The logics backend will be implemented in F# and require F# assemblies, so there will be no Domain specific language. Different logics will allow different directions of exploration, for example, with modal logic we explore concepts of existance and possibility.

The premise itself is very simple, if you map the mathematical structures and object to more farmiliar things, drop down a level an abstraction by entering another, you will be able to enter realms of thought once too difficult to penertrate. In my head i have a dream, The plane, based on your mapping could represent a theorem on the reals. By setting off an explosion or jumping and watching the results you can gain insight into what to do…

Ill have to buck up on my graph theory, combinatorics and graphical logic concpets though.

sys.jpg

Instead of defining behaviour and maps explicity we create in a world whose final output is not known to us. It would be truly like exploring a mathematical landscape, a step towards mathematical visualization..





Why my favourite Language is .NET

31 05 2006

I quite like Microsoft's .NET initiative. And not simply because it further abstracts one from the hardware and ensures any application you write will work on all hardware, all OS's, which have the framework implemented. No, that is only a small bonus. The real great aspect of .NET is its Common Language Specification and the perfect interoperatability between all languages which meet the CLS – are .NET compliant. The fact that all languages compile/produce IL files that are basically the same, regardless of language of choice makes the case much stronger. This freedom, this flexibility, this ability to use what language fits your needs and mix and match strengths and counter weaknesses from this and that language is what I feel is .NET's greatest attribute.

For example, I am using C#, F# and IronPython for my project. Each for a specific reason. C# is what the core engine is in, the language is quite clean..at least when compared to C++. It arguably generates the fastest code of all the .NET languages and is the main Microsoft language, it would seem. I use IronPython to script the application, this is because python is a far more flexible language than C# and is more intuitive. It is also simple but in a manner which allows complex behaviour – using this as a script will allow things to be done that would not have been easy any other way. F# is used to code certain things that would not make sense in anything but a functional language. This functionality is exported as assemblies to be used by the C# app. Specifically, a simple implementation of Metamath to allow for exploration of meta-mathematical concepts in a pretty visual and innocent setting. Takes in scripts as well. A modal logic interface will be built on top of this and will control the behaviour of certain aspects to do with planes and magic etc. Again, I am wrapping some pure maths in the guise of a game. I hope. hehe. Nonetheless this freedom, the ability to not be restricted to any one language is in my mind the greatest offering of .NET. Just take a look at the number of languages available for the platform which can be made to operate with each other with little to no effort.

Why there can be no One Perfect Language

All programming language, all computers, computers running programs by a certain language are all essentially formal systems. This feature allows us to discuss things and apply things and proofs from logic on the capabilities of languages.

Formal System

In the most basic sense, a formal system is a system of logic that allows us to "reason" mechanically. A formal system is composed of:

  • an alphabet: symbols which compose its language e.g. {P,q, – }
  • a syntax which describes how to form a proper expression in the system. Formally called well formed formulae
  • A formal language, valid strings formed with our alphabet
  • Rules of inference – series of operations we perform on our sentences (strings of symbols from our alphabet e.g. pq–p) that end in something which is true in our system
  • and some starting wffs or Axioms.

A theorem in our system is a list of sentences with the first being an axiom or a proven wff (theorem) and every sentence within being a result of transformations which follow our rules – the last sentence in our string is a theorem.

Formal Language

A formal language is in the most basic sense a set of strings over some alphabet or rather, a proper subset of the set of all possible strings that may be composed with some alphabet, with an alphabet being no more than a set of symbols. Formal languages are devoid of ambiguities common to natural languages as English or Chinese (in fact there is no inherent meaning to the set of string or sentences formed in them), they are mechanically manipulable. That is, a computer can follow instructions formed in them. They were originally developed with formal logics and the wish to make math completely mechanized and in essence, air tight. All programming languages contain formal languages. In fact the term programming language is a misnomer since most programming languages are more than just languages. They are entire systems, indeed the term computer programming system would be more appropriate than computer programming language. This argument for this will be given informally later.

Should have known that no machine could replace a pup named Scooby Doo

Computers can be represented as formal systems, programming languages can be said to generate or represent rules of inferences which control the computer's state. This state may be considered sentences in the computer formal system with the act of following wffs represented by computer code transforming sentences to generate a theorem in the machine’s formal system. Indeed an operating computers actions is analogous to proving theorems in its formal system. Programming languages and computers in principle contain "within" the entirety of current mathematics. Converesly, they are tightly bound by the limits on formal systems based on their very nature.

Can the brain be considered a formal system? There are those who argue using Godel's Incompleteness Theories and similar mechanisms (Lucas , Penrose) that the brain is more than a computing machine. Indeed, no finite machine could ever hope to replicate human brains since for one, such a machine would have unprovable propositions contained within that the human brain it was supposed to emulate could. For another it is almost certain (since nothing can be certain) that the human engages in activity in the mathematic endeavour that is not limited to computable functions. Interestingly, if this is true then the Church Turing thesis – any evaluatable function can be computed by an algorithm on some computer is wrong, since we would have an example of a set of "mechanical operations" or more appropriately an algorithim that other machines could not compute. Conversely, if you feel the Church Turing thesis must be true and that the human brain can be represented by a [finite] computing machine then it is necessary that you accept the corollary (assuming consistency) that the human brain can never understand itself, there will be lines of "thought" that it simply will never be able to get to. Nonetheless such arguments for and against the human brain as a machine assume the consistency of the humans brain logical operation (note the use of consistency) and that a list of axioms may be attachable to it. The truth or untruth of this is an issue of debate, one which will not be gotten into in this post, although I do think the human brain to be more than a computing machine.

Why there can be no Perfect Language

One can show that Gödel’s theorems apply to computer languages and thus that no computer languages can ever show itself to be consistent nor are they complete in the sense that every statement in their system is decidable. Gödel’s theorems apply only to formal systems which have axioms that are fairly strong and interesting, in order words they can *encode* some representation of the natural numbers {1, 2, 3, 4, 5, …}. Every computer language that is Turing complete can do any anything that a Turing machine can do. Turing machines can arguably evaluate any computable function as can the lambda calculus (although as mentioned earlier, this statement is untrue if you like me, believe that the human brain is more than a mere computer), an equivalent but different formalism, The natural numbers are definable with the lambda calculus. Thus any Turing complete computer language is powerful enough to define the naturals.

As stated before, programming languages are actually formal systems with wffs (the syntax), alphabet, vocabulary and rules of inferences with the computer state actually being the sentences and the “computer code” being the transformations on the previous list of theorems and axioms (previous computer state) of the formal system. The computer code represents some range of the valid behaviour or transformations of our system. Thus every language coupled with the computer represents a different formal system. Godel’s second incompleteness theorem does not concern us. But the first one is of great relevance. It guarantees that our system will be incomplete and will never be complete. Every new axiom will add, every new feature or behaviour will always allow another new undecidable behaviour to crop up. In programming terms this boils down into the fact that every language will have unreachable portions, states, behaviour. That is there will be things that the computer language will never be able to do. No one language will ever be made capable of doing "everything" at least not while remaining consistent and not convoluted. There will be behaviour that our computer may be able to evince but our language will not allow us to invoke.

This is basically a very elaborate argument for the fact that no programming language can have or will ever have everything and be perfect. As such the .NET and its CLS are the perfect solution around this limitation and the closest one can ever get to a perfect language.