?

Log in

No account? Create an account

Glenn Willen

Previous Entry Share Next Entry
05:43 pm: ICFP contest entry the first
Welp, the 2010 ICFP contest happened. I was on team CBV (Cult of the Bound Variable) with a bunch of CMU grad students and otherwise CMU-affiliated people. We placed in the top 5, which is exciting; we won't know how we did beyond that until the ICFP happens and they announce the results.

My part in this included the following:
- Helping to decode the trit-strings. I didn't take part in this until we managed to get to the point of having the server's parser to query as an oracle; then I worked on it with jcreed, 8, and some other folks, and spent I think a couple hours on it before we got it.
- Writing lots of perl. In particular, I wrote the perl code that drives our Mathematica-and-AMPL based solver; it grabs a car, runs an SML program to get the matrices and output them as a Mathematica program, runs Mathematica to expand them into scalar equations in a format AMPL can work with, then runs AMPL on the result to try to solve it. The only really interesting part here was gross parsing, the ease of which impressed at least one teammate enough that he's talking about learning Perl. Mission accomplished. ;-)
- I played with a lot of matrix math; but this mostly ended up being for my own entertainment.
- I debugged some SML, in particular our car-with-fuel checker. Debugging SML is much easier with exception backtraces turned on, let me tell you. Also, I maintain that a function which takes the product of a list of matrices is Just Wrong if it throws an exception for the empty list, instead of producing an appropriate identity matrix... but making it take an int for size, which is what I did, is admittedly awkward.
- I probably did other stuff I was too tired to remember...

There are probably other interesting things I can say about the contest, but since I just wrote up documentation of the trit-encoding of cars, I wanted to write a basic post so that I could include it. Maybe more will come later; knowing me, probably not.

The following is copied from a blog comment.

"""
As regards the ternary encoding: I was one of the rare people who really enjoyed puzzling through it, and in hopes that I can convince you that the encoding did have an underlying neat organization, I will present to you the schema I worked out for it, written in pseudo-ML-datatypes. Note that the representation of the tuple (‘a * ‘b) is just the representation of ‘a, concatenated with the representation of ‘b.

car = chamber list (* No, we don’t know how to represent ‘a list yet… *)
chamber = tank list * bool * tank list
tank = nat
bool = nat (* restricted to 0 or 1, with 0 being true *)

Now here’s where it starts to get weird:

nat = trit list
trit = 0 | 1 | 2

So a nat is just a list of trits. But how is a list encoded? And how do you convert such a list into a numeric value? Tackling the second question first,

value([]) = 0
value([0]) = 1
value([1]) = 2
value([2]) = 3
value([0,0]) = 4
value([0,1]) = 5
… and so on.

Now, on to how lists are encoded.

EDIT: see below for a better way to do this part.

I will call the encoding of list lengths “wnat” for “weird nat”, since that’s how it looked to me at first.

wnat = 0 | 1 | 22 * nat

Where the numeric value of the wnat is 0, or 1, or the nat plus 2.

And now we represent a list of N elements as the wnat N followed by the elements concatenated together:

‘a list = N : wnat . ‘a ^ N

in very rough made-up notation.


EDIT: After comparing notes with someone in the #icfp-contest channel on Freenode, it seems most elegant to say that we represent lists as a zero (for the empty list), or a one followed by a single item (for a singleton list), or a 22 followed by a number N, followed by N+2 items (for all other lists). Thus:

'a list = 0 | 1 * 'a | 22 * N:nat * 'a ^ (N+2)

As compared to the struck-through encoding I give above, involving an extra type of nats, this one feels much simpler.
END OF EDIT

That together should be enough information to encode and decode cars, and to get a sense of why I, at least, think the encoding is actually pretty elegant.
"""

SON OF EDIT: per _adept_'s comment below, I had made an error, now fixed, by claiming 22N encoded a list of length N, when it is actually length N+2 (since 0 and 1 already have their own separate encodings.)

Comments

[User Picture]
From:175560
Date:June 22nd, 2010 05:33 am (UTC)

Congrats from team vorpal

(Link)
stereotype441 and I gave it a shot with two other Portland software guys. Despite me coming down with acute appendicitis on the day of the contest, the other three team members managed to get to 16th place without using any external software.

Unraveling the problem to its mathematical core by Saturday night was crucial, as was writing automated scripts that could scrape for cars, solve them, and submit solutions without intervention. Unfortunately, the solvers we were able to come up with on our own were not very sophisticated (especially compared to what you guys were doing), but fortunately, many teams submitted many cars that were not mathematically interesting. We solved over 2,000 cars using only 1x1 and 2x2 matrices.

Congratulations, CBV!
[User Picture]
From:stereotype441
Date:June 22nd, 2010 05:37 am (UTC)
(Link)
As regards the ternary encoding: I was one of the rare people who really enjoyed puzzling through it

I too enjoyed puzzling through the ternary encoding. I love doing that kind of detective work. When we figured out the natural number encoding

'a list = 0 | 1 * 'a | 22 * N:nat * 'a ^ N

jes5199 and I looked at each other and said "that is exactly the kind of encoding a functional programmer would choose".

Anyway, congratulations on doing so well. Being in the top five is a commendable feat. We didn't think of integrating with a 3rd party math package like Mathematica or AMPL. I can see why that would have made a huge difference in your score.

Paul (team vorpal)
[User Picture]
From:_adept_
Date:June 22nd, 2010 02:54 pm (UTC)
(Link)
Correction:
Length encoded after "22" is (number of elements in a list - 2). That is, 22{0} is a list of length (2+0).
[User Picture]
From:gwillen
Date:June 22nd, 2010 03:00 pm (UTC)
(Link)
Thanks, I have edited the post. I forgot the +2 when I was unrolling "wnat" into the definition of "list".
[User Picture]
From:gwillen
Date:June 26th, 2010 06:56 pm (UTC)
(Link)
Thanks! All credit goes to the people who did the actual work, I just did the perl hacking. ;-) I am glad we had someone on the team who knew how to apply Mathematica+AMPL to the problem, and had a copy handy. (And the AMPL company is letting us borrow a copy of the full version for free if we want to enter the termination competition with it.)

BTW, I can't remember how we LJ-met before -- was it a previous ICFP, or was it the MIT Mystery Hunt?
[User Picture]
From:gwillen
Date:June 26th, 2010 06:45 pm (UTC)
(Link)
Haha, very true.
Powered by LiveJournal.com