syzygies

i've noticed some similarities in
1. playing games that involve a lot of long-term caretaking, specifically ones you play on devices that are more or less always on your person, such as Ingress and Kim Kardashian Hollywood and the iOS Sims game
2. Quantified Self sorts of ideas: making numeric systems out of personal self-care (exercise, work, sleep, etc.) through, effectively, body augmentation, and using those data to arrange goals and analyze progress.

for example, the process of tracking self-powered movement (walking, running, biking) with endomondo on my phone leaves marks in a digital space, which i then track and do some analysis on in a spreadsheet; in Ingress, my physical movement through space, punctuated with some calculated button-pressing, leaves marks in a digital space measured by the game's objectives. none of these activities is ever about "winning" in a "finishing" sense; it's all about maintenance and learning new strategies and building new habits.

all of these things use time as currency. in the kardashian game, taking actions requires energy points, which regenerate with time. in ingress, the same thing happens with XM, although you can also get more by moving through space. in the sims, you make progress in the game by completing actions, which take various amounts of time during which the sim doing the action cannot do anything else. (every action is atomic; there is no multitasking. even long-term tasks like baking and gardening completely occupy the sim's faculties to the point where another sim cannot, say, talk to them during this process. this is mitigated by the fact that you control a small army of sims and can be clever about dividing their labor.)

if ingress is Augmented Reality then so is QS. these are both ways of giving us access to the same space we didn't have before; ways of superimposing new layers of information on a structure that lies unchanged.

sometimes i refer to games/activities like this as "gardening projects." they are played with spurts of concentrated, calculated action, followed by periods of inattention and patience. you can only influence initial arcs of progression, nudging things in certain directions using predictive intuition, rather than directly control their course.

imposing a quantified/gamified structure atop my own life has been helpful to me in the past. in the months after my mom got sick, i had a spreadsheet i named "LIFE RPG" where i gave myself points for daily aspects of life: cleaning, socializing, working, exercising, and creating. they were instructions that felt external and thus trustable. it made an answer to that sinking feeling accompanied by the question, "what am i supposed to do?"

let me tell you about some video games

naya's quest (browser, free, a coupla hours i guess), terry cavanaugh's new puzzle game about reasoning about nonsensical* isometric 3-space. it has a fantastically just-vague-enough-to-be-spine-tingling little running narrative and a lovely crescendo of "OH MY GOD WHAT IS HAPPENING TO MY BRAIN" at the end. (*well, there's a consistent logic to it, but it took me awhile to convince myself of that fact.)

868-HACK (iOS, $6, infinity time, but maybe 15-30 mins to get a grasp on what you're supposed to do) - this game has such a great combination of roguelikeish randomness and predictable, strategically defeasible behavior. manages to create that oh-shit-oh-shit feeling of timed games (specifically tower defense style games) while being turn based, so allowing you to be as contemplative or as reckless as you want. i play this regularly now as comforting downtime.

imposter syndrome (browser, free, 5-10 minutes) - the only IFcomp game i've played so far, definitely kind of heartbreaking/triggering (TW public speaking nightmares, internet harassment, sexism) - what i liked mostly was (1) the multiple endings (2) the scifi elements of it are kind of the dystopian inevitability of something like this short story i wrote once.

on the bicycle as a vehicle to understand marginalizaton

if you're able-bodied enough to ride a bike and otherwise have trouble understanding, from a visceral perspective, the terminology of feminist and antioppression discourse, i have a concrete recommendation: ride a bicycle as your primary means of transportation in a city where this is not the norm.

i don't claim this is a way to automatically transport the experiences of others into your head, and obviously like all analogies it's imperfect, possibly even treading on "oppression tourism" territory, but as a set of concrete experiences to discuss, i think it can help establish some common ground for the sake of getting basic terminology. by way of example, i give the following glossary.

marginalization: when riding a bike you are literally pushed to the margins of the road. if you assert yourself and drive in the middle of the lane, you are constantly put on the defensive and have to ward off motorists challenging your audacity to be there -- even when in fact it's completely legal and the place where you are safest.

victim blaming: people will constantly question your decision to go out, saying "it's too dangerous" and concluding that therefore you just shouldn't do it; anyone who does is taking an unnecessary risk, and if they get hurt, they "should have known better." what you wear (helmet? light/reflective clothing?) will get you further blamed in the case of a traumatizing accident.

[white/male]-as-default, [hetero/cis]normativity: by analogy, car-as-default. if feminism is "the radical idea that women are people," bike advocacy is "the radical idea that bicycles are means of transport." underlying assumptions in personal conversation, marketing, business planning, and urban planning, frequently make the assumption that "transportation = car", and you'll find yourself repeatedly having to think (or say) "hey, what about me?" furthermore, the fact that personal motorized vehicles are the default thing-for-going-on-roads in cities is more historical accident than the "natural" order of things.

microagression: one or two little things that happen (someone honking or yelling at you, someone passing too close or cutting you off) might be shakeable, but if you keep this activity up and endure it constantly, day after day, i guarantee it will wear on you. the person you wind up snapping at might not have even been the most egregious instance, and they may come away with the impression that cyclists are irrationally aggressive people -- because they don't have the context of every other tiny aggression you encountered across the history of your riding, making you constantly defensive and volatile.

intersectionality: it's entirely too easy to think that the issues you have a window onto as a cyclist only pertain to cyclists. and then you start catching yourself doing the same shit to pedestrians (turning in front of them, not stopping at stop signs) that you're upset when drivers do to you, and you start hearing about cyclists being dicks to other cyclists and pedestrians, or you hear a cyclist wonder why everyone doesn't just ride a bike (including the poor, elderly, and disabled?) and you (hopefully!) start to realize that getting around the city sucks for a lot of people and is a way bigger problem than just your subjective view. this is related to the idea that a workable feminism necessarily incorporates all axes of systematic oppression, not just those that incongruently affect women.

on the bicycle as a tool of autonomy

on the flip side of all this, for me personally, the bicycle has been a hugely, astoundingly critical component of my own sense of autonomy and independence. i mean, okay, in some ways it still represents a dependence, but it's a dependence on something i own and control, rather than a dependence on male friends to wait with me at bus stops at night or on someone to give me a ride home -- in other words, having my location be subject to the whims of unreliable external factors. i don't have a sense for how this would compare to just owning a car, but honestly i think it would still win, because of the increased flexibility (ability to stop on a whim, don't have to hunt as hard for parking, can go on trails, gives access to open air/adrenaline from exercise, etc).

in that sense, i think it's an incredible instrument of feminism, and certainly of my own happiness.

for the first time in my life, i did something for father's day: i finally got round to scanning several of the items pertaining to my father that i received from my grandmother during my visit to arkansas two christmases ago.

i was born in may 1986, and my dad died in october of the same year.

( cut for large images )

this n-category cafe article on the mathematically "sacred" and "profane", while not particularly coherent, makes a bunch of really interesting points.

first there is this sociological observation about how mathematicians get to know each other:

When two mathematicians meet and feel out each other’s knowledge of mathematics, what they are really doing is finding out what each other’s bottom line is.

this clip doesn't really draw a distinction between a personal bottom line, though, and that of one's entire field. in terms of personal bottom lines, this rings true for me; the academic conversations i have typically go much better if we get each other's bottom lines out of the way (e.g. i might tell someone i want a programming language for IF, or a type theory for checking asymptotic complexity, or a clean setting where dependent functional and logic programs interoperate). but i'm not sure i could define what the research programme i associate with carries as its bottom line to the tune of "To the algebraic geometers of the sixties, the bottom line was the proof of the Weil conjectures." certainly for complexity theorists, the obvious bottom line is P vs. NP. but type theorists don't have an analogous sought-after result or theory to nail down -- maybe everyone has their pet problem (concurrency, interactivity, space usage, modularity, theorem proving) for which there is some hypothetical "holy grail" language, but certainly we aren't very unified about it. maybe this is part of the solidarity (and consequently marketing) problems that the PL community seems to have, perpetually; we can never really agree on what we're after.

the side remark about "duty" also struck me:

…of the three reasons for choice [because it is useful; because it is right; and, because it is my duty], the third alone is a complete reason. Choice is always choice to do an individual action. Why do I do it? The answer ‘because it is useful’ explains only why I do an action leading to a certain end: not why, among the various possible actions which might have led to that end, I choose this and not another. The answer ‘because it is right’ explains only why I do an action of a certain kind, specified by the rule which I obey; not why, among the various possible actions conforming to that specification, I choose this and not another. But the answer ‘because it is my duty’ is a complete answer.

at first this bothered me, because i wanted to object, "but who assigns you this duty? that itself is a choice" -- until i recast it as a description of how to execute proof search. suppose you have a bunch of clauses in your context and some goal C. any clause with C at its head is "right", but there may be many. any clause that is a precondition to such a clause is "useful", but only because it's an intermediate step. the only way to decide what part of your context to use is to give an algorithm like focusing which forces you to pick, and to follow through on your choice. :P

maybe this can be applied to life as well: the only thing that can really justify an action is a pre-determined choice procedure, and having one, even if it's poor, is better than arbitrarity.

also i think the line "If I show you how my new knife cuts through some wood, I may do so to allow you to admire the sharpness of the blade, rather than because I want two pieces of wood." is good to keep in mind for any discussion of math/programming.

occasionally you'll hear someone ask, "are higher-order functions 'higher-order' in the same sense as higher-order logic?" here is a possible answer.

from my understanding of current logical diction, something like the following story is true:

once upon a time, humans invented lambda calculus. they said, "a function that takes a functional argument (or returns a functional value) is a higher-order function." they wrote that definition down, and then two different humans read it.

the first said, "ah! a 'higher-order' function is one that operates on a function. so, in general, for something to be 'higher-order' means it operates over functions."

the second said, "ah! a higher-order function is a function over functions. to generalize, a higher-order X is an X that operates over other Xes."

error! and from their teachings sprang many logician progeny of both lineages, and the confusion remains.

some examples:
- higher-order abstract syntax. "lam : (tm -> tm) -> tm" is higher order in that "oh look there's a left nested arrow", i.e. we're describing syntax in terms of function types (and for that reason may be better deserving of the abstract higher-order syntax coin).
- higher-order judgment. in twelf lingo we use this to mean, again, a judgment over open terms (like (tm -> tm) -> type) rather than what you might think following generalization (2), a judgment about judgments (i.e. a metatheorem).
- higher-order logic. if we squint for the sake of uniformity and pretend that by "logic" we mean "predicates", then i think it's accurate to interpret this as an instance of generalization (2), predicates over predicates. it certainly doesn't mean "logic about functional data", which is just propositional logic.

despite my NPOV efforts, it might be coming through that i'm a little annoyed with generalization 1. it just seems a little bit provincial or narrow-sighted, like the only thing that we could possibly want to get fancy with is the types of the things we describe, rather than the (quite literally) more judgmental-methodology-motivated notions of our system. of course, in practice, i use the jargon that will get me understood, but if i got to prescriptively reinvent it i'd change the word for generalization 1 to something like "functional" (where of course in this perfect universe, "functional programming" would be renamed to "value programming").

the SPIN paper, which we're reading for 712 (grad OS), drinks the PL koolaid:

"Our decision to use Modula-3 was made with some care. Originally, we had intended to define and implement a compiler for a safe subset of C. All of us, being C programmers, were certain that it was infeasible to build an efficient operating system without using a language having the syntax, semantics and performance of C. As the design of our safe subset proceeded, we faced the difficult issues that typically arise in any language design or redesign. For each major issue that we considered in the context of a safe version of C (type semantics, objects, storage management, naming, etc.), we found the issue already satisfactorily addressed by Modula-3. Moreover, we understood that the definition of our service interfaces was more important than the language with which we implemented them.

"Ultimately, we decided to use Modula-3 for both the system and its extensions. Early on we found evidence to abandon our two main prejudices about the language: that programs written in it are slow and large, and that C programmers could not be effective using another language. In terms of performance, we have found nothing remarkable about the language's code size or execution time, as shown in the previous section. In terms of programmer effectiveness, we have found that it takes less than a day for a competent C programmer to learn the syntax and more obvious semantics of Modula-3, and another few days to become proficient with its more advanced features. Although anecdotal, our experience has been that the portions of the SPIN kernel written in Modula-3 are much more robust and easier to understand than those portions written in C."

yesterday i learned two new games.

1. "google ghost": designate one person to type things in to a google search bar. go around in a circle. the first person says a word, with optional space character after it. then you proceed around the circle, each person saying a character (usually a letter or space). the typist enters each utterance into the search bar, and as soon as google suggest has no suggestions, the person who said the last character loses and picks the next start-word. the best part is hearing all of the pruned-away suggestions every time someone picks a branch.

2. "add-on": another climbing game, sort of like the dual of climbing-horse, where people take turns making moves and simon-says-style repeating all previous moves and adding one at the end. have not actually tried this one yet.

it would be neat if there were a database that classified songs by their chord progressions so that you could look up all songs that use a particular one.

by the way, if you ever want a backtrace in smlnj, here's the ticket:

    CM.make "$smlnj-tdp/back-trace.cm";
    SMLofNJ.Internals.TDP.mode := true;

apparently everyone i've talked to has always been as lazy as i am about doing a google search to discover this, so i thought i'd point it out.