Planetary Hoppers is a space strategy game between several human players (current AI exists just to show how AI-API can be used). Every player takes control of a civilization and competes over control of known space (there are several options for victory conditions ranging from one player controlling all starting planets to cumulative scoring system where all planets are worth one point per round and where game is played for a fixed number of rounds). It is quite standard game of researching technology, building armies, making alliances and crushing opposition under Dodechadrium heel of your boot.
Somewhere in around the map (usually in the middle) there is a dodechaedron - strange planet with Dodechadrium - material that can be used to create technology yet unrivalled anywhere. Unluckily for populations of this quadrant there ain't enough for everybody so vicious war usually ensues that'll kill fleets in space and troops on planets even if otherwise everybody would have just agreed to live in peace (which just isn't very likely anyway).
Currently in normal games with random maps players start with single production planet and possibly couple other near planets under their control. Technology starts from level 1 on production planet and from level 0 everywhere else. Planets not under anyones control join empire of player whose fleet arrives there first, but after that planets are conquered either through shooting troops on planet with bombardment weapons or (more rarely) by dropping troops on planet from cargo holds of your fleet.
Resources can be transferred between planets by autotransfer which currently just costs percentage of transferred goods (which increases as distances increase) or by ships. Sometimes autotransfer if preferable over using cargo ships and sometimes some resource is so scarce that it is worth dedicating ship or two just moving it to production planets.
How come that all those budding empires start from the same situation? It is because of the Thargan Empire to which (nominally at least) all planets in this quadrant belong to and to which every culture ought to pay taxes. Finding the dodechaedron brought all those planets to same realization that it might be time to rebel against old empire and carve a new one from its carcass.
Playing planetary hoppers is quite nicely strategic endeavour as available resources and several quite viable strategies exists even though some units are stable favourites in most situations. Dodechadrium is used to research of level 7 and 8 technologies and to research of all misc technologies. Currently I plan to try out some strategies I haven't used before related to using cargo ships to transfer resources - and as somewhat related note I plan to code some more automation into use of ships that can be used if there is not en0ugh time for micromanagement.
2008-01-29
Writing is hard
I have had real difficulties with writing anything at all. A terrible version of a writer's block has taken over me - it affects writing code, doing math and even writing poetry. I've done almost nothing at all for a while now. Solution I came up with is hardly original, but I do hope it will help me with writing.
Simple solution is decreasing my inhibitions about writing so that at least I will write something every day and preferably I will try to write something in every language I can reasonably well write at all - which would mean writing in finnish, english (maybe swedish), Haskell and Scheme. Perhaps I will include Java, C/C++ and Coq to that list. Java because I am trying to write little helper functions to wonderful space strategy game called Planetary Hoppers. C/C++ because it's language I actually don't know very well and that I would like to toy with (especially with it's exceptions and unsafe commands and all that fun stuff). Coq would belong to that list just because it is language I am trying to learn at the moment, but I am lazy and I don't think SICP approach will be optimal for toying with coq. I will try to write about 1000 words about anything at all in any natural languages in that list and couple neat functions in any programming languages in that list every day. So that is that.
I am thinking about writing something about poker here as Michael Halila borrowed me couple of books about poker and I finally got around reading half of them (Dummies was very quick to read - I read it in about 5 hours. Sklansky seems like fun book so far). At the moment 7-card stud and texas hold'em are my favourite games.
Coming soon: Planetary Hoppers, Poker, random-stuff-that-I-like
Simple solution is decreasing my inhibitions about writing so that at least I will write something every day and preferably I will try to write something in every language I can reasonably well write at all - which would mean writing in finnish, english (maybe swedish), Haskell and Scheme. Perhaps I will include Java, C/C++ and Coq to that list. Java because I am trying to write little helper functions to wonderful space strategy game called Planetary Hoppers. C/C++ because it's language I actually don't know very well and that I would like to toy with (especially with it's exceptions and unsafe commands and all that fun stuff). Coq would belong to that list just because it is language I am trying to learn at the moment, but I am lazy and I don't think SICP approach will be optimal for toying with coq. I will try to write about 1000 words about anything at all in any natural languages in that list and couple neat functions in any programming languages in that list every day. So that is that.
I am thinking about writing something about poker here as Michael Halila borrowed me couple of books about poker and I finally got around reading half of them (Dummies was very quick to read - I read it in about 5 hours. Sklansky seems like fun book so far). At the moment 7-card stud and texas hold'em are my favourite games.
Coming soon: Planetary Hoppers, Poker, random-stuff-that-I-like
2008-01-15
The Coq proof assistant
I must admit that I really like the Coq - it's terrific tool that already feels rather nice even though I haven't got much experience with it. It can be used as a proof assistant in proving theorems in Calculus of inductive constructions and as a tool for building verified programs. I plan to explore its reach more completely in later posts after I've played with it more.
Here's example from the Coq's standard library:
This is pretty much normal way to define natural numbers as zero and its successors. In coq this means that we are defining this type called nat that nat is either O or successor of a nat. Inductive in the beginning means that this definition declares way to construct instances of this type - which in turn means that coq will produce nat_ind, nat_rec and nat_rect - way to do inductive statements and recursive operations on nats. Definition of predecessor function is very straightforward and theorem of every natural number being predecessor if its successor is also easy to read even if one might not know what simpl and reflexivity are - they are called tactics and proofs in coq are build from them.
The Coq tutorial was rather nice introduction if rather short and now my prime source of information about the Coq are its reference manual and standard library - both of which are rather readable and intresting even though I have just started learning coq. Other people have written about it much more elegantly, but since this is learning experience it doesn't really matter.
I must admit that the french can name things well - I mean what would be better name for a tool?
Here's example from the Coq's standard library:
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
Definition pred (n:nat) : nat := match n with
| O => 0
| S u => u
end.Theorem pred_Sn : forall n:nat, n = pred (S n).
Proof.
simpl; reflexivity.
Qed.
This is pretty much normal way to define natural numbers as zero and its successors. In coq this means that we are defining this type called nat that nat is either O or successor of a nat. Inductive in the beginning means that this definition declares way to construct instances of this type - which in turn means that coq will produce nat_ind, nat_rec and nat_rect - way to do inductive statements and recursive operations on nats. Definition of predecessor function is very straightforward and theorem of every natural number being predecessor if its successor is also easy to read even if one might not know what simpl and reflexivity are - they are called tactics and proofs in coq are build from them.
The Coq tutorial was rather nice introduction if rather short and now my prime source of information about the Coq are its reference manual and standard library - both of which are rather readable and intresting even though I have just started learning coq. Other people have written about it much more elegantly, but since this is learning experience it doesn't really matter.
I must admit that the french can name things well - I mean what would be better name for a tool?
2008-01-11
Coq and SICP
I feel like I don't have much to say most of the time - which is rather huge problem for a starting blogger. Easiest way out is of course to describe all wonderful thoughts that have crossed my mind during the day which would fill this blog easily enough - only problem is that I would prefer having something worth saying.
Now I do have something of a plan - I intend to read SICP again, but this time I will use Coq as language of implementation so that I learn to use Coq and its intresting extraction facility. In essence I will prove theorems about some types and use Coqs extraction command to produce Scheme code. Now I do expect this to be a little bit harder than what it was to read through SICP using Scheme or Haskell, but I expect it to teach me a lot about using Coq as specification tool and proof assistant.
SICP is my favorite CS-book, because of its clear approach to foundations of programming. It does have its critics (pdf) and HtDP seems to have advantage over it when taught in CS101 courses.
There's still a lot of doing left before I can claim any basic understanding of coq - which is very point of my SICP project.
Now I do have something of a plan - I intend to read SICP again, but this time I will use Coq as language of implementation so that I learn to use Coq and its intresting extraction facility. In essence I will prove theorems about some types and use Coqs extraction command to produce Scheme code. Now I do expect this to be a little bit harder than what it was to read through SICP using Scheme or Haskell, but I expect it to teach me a lot about using Coq as specification tool and proof assistant.
SICP is my favorite CS-book, because of its clear approach to foundations of programming. It does have its critics (pdf) and HtDP seems to have advantage over it when taught in CS101 courses.
There's still a lot of doing left before I can claim any basic understanding of coq - which is very point of my SICP project.
2007-12-27
First post
I'm blogging again! A another attempt to blog about pretty much everything. Blogging isn't clearly for me, but I am not ready to give up yet. While my other blog (http://sketsis.net/) is more serious and written in finnish this one will be more fun (to me). Hopefully this means I will write here at least something.
Subscribe to:
Posts (Atom)