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