Dmitry Astapov (_adept_) wrote,
Dmitry Astapov
_adept_

ICFPC-2020: To boldly go ... where?

This is part two of the ICFPC-2020 write up. Part one is here.

(reminder that our team name was Just No Pathfinding, for reasons that would be explained later)

One particular message from aliens, #38, was rather long and convoluted. It mentioned "encoding" and "decoding" primitives, and another function that earlier was tentatively named "send", so the consensus was that message was describing some way to communicate with aliens.

Message #38


Believe it or not, but it was eventually decoded to mean this:

let f38 protocol (flag, newState, data) = if flag == 0
                then (modem newState, multipledraw data)
                else interact protocol (modem newState) (send data)

let interact protocol state vector = f38 protocol (protocol state vector)



As you can see, crowdsourcing on Discord eventually hit a wall with helper function here, which ended up being named "f38" even in the official docs :)


So, this is a way to apply some hitherto unknown function called "protocol" to some "state" and "vector" and results will either have to be "drawn" or "sent" to aliens. Separately, there were alien messages to explain that "drawing" is just plotting points defined by (X, Y):

Message #32, Drawing.
It shows (draw 1 1), (draw 1 2), (draw 2 5), etc



Finally, the last message we had, #42, means "interact = ....", where meaning of "galaxy" was unknown:



As I mentioned in the previous part, Alex wrote decoder and I wrote encoder for the data according to alien "specs". The only data supported were integers (positive and negative) and cons-encoded lists, so that [1,2,3] will be written as (cons 1 (cons 2 (cons 3 nil))).

I also mentioned that organizers provided REST API that supported one method: "/alien/send". You could send an encoded list "to the aliens" and receive encoded data back.

So far, we knew that aliens will respond to '(0)' with '(1, 81744)', where the second number will decrement over time, and would respond to pretty much anything else with '(0)'

Overall, that looked like a clock that probably counts down to the contest end. We had no other ideas and feeble attempts to send other messages to aliens were soon abandoned.

They were abandoned because finally, at T+4.5 hours the long-awaited HUGE MESSAGE from space had arrived.

It contained a definition for the 'galaxy'!

galaxy = :1338
:1338 = ap ap c ap ap b c ap ap c ap ap b c :1342 :1328 :1336
:1328 = 0
:1342 = ap ap b ap c ap ap b b ap ap b s ap ap b c ap c :1343 ...
...


Ok, FINALLY: some clarity.

We do need an interpreter for this language.

We don't seem to need a decoder for alien pictures. And we definitely don't need to produce alien pictures.

And once we have an interpreter for the alien language, we could "interact galaxy", and hopefully something new will happen afterward. But first, we will need an interpreter.

Alien language was clearly based on Lambda Calculus: minimalistic computation formalism that has just three constructs:

  • Variables (and, in our case, numbers)
  • Application of the function to its arguments : (f arg1 arg2 arg3 ...)
  • Function definition (more formally called "lambda-abstraction"): (λx.BODY) or more conventionally (\x -> body) or (fun x -> body)


The alien language was even more minimalistic: they had a bunch of pre-defined functions like "add", "mul", "neg" etc, but no symbols for lambda abstraction (function definition).

So new functions were defined only via the composition of pre-defined functions given to us in alien images, which seemingly simplified things.

However, lambda-calculus itself is pretty far removed from anything that typical programmer encounters in the daily life, and due to its sheer simplicity, even most trivial things end up being quite obscure and non-intuitive (those who know lambda calculus could skip to the next occurrence of the word "ANYWAY").

For example, how do you define "true" and "false" in a language that has no built-in boolean type, and by default - no numbers? Well, OBVIOUSLY, you define them like this:

let true x y = x  (or λx. λy. x)
let false x y = y  (or  λx.  λy. y)


Because then, you see, you can define "and" like this:
and x y ifTrue ifFalse = x (y ifTrue ifFalse) ifFalse (or: λx.λy.λt.λf.x (y t f) f)


And will take two boolean values and two expressions to evaluate depending on the result of "and". You can check for yourself that supplying true/false values as defined above would yield expected results.

As you might imagine, things like lists, numbers, conditional execution, and conditional recursion require even more trickery due to the simplicity of the tools you have to work with. You can build higher-level primitives, and a good deal of theoretical articles explore the subject of what should those primitives be and what is the smallest number of them you need to have to semi-comfortably use lambda calculus for something resembling real-life computations. Those sets of primitives are called "combinator basis" as they allow you to build pretty much anything by combining lambdas.

Most famous basis is called S,K,I calculus, but there are others, for example B, C, K, W system.

We got "lucky" - alien messages described combinators S, K, I, B, and C and galaxy.txt used all of them.

ANYWAY, first attempt to write evaluator for galaxy.txt quickly displayed the tendency to go into endless loop, seemingly unable to deal with the value ":1141", one of the many recursive values to be found in galaxy.txt (here "ap" is a function application, (ap f x) is (f x)):

:1141 = ap ap c b ap ap s ap ap b c ap ap b ap b b ap eq 0 ap ap b ap c :1141 ap add -1



This was a clear sign that alien language has lazy evaluation semantics, where you don't rush to eagerly evaluate all the expressions that you have because some of them could be self-referential and you will end up expanding and evaluating them forever. Instead, you evaluate as little as necessary to compute the result.

Alex and I worked with languages with lazy evaluation in the past (Haskell, anyone?), but neither of us had any recent experience implementing a lazy lambda evaluator.

This quickly started to shape like our downfall. Our evaluator was alternating between something that loops forever and something that stops evaluating too early. Annoyingly, we had 80+ tests for the evaluator, mostly derived from alien images, and they seemed to pass all the time, even though galaxy.txt stubbornly refused to be evaluated. Attempts to reduce failures to something resembling minimal test cases failed, and attempts to produce more tests by hand just yielded tests that were always passing.

I tried to translate galaxy.txt to OCaml code so that we would not have to write our evaluator, but this turned out to be harder than I expected, plus we were not sure that there would not be more alien code incoming.

Time for my favorite ICFPC-related gif:



We had, probably, 4 to 6 different evaluator rewrites, until finally, I was ready to give up altogether. We even tried to use an existing library that implemented a lambda calculus evaluator, with little to no success. I vented my frustration in the chat with Alexey Shchepin, winner of several lightning rounds in the previous years, with whom we often get in touch during ICFPC (hi!), and he said that I probably messed up rules for cons/car/cdr (list construction and deconstruction), because people often get them wrong.

His crystal ball was right on the money and finally, we had evaluator that churned through galaxy.txt and emitter a list of numbers. Based on alien instructions, we should've had a list of number pairs (so we can plot them). Instead, I got a list of number pairs AND numbers. Obviously, there was a bug somewhere.

After reading and re-reading the code (which was tantalizingly small, almost too small to have a bug somewhere) I finally spotted "ifnil nil = false", which should've been "ifnil nil = true". Rookie mistake, easy fix. I swapped true to false, any evaluator promptly went into an infinite loop.

You know all these complaints about interview questions that focus on linked lists, and how nobody implements them in real life, because every language out there has native support for lists?

Well, I am here to tell you that linked lists are HARD. At least, when they are done using lambda calculus and should behave lazily (that is, you never evaluate more than fist element of the list until you consumed it).

It took us the longest time to realize that in our implementation lists either behaved as strict (that is, fully evaluated) and we ended up trying to evaluate infinite self-referential lists, or they had lazy semantics, and then at the end of the evaluation, we ended up with a partially-evaluated list of coordinates with just the first element ready.

We needed lazy lists, but once we had the final list of coordinates, we had to strictly evaluate all of it, "forcing" all its elements.

It is embarrassing to admit this after all my years of programming in Haskell, but otherwise, I would've had to write "and for the second day, we did absolutely nothing" :)

A rough timeline of the long slog towards evaluator:
T+5h: number encoder and decoder
T+6h: list encoder and decoder
T+7h: aborted attempt to convert galaxy.txt to OCaml
T+8h: parser for galaxy.txt
T+8.5h: we communicated with alien proxy (and, I think, scored the only point in the lightning round)
T+9h: the first buggy version of the evaluator
T+11h: organizers upload to youtube a series of three videos that explain what is a partial application, lazy evaluation, and common subexpression elimination - all in alien/galactic terms.
Somewhere here we slept
T+26h: evaluator finally works, but is very, very slow

While we were fighting with the evaluator, we missed this little gem of a message in the discord, which to my knowledge was not documented anywhere else:



Participant: alien proxy has method /aliens/{responceId}, but when are we supposed to use it?

Organizers: It's a part of our long-polling protocol - we don't know how long aliens would respond to us. You will receive responseId in Location header. I will write the docs for this. But you see - now aliens respond fast enough.



We would hit this in the next 24 hours and waste approximately 30 minutes scouring Discord for answers :( (As you can probably tell, web development is not my cup of tea)

Meanwhile, other people had other problems.

At T+7h, this exchange took place on discord:


Participant A: Is there a task description somewhere public, or is this only available to registered teams? I always enjoy reading the task description, even when I don't have the time to participate.

Participant B: the task: interact with UFO and score points by learning how to score points.
Sup dawg we heard you like ICFPC so we put ICFPC in your ICFPC so you can struggle while you struggle



At T+12h, we learned the new etymology for the word modem:


XXX: Hmm...I thought "modem" hinted at some sort of transmission but according to the discord history it just means "modulate -> demodulate" :/

YYY: the word "modem" in real life means modulator/demodulator

ZZZ: My girlfriend guessed "modern data ejaculation machine" and imho that was pretty close and way funnier



Sooner or later everyone was hit by the infinite loop:

so how long did the program run for you guys
mine hasnt crashed yet, so something must be working
kinda hard to know tho
(5 minutes later) ok nevermind thats definitely wrong


At T+19h, when it was 6 am in the organizers time zone, people were incredulous that "Ivan Zaitsev" is still awake and on Discord, so he had to post a "proof of life":




While we were busy working on the interpreter, two teams seemingly took the lead in the lightning round (and as it turned out, there were only 5 teams to score more than 2 points in the lightning round) and were posting pretty pictures:

https://twitter.com/icfpcontest2020/status/1284413782937280512





At this point, we realized that our evaluator uses 63-bit ints, and galaxy.txt contains numbers that don't fit in 63 bits, so we had to add Big_int into our code, and add some rudimentary UI to plot the set of points returned by "interact galaxy".

We also realized that we don't do a common subexpression evaluation for S combinator properly, so our evaluator is very very slow, and we tried to speed it up, which took way longer than expected.

Finally, at T+35h, we executed "interact galaxy", received two sets on points, plotted them on the same image in two different colors and saw this:



This is an alien glyph for 0, followed by a galaxy symbol.

To be continued here.
This entry was originally posted at https://dastapov.dreamwidth.org/132037.html. Please comment there using OpenID.
Tags: #38believe, icfpc
Subscribe

Comments for this post were disabled by the author