Donna

You know, I do like obsessively keeping old work of mine, even if I am terrible at organizing it, because I think between 2006ish and nowish I got somewhat better at Illustrator and Photoshop and stuff. (The latter link is a work-in-progress teaser for a print project for Spoons'n'Copic's living room that I am having lots of weekend fun with)

It helps I guess also that I used proper fractal-random-displacement nonsense that I learned in like 1994 (implemented by having sml output svg, of course) to generate the outlines rather than trying to draw them by hand.

Some papers I read today.

"Resource usage analysis", Igarishi and Kobayashi, from POPL'02. This was the PLClub paper of the week. I didn't care for it much at all. There's some idea in there that seems really cool as a generalization of linear uses, but I struggled in vain to really grasp it. There are too many formal concepts not really nailed down enough for me to understand what they're doing. There's not really a strong distinction between things that are definitely propositions and things that are merely functions-on-propositions that feels incredibly alarming to me aesthetically. I'm told these are the dudes who went on to do session types --- can't say I ever totally understood them, either.

"Simplicial Databases", David Spivak. Got this from a CMU talk announcement that Steve Awodey sent out. I am such a sucker for aiming big, big categorical guns at problems like these. I kind of lost track of what was going on halfway through, but it was fun going up to that point, pullbacks and slice categories and labelled simplicial categories and whatnot, all in the name of making mathematical sense out of how databases are actually done out in the real world, especially when that diverges from the nice but too-simplistic classical theory of relational algebra.

"F-ing modules", Andreas Rossberg, Claudio Russo, and Derek Dreyer. This paper is an utter breath of fresh air. I like it so much I find myself constantly worrying that I am missing some flaw in it only because of my nonexpertise in module systems research. Anyhow I find it a rarity that I am able to write a research paper in such a pleasantly direct style. It's just, I don't know, here is what we are going to do, here is why we want to do it, here is how it works, step one, two, three, there --- we're done, isn't it fucking beautiful? Maybe it is a matter of choosing your content carefully to be in reasonably-sized pieces or something, but even before finishing digesting all the middle bits, I can already say that I find it a pleasure to read, and a very nice result to boot, to wit, directly translating a generalization of the ML module system into System F_ω. I mean, if there are not the aforementioned flaws that I am too dumb to notice, it definitely has the feeling of "gosh why wasn't the ML module system explained this way all along" to it. You just kind of pop out abstract types into "monadically" managed prefixes of System F_ω existential quantifiers and dodge a ton of bullshit with selfification and the avoidance problem and stuff.

Plus, you can't beat the cute title.

That ATS post was really gumming up the LJ works. LoWri #3 is a PDF miniposter I hacked together with Dan after reading Types, Abstraction and Parametric Polymorphism in Karl's class and deciding to implement the first little bit in Agda. What we discovered is "interpreting an expression into set theory" and "proving the abstraction/parametricity theorem - that the expression is logically related to itself" are two things with precisely the same computational content. As we suspected, as Bob confirmed, and as these guys probably describe in detail but I haven't read it this means that basically it's the same thing happening in two different categories. Nifty.

So, if you're inclined, here's a PDF with pretty Agda code laid out perfectly in two parallel columns.

A while back I talked about blood donation - I'm scheduled to give blood around 1:30pm on December 10 at the cushy nice permanent blood donation place downtown. Anybody interested in joining me for the bus ride down and a good ol' fashioned blood donation? Feel free to respond off-comments.

So, because ATS is the name of any number of Hogwei Xi's typed languages, the current incarnation is called Anairiats. Simple stuff today; I'm quite a few days behind on my NaLoWriMo.( LoWri #2 - Hello Anairiats )

In conclusion I achieved nothing so far but it wasn't too hard to get the darn thing running, and I'll stop here because I wrote this like four days ago and never finished. More Anairiats games later.

http://radar.spacebar.org/f/a/weblog/comment/1/1033

It was a special shame/privilege (tried to come up with a good sounding portmanteau expressing this sentiment; failed; any luck?) to find myself looking at cplusplus.com and to see an animated Microsoft Windows VII advertisement that uses my 13 year-old font Action Jackson:



It is truly my most popular child. I looked around: It turns out that the font is actually part of Microsoft's current enterprise software branding campaign "the NEW efficiency". You'll see it in whenever they try to sell their expensive stuff by the hundreds to CTOs; e.g.



I like to imagine some guys in suits trading whitepapers. The most surreal is their launch event hooha which has extremely boring videos of señor people giving powerpoint presentations which include this branding. For example, join them for the launch event (warning, you need Silverlight and then you gotta wait to download a LOT of this animated lady that's going to be your personal liaison).

(In old, non-ironic sightings news, Tadbot spotted One Constant used on the Scribblenauts site, which game looks awesome.)

Decided to try something different from Frita's this morning; had a chicken gyro. Not bad! I am not sure if the sauce is sour cream or yogurt-based (I think it is sour cream?) but it is pretty tasty.

Another CMU-ism that I am slightly sad to be without: everyone having a UPS in their office. Some dudes fiddling around with electrical stuff here in the basement caused a brief power blip.

When my computer came back on, I had no network. Not that the internet infrastructure in the building was down, because my laptop still worked, but I had no /dev/eth0 device at all! I tried rmmodding and modprobing my network driver, e1000e, but no dice. I did two finds and a diff to determine that there was no change to all of /dev between the module being there and not. /var/log/messages revealed the module not complaining about any errors, though. In an act of desparation, I got the kernel module sources off the thumb drive I had originally installed them from, recompiled, and reinstalled. And it worked! I have no idea why. Even more mysteriously, /dev/eth0 still doesn't exist. Indeed, the module's installation or removal again causes no changes to the entire /dev tree. But eth0 does exist according to ipconfig. Is this some new fancy modern linux virtual device notion? Nobody told me about it. Grumble grumble off my lawn.

No, apparently I am just having bizarre, reality-independent notions about network devices living in /dev.

Amusing log message coming out of a Haskell compilation: (attempting to play with grapefruit)
Generating and compiling a zillion numerical type aliases, this might take a while

Yesterday food adventures:

"Steak Queen" food truck. Boasts "bests steaks on campus". Had a cheesesteak, was not impressed. Steak was sort of gristly and tasted not entirely pleasantly like stir-fry. At least it wasn't liquid-greasy. More expensive than Frita's, farther away from my office, and less tasty. (5/10)

"Gusto", ever so slightly upscale neighborhood pizza place on 22nd between Spruce and Locust. Had an italian sausage calzone, very very tasty. Only problem was that it was two people's worth of food. The onions in it were sort of meh, and achieved that floppy cooked-(but not fried-)onion texture that no right-thinking person enjoys, but the red peppers were really good, the other filling ingredients quite tasty, and the dough was just perfect. The problem with a lot of calzones I have is that the two foldy-end bits get nice and crispy and the center is mooshy and doesn't have enough bread. This fellow was rectangular and somewhat thin, so basically the crust was perfect everywhere. Also: either there was only mozzarella and no ricotta, or else very little ricotta such that I could not even tell it was there. This is exactly as it should be. (8/10)

I was skimming this paper and at the top of page 3 misread

the task of the mathematician is to seek a deductive pathway from the
axioms to the propositions or to their denials.

as

the task of the mathematician is to seek a seductive pathway from the
axioms to the propositions or to their denials.

I like my version better.

( An algorithm puzzler )

Two months at this postdoc today. Woo?

Just got an email from Vivek Nigam, who is newly arrived over at the math department. He had a paper with Dale that I wanted to bug him about, so this is very welcome news.

urban hike #8 (numbered counting urban hike "maurice" in san francisco and the west virginia walk) was a short one, about 7 miles, since it took place later than usual due to brunch. a little longer than that if you include the walk from coca cafe. stops included voluto cafe (where kepod was working), the church used for the last scene of dogma, and tazza d'oro. weather was perfect! good times. still no title for it yet, so if you have any ideas...

Have been looking at the literature on Functional Reactive Programming and related things. I am learning that no matter how much I think I've properly digested the whole world of monads and arrows and applicative functors, there's always more to learn.

Generally speaking the programmers' approach to all of these concepts seems very weird to me compared to the logician/category-theorist take, but McBride and Paterson's "Applicative programming with effects" is a really awesome paper that synthesizes the two points of view pretty well for the case of applicative functors. The punchline is that what a Haskell hacker calls applicative functors are what a category theorist calls strong lax monoidal functors. Yes, both strong and lax! Terribly, from a terminological point of view, "lax" means that the functor is weaker than "weak", and "strong" isn't the opposite of "weak" (if anything, "strict" is --- but since "lax" exists as a concept, it's hard to say that "strict" is the opposite of "weak", just that it's, ahem, a stronger condition than "weak") and means that the functor has a "strength".

Ok, everybody sufficiently confused now? Good.

The important thing about these strong but sensitive applicative functors is that they represent a notion of effect that is compatible with product types in one direction, and this very compatibility is a notion of sequencing of effects. Suppose T is an applicative functor. If I have a piece of data of type TA, which is a computation returning type A, and a piece of data of type TB, a computation returning B, then I can make T(A × B) by running the first one and then the second. I can't expect to necessarily do the reverse --- I might reasonably encounter a computation T(A × B) that doesn't naturally decompose into TA and TB. This one-way ticket is the laxness. For a weak monoidal functor would commute up to isomorphism with products, and you'd have T(A × B) isomorphic (with suitable coherence diagrams) to TA × TB, but a lax monoidal functor only goes one way. It needs to be a strong lax monoidal functor for the same reason that the monads in functional programming are always strong monads, to be compatible with our expectations about variable contexts.

But wait, I hear you saying, weren't we told that monads were the ultimate story on a pure functional treatment of effects and sequencing and stuff? Answer: they're one story, yes. The intuitive distinction between monads and applicatives (which the paper above explains rather nicely) is that monads, unlike applicatives, let you use the result of one computation to influence which other computation takes place as the second step. Just look at the Kleisli star's type, it's right there:

TA → (A → TB) → TB

The second argument gets the value of type A before it spits out the final computation. If T were just an applicative functor, the most we could make out of TA and (A → TB) would be TTB. When T is a monad, we have exactly the categorical μ to turn that into TB (this is of course exactly how the Kleisli star is implemented from the categorical data T, η, μ) but when T is merely applicative, TTB is considered a more complicated thingy than TB --- it has two stages of computational dependency, which we're not allowed to erase.

I woke up this morning with the word "huitlacoche" in my head and I had no idea why. I looked it up on wikipedia and it turns out it's a weird-ass black, swollen, infected version of corn that some people consider a delicacy.

I was like why do I even know this word.

Then I remembered! I had seen it years ago on Steve don't eat it!, which is great food writing and you should read it all if you haven't already. The your-mom jokes in the Huitlacoche episode are kinda dumb but I like a lot of the other ones and anyhow I take pleasure in reading about another dude eating really gross things so I don't have to.

An observation on researching problems you are not an expert at, or, "Why I am not a kook".

This happens to me occasionally that I get interested in a cute little problem, (e.g. graph reconstruction) think about it for a while, come up with some partial results, and then poke at the literature and quickly go ohhhhh shittttt people have really studied this, and a single section of their papers has way more insight than I could expect to generate if I slogged away at the problem for a month.

Which is okay, since I'm not going to slog away at it for a month, but rather go back to working on problems I can make headway on. But it's still fun to play with such things, and a good sort of exercise to wrestle with new problem domains.

I think all it takes to go off the deep end into kooksville is to forget this last step of being at least a token amount of welcoming to other people's ideas.

Anyway, case in point (of other people doing awesome work, not of people being kooks) is David Rivshin's master's thesis which has some algorithmic cleverness that let him computationally determine a whole ton of statistics on graphs that are sort of "trying to be counterexamples" to the reconstruction conjecture. In particular on page 19 there are a few pairs of graphs that have 7 "cards" in their "deck" (i.e. vertex deletions) in common! I managed using some dumb perl scripts to find a pair of 8-vertex graphs with 6 in common, and determined that there were no 9-vertex graph pairs with 7 in common but after that bumped up against the fact that there are like 12 million 10-veretx graphs, and finding pairs of things in a 12 million member set that satisfy some property sounds very 72 trillionish, and that's no good for anybody.

Also, Bowler, Brown, Fenner's "Families of Pairs of Graphs with a Large Number of Common Cards" [sorry, I can't find a copy not behind a !@#$ paywall] has a nice construction on page 16 that yields as many overlaps as you want; if you want n nonisomorphic co-occurring vertex deletions, you need a pair of graphs of (asymptotically) 5n vertices. (note the paper says effectively 5n/2, because it's thinking about multisets of vertex deletions, whereas I'm thinking about sets, and the deletions come in isomorphic pairs) You basically take a line graph with a pair of dangling degree-1 vertices hanging off it every three vertices:

   o        o        o
   |        |        |
o--o--o--o--o--o--o--o
   |        |        |
   o        o        o

and the other graph is a ring graph with, again, a pair of danglies every third vertex of the ring except exactly one of the danglies (just one, globally) is missing. This is harder to ASCII-ize, but imagine:

       o                 o
       |                 |
...-o--o--o--o--o--o--o--o-...
       |        |        |
       o        o        o

where those outer two half-edges are supposed to wrap around and connect. The way this generates lots of different common vertex deletions is this: imagine cutting the ring graph on one of the ring vertices without bits dangling off of it. This creates a line graph with one danglie-thing missing somewhere, but all of the somewheres are non-isomorphic to one another, and the original line graph can be made isomorphic to this one by chopping off exactly one dangling vertex.

There's something I really like about both of these works that seems ubiquitous and useful in dealing with really hard conjectures about the existence of mathematical objects --- that is, looking for a quantitative sliding scale at the one end of which the conjectural thing might or might not exist. The win is that (at least in this case) you can write programs to hunt around for the almost-counterexamples, the close calls, the weird outliers, and hopefully learn something from them. Looks as if graph reconstruction is still quite tough after all this data has come pouring in, but it's neat to think about.

Stupid fun with graph visualization from last night. I am not sure which browsers it will work on, since it does funny embedded SVG stuff. Works for me on the latest firefox.

( You are about to view content that may not be appropriate for minors. )

I do so love Lipton's blog. The linked entry mentions the graph reconstruction conjecture which is a beautiful little open problem in graph theory. In one sentence, it is:

A graph (on at least 3 vertices) is uniquely determined by the multiset of all possible vertex deletions of it.

Determined up to isomorphism, that is. A vertex deletion of a graph is the graph you get out of deleting some vertex and all the edges incident to it. You have to say at least 3 vertices because it's just not true for 2! There are only two graphs on 2 vertices, * * and *→*, which both have {*,*} as their multiset of vertex deletions.

There's a related (stronger) conjecture,

A graph (on at least 4 vertices) is uniquely determined by the set of all possible vertex deletions of it

And there you can see the 4 is necessary, because the multiset of vertex deletions of
* *→* is {* *, * *, *-*}, and that of *-*-* is {* *, *-*, *-*}, and these collapse to the same set if we ignore multiplicities, {* *, *-*}.

Here's a question I thought of:
Given n, what is the smallest pair of graphs G and H such that ||D(G) ∩ D(H)|| ≥ n, where D(G) is the set of vertex deletions of G?

I can't even think of graphs such that ||D(G) ∩ D(H)|| ≥ 3! I sort of expect they must exist, though. The thought of there being a constant upper bound on ||D(G) ∩ D(H)|| for all G and H seems absurd. I bet this could be refuted by playing with the output of Nauty, which contains tools for generating all nonisomorphic graphs over n vertices, and testing graph isomorphism.

---

Ah, thought of a pair over four vertices just by pencil-and-paper brute force.

   o--o
   |
o--o--o

   o--o
   |  |
o--o--o

both possess vertex deletions

o--o   o--o
|      |
o--o   o

   o
   |
o--o--o

and then each has one more that distinguishes them.

---

Another example that is smaller with respect to jointly how many distinct vertex deletions exist of of G (3) and H (4):

G           H
  o---o       o---o
 / \ / \     / \ / \
o---o---o   o---o   o

Maybe the right question to ask is how small you can get the distinct sets of vertex deletions of the pair
such that their intersection is at least n big. In this case (||D(G)||,||D(H)||) = (n,n+1) for ||D(G)∩D(H)||=n is as close as you can get without violating the second conjecture above (which violation would require (n,n)), and this does in fact obtain for n=1,2,3.

Some things that have gone wrong lately but are more or less acceptable:

My office is at a pretty steady temperature of 85 degrees now. I complained about this a week ago-ish when it hit 80 and, allegedly, gears are turning, and maybe eventually it will be fixed.

My bicycle's tires started to get a little low on air, and I thought, hey I'll by a cheap little pump and pump them up a bit, and promptly did everything wrong and let all the air out of my back tire. After escargonaut heroically helped me a lot over the phone, I still couldn't get any air to apparently get into the tire and I finally gave in and went back to the bike shop and they just air-compressored them back to normal shape.

The moral here is that when you are a Educated Person and fancy yourself an Adult at least and on a good day Generally Quite Clever, and it's just about the most painful thing in the world to have --- and not only to have, but to display in front of an entire store full of people who know what's what --- the sort of obliterating, flailing, not-even-a-rudimentarily-correct-mental-model ignorance (the sort that you can just hardly fathom any non-troglodyte human having when it is about your own favorite problem domain), it is actually a good idea to just suck it the fuck up, ask for help when you need to, and try to observe and by observation learn a couple of things if you can. Now I know, for instance, that there are two types of air valves, one common in low-pressure mountain bike tires, one in high-pressure road bike tires.