BlogFace.org

So, specifically trying to counteract my lifelong tendency towards grumpiness about cooking, I pulled what may have been a very bone-headed move and purchased a ~10" cast-iron skillet. Now of course I know very little about cooking, and I know it's a risk in any endeavour to think you are going to succeed just because you bought the right equipment, but it seemed from basic internet research like a very appealing sort of one-size-fits-many tool, rather inexpensive ($20) for being so, which favors (through the "seasoning" process) cooking with a lot of oils and fats, which though I am not necessarily expert in executing, aligns well at least with the sort of foods I like eating. Also I get kind of a perverse luddite thrill from it being so heavy, clunky, and dangerous, inasmuch as you can burn yourself on the handle really easily.

I "tried" cooking a simple scrambled egg to give it a "I actually know this is going to fail" sort of initial test run, and it did utterly fail. A mass of burnt butter and burnt egg.

Somewhat surprisingly, the second attempt yielded results both fluffy and delicious. Internet advice insisted that you are supposed to wait a certain amount of time before pushing the egg around, but somehow it got to the stage depicted by their "wait until it looks like this" pictures in a matter of seconds. Maybe I just had it on super high heat, but it was at the middle of the dial. Dunno how "low heat", "medium heat", "high heat" mean much of anything consistently across different people's stoves anyhow but I'm sure I'm not the first to observe that.

Anyway, tossing some eggs, butter, and a bit of milk into a hot iron thing yielded Tasty Food. Hopefully I will not soon get sick from rust poisoning, salmonella, or rancid butter from improper cleaning. Barring that, I'll next attempt the dish that was the major ulterior motive for having this thing: it is just about the right size I think for a single-serv version of the one ever-so-slightly-nontrivial recipe I've always been able to manage well, namely Dutch Baby.

Hm, I made a hotel reservation for POPL, and they said it was made, and then they retracted their claim and said they can do me for all but the last couple days. Guess I have to look around again, grr.

Fighting generalized bitrot today again by seeing if I could get sketchup working on my desktop machine. This is in principle harder than getting fontforge working again because (a) it's not open-source, and (b) there is no linux version at all.

So I tried running it under wine. Somewhat impressively, it worked, and pretty acceptably fast, even though I have no hardware GL acceleration on this machine under linux.

...except around every cursor there is an ugly white box, obscuring what you are trying to work on.

Obviously then I dug into the wine source and determined that the following patch suffices to fix the problem:

*** wine-1.1.33/dlls/winex11.drv/mouse.c
--- wine-1.1.33/dlls/winex11.drv/mouse.c
***************
*** 518,527 ****
              {
                  case 32:
                      /* BGRA, 8 bits each */
!                     *pixel_ptr = *xor_ptr++;
!                     *pixel_ptr |= *xor_ptr++ << 8;
!                     *pixel_ptr |= *xor_ptr++ << 16;
!                     *pixel_ptr |= *xor_ptr++ << 24;
                      break;

                  case 24:
--- 521,540 ----
              {
                  case 32:
                      /* BGRA, 8 bits each */
!                 {
!                 char red = *xor_ptr++;
!                 char green = *xor_ptr++;
!                 char blue = *xor_ptr++;
!                 char alpha = *xor_ptr++;
!
!                 if (alpha == 0 && !alpha_zero) {
!                   red = 0;
!                   green = 0;
!                   blue = 0;
!                 }
!
!                 *pixel_ptr = (alpha << 24) + (blue << 16) + (green << 8) + red;
!                 }
                  break;

                  case 24:

though I'm still slightly confused which piece of software is to blame for the problem. It seems like the Xcursor library thinks that "white with alpha 0x00" means "ha ha just kidding completely opaque white" and so what the patch is doing is just forcibly rewriting "transparent white" to "transparent black" which Xcursor will honor as transparent. But I have this sneaking suspicion that maybe a "add brightness" or "screen" sort of transfer mode got invoked somewhere, as that would explain some of the other mysterious experimental results I got on fully transparent colors other than white.

Oh, and the other broken thing is COLLADA export. It spews some errors at me about XML libraries not being found, and hell if I know how to fix that on the windows-side of things. In the meantime I found a Ruby script to be run inside sketchup itself which seems to export DXF okay, but I tried getting Blender to import it and it just choked and gave me silent failcess.

---

Turns out: blender just doesn't accept DXF files without a proper header. Easy enough to add that.

so what about insomnia. This is not insomnia. so what about denial. This is not that, either.

Aw dude the contractor dudes that were here a few weeks ago and told me they'd fix the huge (like nearly 0.5in at their widest) air-gaps in my street-facing windows totally just did today. My livingroom is so toasty-warm now.

Hung out with rdore today since he's on xmas vacation still and his family live out in the Philadelphia suburbs not quite an hour away on the R5. Played "Agricola" for the first time and rather enjoyed it --- he beat me pretty handily though. Also played some very abstract game with a pyramid-shaped board I can't remember the name of, which Richard said was Reiner-Knizia-designed, but which can't possibly be the same game as Ramses Pyramid, which involves dice. Anyway it was very interestingly subtle for how simple the rules were.

Terrence Tao has a post about probability theory that made me puzzled at first, but I'm growing to like it more and more as I digest it.

There's an important insight to be had somewhere along the line that probability theory is "just" measure theory, that you can stop worrying about what words like probable "really mean" and get a significant amount of work done by just thinking of probable events as just "taking up more space" in the measure space of all possible worlds.

But Tao is making a further point, that even the set-theoretic underpinnings of measure theory are somehow excessively concrete. We don't have to go so far as to philosophically settle what randomness "really is", but we do benefit from building up a more first-class intuition for the concept of measure than it being just a map from sets to reals.

I like his point that extension (or what might also be called "refinement") of a measure space by observation of new experiments/events is the thing-which-concepts-must-be-robust-under for probability theory, just as change-of-coordinates is the thing-which-concepts-must-be-robust-under for linear algebra. Is there a category-theoretic way of saying this, I wonder? It's not immediately occurring to me, but I suspect I'ma feel dumb when it does, or when someone points it out.

The thing I'm getting stuck on is that change-of-coordinates (or homeomorphism, or algebraic isomorphism) are all, well, isomorphisms. They're two-sided, bidirectional, symmetric. Extension of probability spaces is directed, so it doesn't seem to make sense to say that the theory should quotient out by it.

Here's a quick little monocase font named after the CTA Brown Line terminus. It is intended to be what it would look like if Gotham and Clarendon had a baby. Color scheme is stolen from one of 0436's that I liked, and then washed out a bit.

About ten years ago, at the end of the calendar year 1999, I got into bed around at my dad's house in Madison, WI at a little past 9pm, thinking I was going to just take a quick nap before going back downstairs for the big y2k roll-over.

I slept through it, of course. And woke up a half-hour later to wander down and find the world hadn't exploded.

I just reenacted the event last night for the sake of tradition. Well, it was more like 10:30 when I went to sleep, and had no illusions that it was just a nap, and was woken up just at midnight by the neighbors cheering, but it felt right somehow anyway.

About ten years ago, in the beginning of the calendar year 2000, 19-year-old me took some classes including "15-312"^* and "Category Theory", and finally got around to experimenting with a thing called "dating".

A highly auspicious time.

Conclusion: it's been a good decade for me, personally. I've learned a lot.

(^*for the non-CMU people: a very formal-methods-centric course on the principles of programming language design and type systems, the gateway drug to essentially all the research I've done since.)

I went back to trying to get fontforge in a pleasant working state, and learned a few minor but interesting facts about fvwm. This is because one of the main obstacles to it being in a pleasant state is that on this dual-head setup, it keeps tossing windows right on the seam between the two monitors (i.e. right in the middle of the two-screen virtual screen). I succeeded at stopping it from doing this by saying

Style "lt-fontforge" !UseUSPosition, !UseTransientUSPosition

in my .fvwm config file. One thing of note is the string "lt-fontforge". I thought the first argument of the fvwm Style command had to be a string matching the title of a window, which would be a real pain in the case of fontforge, because it does not include any one reliable substring in its windows' names. Fortunately, Style is actually matching (according to the manpage) "a window's name, class, visible name, or resource string", with "class" and "resource string" being afaict conventionally application-consistent strings supplied to X11 somewheres in the guts of the window creation process. I was able to find out the one fontforge uses by running FvwmIdent. Dunno what "lt" stands for.

Again citing the manpage, what !UseUSPosition does is it

suppresses using the user specified position indicated by the program (USPosition hint). It is generally a bad thing to override the user's choice, but some applications misuse the USPosition hint to force their windows to a certain spot on the screen without the user's consent.

with the arch passive-agressive bold emphasis being entirely mine. I'm looking at you, fontforge.

But of course !UseUSPosition doesn't suppress this bad behavior for all windows, just all nontransient windows. You need to additionally say !UseTransientUSPosition for that. Not that the documentation tells you this or anything, but you can infer it from the documentation for UseTransientPPosition if you happen to look there.

---

Mysteriously, once I did "make install", lt-fontforge changed to just fontforge.

Back in Philly, 8 hours door-to-door from Chicago. Feels good as fuck to be back on my bike fighting headwinds off the Schuylkill. Had a sudden worry that the rent check I already wrote to my rental agency was going to bounce because of the national city/PNC buyout, but I called them and they said no, only the checkcard expires, and national city checks are still good.

Wound up seeing "Avatar". Definitely the most beautiful episode of "Captain Planet" I've ever seen. ( spoilers maybe ) (7/10)

Hanging out with techstep today. Got some Giordano's, played some Rock Band, watched some football.

Have been reading "The Trouble About Tom", a nonfiction (but with ample narrative liberties taken) book about Thomas Paine and various historical people connected to him, which _tove recommended to me. I really like it.

Also recently read:

Klosterman's "Eating the Dinosaur". This is a tough call. At his best (e.g. in the "Best Responses" essaylet, and talking about american football) he's just straight-up clever and funny. At his worst he seems to try a little too hard to mine exactly the same David Foster Wallace vein of footnotey moralizing-but-somehow-balanced introspection. On the plus side, the cultural references are 2000 plus or minus a few years (instead of ca. 1990 in the case of DFW) so I can't help but find it... comfortable in a certain way. But it's something to chuckle at, not the rich theology of tennis and genius and loss that makes you think about Life-and-what-it-Means-comma-man that I found in Consider the Lobster. (7/10)

Daniel L. Everett's "Don't Sleep, There Are Snakes". A collection of anecdotes about the author's work studying the culture and language of the Pirahã, a small tribe of people in Brazil whose isolated language is (allegedly) a counterexample to previously accepted universals about how languages work. Interesting observations and stories to be sure, though it feels a bit slopped-together at times. (6/10)

Pratchett's "Unseen Academicals". Oh this is just totally classic Pratchett. Great characters, silly and entertaining plot, ridiculous asides. And, ultimately, I think some nonzero insight about how professional sports plays a role in people's lives. (9/10)

---

In logic news, I had a good hour or two's meditation this morning over these notions of encoding modal logic into linear logic. I was afraid something would go totally awry with dependent types, because of the following line of thinking:

Linear pi doesn't work in a straightforward way. (I mean, see my thesis for how to dodge the problem without exactly coming up with the linear pi that you expected) Modal pi (as found in contextual modal type theory) does work in a more or less straightforward way. If modal stuff can be encoded as linear stuff, than where the heck does the problem go?

But I realized that I wasn't looking hard enough at the problem's particulars. If you step through the encoding, it only ever creates lollipops in types and not in kinds and so avoids the dangerous territory of linear pis entirely. Moreover, if you push the result subsequently through the LLF-to-HLF encoding from my thesis, then what pops out has no occurrence of epsilon or * --- it's a very special case that doesn't make use of the algebra peculiar to linear logic at all.

What does this mean? I think it's that there is something extra-special about a "linear" context zone which by invariant there is always exactly one inhabitant of. If you have more than one of them, you need to have an operation like *, and then you need to decide whether it's associative, commutative, idempotent, etc. If there can be none of them, you have to have an epsilon and decide what sort of unit laws it might or might not satisfy with respect to * (witness the two different units and two different notions of "empty context" in BI). But if there's always exactly one, you can get away with no algebraic choices at all!

I think this reasoning has a chance, if developed further, of settling in my mind why intuitionistic logic's right-hand side, which is sort of "linear" from a Girardian perspective (or "modal" from a Gödelian perspective) is nonetheless more canonical than just a special case of classical linear logic (or classical modal logic).

i've noticed a particular quasisynaesthetic thing i do with math where i subconsciously map abstract ideas not to color nor shape but rather size. i notice this primarily when i'm trying to think of some kind of math in terms of some other math, and suddenly a thing that used to be very small is now big, or vice versa. only once i get used to working with the tools at the "bigger" level do the things they work over become "small" and easy to think about abstractly. like for example, when i first learned about functors, they were HUGE, because i mean, come on, they go from a whole category to another freakin' category. but then i remind myself, oh, they're just morphisms really, which are these little spindly arrows, and they go between little pebble-sized objects that just happen to be categories. (i used to think sets were big!) it still blows my mind a little that initial algebras are these big clunky things, but the natural numbers are one o' those, and the natural numbers are tiny.

Merry xmas!

I'm trying not to be that guy but it is kind of weird being in a household where there is always always always a television that is on, compared to not owning one. It's not that I don't like television shows, I mean, I love 30 rock and am getting into "Always Sunny" and have enjoyed Lost and the Soup and all sorts of stuff, but I just start flipping out after hours and hours go by and there is never any silence ever.

Anyway I watched some bits and pieces of various movies because I couldn't help it.

"500 days of summer" seemed moderately interesting, if a bit depressing. And sort of cookie-cutter-shaped in some ways how the character motivations worked. I mean, there's a dude, and he totally falls for a cute girl because she's cute, and he mopes to the extent that he does not get in her pants.

"Enchanted" seemed like a passably good parody/pastiche/mocking-reboot of disney movies.

"Night at the Museum" bleah bleugh ugh. I am disappointed that this is being turned into a "traditional christmas movie that we will play on repeat all day".

"Elf" mostly the same reaction.

"All about Steve" has Sandra Bullock awkwardly portraying an aspie who makes crosswords I think? Seemed pretty terrible, but I wasn't paying much attention to it. Tomatometer says 6%.

i suppose it's about time to repost this from last year:

The Twelf Days of Christmas

have a lovely day!