Log in

No account? Create an account
Lindsey Kuper [entries|archive|friends|userinfo]
Lindsey Kuper

[ website | composition.al ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Some victories [Aug. 12th, 2014|07:07 pm]
Lindsey Kuper

In the last two days:

  • I sent a draft of my dissertation to my committee! There are some parts that aren't quite finished; it's a three-papers-stapled-together dissertation in some sense, but I'm also retconning all my work to make it fit together nicely with what we now know about LVars, which involves redoing the various determinism and quasi-determinism proofs, and I'm not done with all of that yet. Nor is all the prose quite as far along as I want it to be. But it's ready for my committee, at least, to look at. Sooner or later, I'll make it public, revision history and all, like Rob simrob did; I might even do that with it in its current, unfinished state, like Alex and Brent Yorgey are doing.
  • Working on my dissertation brought me to the breaking point of frustration with my janky old OS X 10.6.8 and my janky old TeX Live 2008 installation and my janky old non-deterministically segfaulting GHCi. So I finally upgraded to Mavericks, and, among other housecleaning tasks, blew away my old TeX and Haskell environments (and a bunch of other language platforms and environments and so on) and got shiny new everything. Foolishly, I decided to do all this twelve hours before my self-imposed draft-to-committee deadline. But I was able to get everything building again under the new TeX with minimal fiddling, so, no harm done, and I'm much happier with my whole Computing Situation now. (And it will be nice to be able to actually build Rust again, which I haven't been able to do on my OS for the better part of a year!)
  • I finally won at 2048, which I've been trying to win for months! A few days ago, I was talking with a Hacker School acquaintance about my seeming inability to win the game, and she said that I should ask her if I wanted "spoilers", which struck me as a strange choice of words. I realized that perhaps my lack of success with the game had something to do with the fact that I didn't understand what it would mean for this kind of game to have "spoilers", and said so; she said that there was indeed "one weird trick" that she'd found was important to winning. The interesting thing is that I didn't have to ask what the "one weird trick" was -- just knowing that there was one was enough to give me an idea about what it might be. Once I started playing with that technique, I was consistently scoring higher than I ever had before, and pretty soon, I won. Later, it turned out that what I had done was in fact the "one weird trick" she'd had in mind (rot13'd for spoiler): gur gevpx jnf gb cvpx n qverpgvba va juvpu V jbhyq arire zbir -- va guvf pnfr, V jnf nyybjrq gb zbir hc, evtug, be yrsg, ohg arire qbja. Qbvat guvf zrnag gung V dhvpxyl npphzhyngrq ybgf bs ovt-ahzore gvyrf ng gur gbc bs gur obneq, naq V eneryl unq fznyy-ahzore gvyrf genccrq va n cynpr jurer V pbhyqa'g trg gb gurz. Vg frrzf pbhagre-vaghvgvir gung lbh'q or noyr gb cynl orggre ol gnxvat bcgvbaf njnl sebz lbhefrys, ohg gurer lbh unir vg. Sbe zr, gur uneq cneg jnf univat gur frys-qvfpvcyvar gb arire zbir qbja, rira jura n grzcgvat zbir gung frrzrq tbbq va gur fubeg grez cerfragrq vgfrys.

[User Picture]From: cos
2014-08-13 02:32 am (UTC)
Huh. That's not at all how I would phrase it, but I think what you call the "one weird trick" turns out to be more or less equivalent to what I think of as the basic strategy of 2048. Though I wouldn't call it a trick or weird.

How I would put it is:

Gel gb xrrc gur uvturfg ahzore gvyr va n pbeare, naq nyy bs gur uvtu ahzorerq gvyrf nybat bar rqtr. Ohvyq hc gbjneqf gur rqtr, gnxvat rirel bccbeghavgl gb pbzovar vagb vg, fb gung lbh arire trg n ohvyqhc bs uvtu be zrqvhz ahzorerq gvyrf va gur erfg bs gur svryq. Guvf rafherf gung gur nern jurer arj gvyrf nccrne vf nyjnlf shyy bs ybj ahzorerq gvyrf gung lbh pna pbzovar gbtrgure.

Gur jbefg zvfgnxr - fbzrgvzrf erpbirenoyr ohg bsgra abg - vf gb zbir lbhe uvtu ahzorerq gvyrf bss gurve rqtr, be gur uvturfg ahzorerq bar bhg bs vgf pbeare. Bapr lbh qb gung, lbh znl or fghpx jvgu ybj ahzorerq gvyrf ba bccbfvgr fvqrf bs lbhe uvtu ahzorerq gvyrf. Gur uvtu gvyrf npg nf n fbeg bs oneevre, ceriragvat lbh sebz pbzovavat gur ybj gvyrf ba rvgure fvqr, juvpu zrnaf lbh'er rssrpgviryl cynlvat jvgu gjb zhpu fznyyre nernf vafgrnq bs bar ovt bar. Lbh'er zhpu zber yvxryl gb svyy hc rvgure fvqr fhpu gung vg pna ab ybatre or zbirq, naq gura lbh'yy or zber yvxryl gb svyy hc gur erznvavat fvqr.

Vs lbh qb svaq lbhefrys nppvqragnyyl sbeprq gb zbir gur uvtu gvyrf bss gurve rqtr, gb erpbire lbh zhfg svaq n jnl gb dhvpxyl trg nf znal bs gur uvtu gvyrf nf lbh pna - rfcrpvnyyl gur uvturfg barf, bagb na rqtr gbtrgure. Vs lbh znantr gung gura lbh fgvyy unir n tbbq fubg, ohg vg pna or qvssvphyg gb qb guvf.
(Reply) (Thread)
[User Picture]From: lindseykuper
2014-08-13 08:00 am (UTC)
Interesting. Yeah, when phrased that way it doesn't seem like a "weird trick" at all! They're not quite equivalent, of course -- for example, when I play the way I described it, V qba'g znxr nal rssbeg gb xrrc gur ovttrfg-ahzorerq gvyr va n pbeare; V whfg gel gb xrrc nyy gur ovt barf nf pybfr gb na rqtr (va zl pnfr, gur gbc, nygubhtu vg qbrfa'g znggre) nf cbffvoyr. But maybe I'd do a lot better if I actually paid attention to that.

It's funny to me how, even though parts of the strategy you describe had occurred to me before as I'd played the game, for whatever reason it wasn't until I started thinking of the game as something I could win if I applied "one weird trick" that I was able to finally actually win.

Another funny thing, which has nothing to do with the game itself but is another testament to how brains are weird, is that there was a period of time a couple months ago when I was both playing a lot of 2048 and scouring craigslist for housing, and I'd alternate the two activities -- so now the two are inextricably linked in my mind, and whenever I play the game there's a mental voice saying, "Shouldn't you be on craigslist right now?"

Edited at 2014-08-13 08:05 am (UTC)
(Reply) (Parent) (Thread)
(Deleted comment)
[User Picture]From: lindseykuper
2014-08-15 08:05 am (UTC)
Interesting! I think I'd better not try Threes -- all the evidence I've seen suggests that for me, it would prove even more addictive than 2048.
(Reply) (Parent) (Thread)
From: aleffert
2014-08-17 04:23 pm (UTC)
It may be you would have a different experience, but I found Threes significantly less fun than 2048. Sure, Threes had more replayabilit,y but since there was less of a goal and it was easier to get stuck it hit my why am I doing this sensor, unlike the half mindless addictiveness of 2048.
(Reply) (Parent) (Thread)
From: Gabriel Scherer
2014-08-13 04:36 pm (UTC)


Nice to see all this wrapping up nicely! (And congratulations for your new position, that looks like an exciting job.)

Something that was a bit puzzling with the first LVar proofs is this business of merging names coming from independent threads. At the time it felt like a form of accidental complexity, but you've made the connection with distributed computing that probably has this kind of problems (decentralized handling of names). Do you have any hopes to get rid of it eventually, or do you now think it is an essential part of the metatheory?
(Reply) (Thread)
[User Picture]From: lindseykuper
2014-08-14 09:44 am (UTC)

Re: Names

Hi, Gabriel!

You're absolutely right that the stuff about names of allocated locations was, and is, accidental complexity. In our FHPC '13 paper, it was particularly bad -- the business with renaming locations leaked into the language semantics itself. It got a little less awful with our POPL paper, where we just decided that our language would be quasi-deterministic modulo a permutation on location names. If you look at the technical report that goes with our POPL paper (not that I really recommend you do), there's an ugly little cluster of lemmas in the middle of the quasi-determinism proof that are basically there entirely because of name-related bookkeeping. So, for my dissertation (and because we're planning to do a journal paper), I (with a lot of advice from Neel) am refactoring that proof to make it much less nasty.*

It wouldn't be the first time that someone had to do a lot of name-related bookkeeping to deal with allocation -- what we do is actually kind of like what Neel did in his "FRP without Spacetime Leaks" paper (see the paragraph on "Supportedness and Location Permutations"). Some other authors deal with this by just not doing allocation at all -- instead, they have a pre-existing, arbitrarily large store of locations where every location has some default initial value. That's how it is done in, for example, the Featherweight CnC language in the Concurrent Collections paper that was the original model for how to structure our determinism proof. Note that there's no way to allocate a new location in the store in Featherweight CnC -- you don't need to, because they all already exist! In retrospect, it seems like that would have been a smart way for us to design our formalism. On the other hand, when one is programming with our Haskell library then one really does have to create and allocate new LVars, and so I suppose it's nice to have something in the formalism that corresponds to that.

The connection with distributed computing hasn't really done anything to change our approach to allocation and naming. The "Conflict-free replicated data types" paper, for instance, ignores the question of how to create new replicas (and what to name them), and just assumes that there's a finite set of processes with one replica at each process. So we inherit that assumption in our own work.

(Thanks for asking, by the way! Maybe I should say a little more about all this stuff in my diss -- I didn't know anyone cared. :) )

* Incidentally, I've also updated the formalism to allow not only the usual least-upper-bound writes, but also any write that is both inflationary and commutative. (My dissertation, and the eventual journal paper, will cover this in much more detail.) So I would need to revisit the proof anyway, even if it weren't for this refactoring that we are doing.

Edited at 2014-08-14 09:45 am (UTC)
(Reply) (Parent) (Thread)
[User Picture]From: mindstalk
2014-08-13 07:05 pm (UTC)
Ah, you must have missed my post on the game: http://mindstalk.livejournal.com/394305.html

Congrats on the accomplishments.
(Reply) (Thread)
[User Picture]From: bubblingbeebles
2014-08-14 01:06 am (UTC)
(Reply) (Thread)
[User Picture]From: lindseykuper
2014-08-14 08:49 am (UTC)
Hah! I think I'm not quite ready for that.
(Reply) (Parent) (Thread)
[User Picture]From: bubblingbeebles
2014-08-14 01:08 am (UTC)
also congrats on the draft!
(Reply) (Thread)