| (no subject) |
[Dec. 4th, 2009|11:33 pm] |
Hey, it's a challenge to find big red balloons for DARPA tomorrow! Feels kind of like a Public Option Alternate Reality Game.
Anyway - the setup for MIT's team is an elaborate Reverse Ponzi Scheme of sorts and I have a bridge to sell you especially if you're in some weird random non-Pittsburgh US location (sorry people in Japan or Canada). |
|
|
| (no subject) |
[Dec. 3rd, 2009|02:48 pm] |
Based on ![[info]](http://l-stat.livejournal.com/img/userinfo.gif) _tove's comment here, I kind of want to write a short story about logicrats, the bureaucrats of the future which approve or deny requests for additional proof-theoretic strength within massive government-run software projects written in total functional programming languages. But this is another logicrant.
I wrote this thing about embedding logics in other logics up basically as my own personal intro guide to Jason and Frank's constructive resource semantics stuff (also: unicode Twelf!). Perhaps the only interesting bit is that, in the continuing bumble of trying to understand what the difference between an embedding and an encoding is, I propose this:A logic is encoded in a logical framework by adequately encoding object language propositions as terms in the framework and then by representing object language judgments as propositions in the framework. A logic is embedded in a logical framework by giving a function from object language propositions to propositions in the framework. And the interesting part is, this is kind of what the mysterious hacked up %clause is in Twelf is all about - I've got this one logic (PROOFSEARCH) which I want to embed in another logic (HOL). But the second logic (HOL) does not have good proof-search/focusing/what-have-you properties, so in Jcreed'sthe Hierarchy of Adequacy I want dependent types to ensure that adequacy criteria (1) holds without ever having any hope of adequacy criteria (2) holding. There, I've summarized Dependent Types Ensure Partial Correctness of Theorem Provers for you.
This is an interesting observation because, in HLF, certain metatheoretic properties hold in the object logic (LLF) that do not hold in the metalogic HLF (which maybe shouldn't be called a metalogic in this instance - it's more just a target logic or host logic?) So, whereas in the uses of %clause we wanted to use the more refined proof-search strategy of the object logic, in LLF/HLF we want to use the more refined coverage-checking strategy of the object logic.
Anyway, thus ends the meditation. |
|
|
| Braincruft and zippers |
[Nov. 22nd, 2009|01:53 pm] |
This is a note based on a GatesWall full of logic I wrote down about five weeks ago: Encoding Substructural Logics in a Hybrid Framework - it's also why I started out this logicrant from early October. I've since moved on to a more ambitious project, but I felt like this needed to get finally hacked together, even if it won't ever make sense for anybody but a future version of myself.
I tried writing this down over a month ago and it didn't work, but putting some renewed effort into it over the last three days makes it clearer. I wish I understood better why putting a fairly well-understood idea down on paper sometimes takes 2 hours and sometimes takes 2 months. |
|
|
| Blood donation |
[Nov. 12th, 2009|09:58 pm] |
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. |
|
|
| (no subject) |
[Nov. 12th, 2009|09:56 pm] |
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. |
|
|
| Vote Tomorrow! |
[Nov. 2nd, 2009|07:49 pm] |
I'm going to be spending 14 hours or so running a polling place, the least you can do is spend half an hour and vote! It's a good habit.
You can find your individual ballot at smartvoter.org.
There are actually many fewer endorsements than last time, because the Democratic Party entities kinda obviously just endorse the people that won the Democratic primaries.- State Bar Association judicial election ratings. The summary is that pretty much everyone is recommended except for Marakay J. Rogers, the libertarian candidate (because he didn't play the endorsement process game) and Barbara Jo Ernsberger (because of lack of courtroom experience and concerns about "temperament." Perhaps this involves a story in which she was fined for calling a defense council's paralegal a jerk; her survey goes on to explain why defense council's paralegal was, in fact, a jerk, though using more polite language than that.)
- Allegheny County Bar Association judicial election ratings are kind of confusing - are they just recommending that we don't have a Commonwealth Court?
- Summary of Pittsburgh P-G endorsements.
VOTE, GOSHDARNIT. If you have moved since the last time you voted and didn't update your registration when you changed your drivers license, but you did and you still do live in Pennsylvania, you should be able to do "one last time" voting - vote tomorrow at your old place, but tell them you've moved and need to update your voter registration information. |
|
|
| Observation |
[Oct. 18th, 2009|12:38 pm] |
I listened to (part) of This American Life's healthcare episode yesterday - the last act about how patients put pressure on insurance companies (via politics, mostly) and doctors (via malpractice lawsuit risks, mostly) to do things that don't make sense from a systematic perspective. The first example was customers forcing an insurance company to cave to an expensive health system's demands, thus raising healthcare costs for everyone. The second example was people getting the prostate-specific–antigen (PSA) test that either 1) doesn't help anyone or 2) saves lives, but at the cost of 49 expensive, disruptive, painful, and totally unnecessary treatments for every 1 saved life, depending on which study you follow.
In the latter case, the overwhelming attitude was that people want to do something. But then, again, if everyone gets the PSA test, why doesn't everyone want this H1N1 shot? Because "cancer" will kill you (actually, it won't, not all of the time) and "the flu" won't (actually, it will, even and in some cases especially totally healthy people, some of the time). Instead of pushing the science and educating the public about the controversy and the research, should we start conspiracy theories about how PSA tests give you mercury poisoning and vague, ill-defined but terrifying long-term health risks and causes autism in your children?
And why can only doctors and not parents/individuals get sued for malpractice? CMU will cover your $50 bucks for a flu shot, or your two weeks of sick leave and your insurance when you get admitted to the hospital. What's their recourse when you choose the latter? Maybe I'm stating it wrong, but stated this way it seems like a fundamental asymmetry. |
|
|
| (no subject) |
[Oct. 14th, 2009|10:49 am] |
Now that's interesting. Springer will let your journal paper be Open Access for a one-time fee of $3000 after your journal paper is accepted. It's called Open Choice and I hadn't heard about it. There are two obvious questions: what's the monetary cost of Springer actually publishing your paper, and what's the social value of having your paper be open access? I imagine that both are somewhat lower for an average paper, but I have no evidence of this.
That said, for an open-access diehard, it's a good way to play the academic game and still live your beliefs (for a cost - but hey, that's a cost some people paid to shop at Whole Foods, at least before some fraction of them noticed it didn't make sense). And it starts giving academics real social leverage to push real open access journals: "I'm sorry, I'd normally send this paper to your journal, but I only publish open access. If it gets accepted to you're journal it's gonna cost me three thousand dollars whereas Logical Methods in Computer Science (LMCS), which I perceive to be {as good, better, almost as good} as your journal will publish it open access for free." |
|
|
| Flurant |
[Oct. 14th, 2009|10:10 am] |
Stopped by the UC for a seasonal flu shot yesterday, H1N1 nasal sprays weren't supposed to be available, but they didn't have a big crowd so I got one. They're available to everyone at CMU in the UC from 9:30-4 (or so) Thursday.
I tried to spread this news around - I was shocked by how many people weren't planning on getting a flu shot! Half of the people being hospitalized for the flu were healthy ("Health officials...have said before that the majority of swine flu patients who develop severe illness have some sort of pre-existing condition, but the new data suggest the majority may be slimmer than was previously thought.") This is not a fun and exciting public health adventure, guys.
I was also surprised by the grab bag of information about not getting the flu virus online - most from 2002-2004 when the seasonal flu shot was less effective than usual. This is either one of those cases where there's not a scientific consensus but a consensus group is now (or sometimes) charge (see economics, "supply side," or health economics, "public option") or a place where there is strong scientific consensus but the dissenters can get heard really loudly over the internet (see medicine, "homeopathy," or climatology, "global warming is real").
I am pretty clear "measles vaccine causes autism" is in the latter category, which is why I'm tempted to conclude that anti-flu vaccine people are similar. But the anti-flu shot mentality of most of the people I talked to in the department at least gives me pause. Noone I've talked to has a life-threatening allergy to eggs or any history of Guillain-Barré Syndrome.
And let me be clear what I'm talking about: the statement "sometimes they get seasonal flu wrong or the virus mutates" is OBVIOUSLY correct, but that's a separate issue from "I should be more concerned about the risks (specifically the long-term risks) of getting a flu shot than I am about (say) drinking Diet Coke or donating blood or drinking out of plastic cups," all of which are potentially risky behaviors involving potential consequences that suffer from the scientific condition of absence of proof but not proof of absence. I live my life utterly comfortable with all of those risks, and so there's a pretty low threshold to live up to (15 minutes, a sore arm, and some risk of a slightly runny nose) for any chance of avoiding the flu, seasonal or Novel H1N1. So what's up, people?
P.S. To begin another rant for another time, I pretty much totally reject "there are long-term health risks" as a valid reason for not donating blood. Valid reasons include but are not limited to: phobias, disliking being inconvenienced, being female, low iron, being busy/lazy, I fainted once, and not giving a crap about others - I don't expect anyone to give blood and haven't done so consistently throughout my adult life, I'm merely saying "I am worried about generic difficult to describe long-term side effects" is a nonsensical excuse and am happy to expand on this. |
|
|
| (no subject) |
[Oct. 11th, 2009|02:04 pm] |
Been butting up against a conceptual roadblock and searching for some papers, mostly by looking up papers that cite Huet's paper "The Zipper." The bright side of this is that a lot of said papers are independently very interesting.
The problem has to do with the right way to understand case analysis when we're looking a tree "A" that we know has two subtrees, "B" and "C". Intuitively, either B and C are the same tree, disjoint different trees, B is a subtree of C, or C is a subtree of B.
Oh, wait! I say - but my tree formation operator is really just an AC (associative, commutative) operator, so that I think of this tree as a multiset. Okay, then: now there is one more possibility - B and C overlap some amount without being exactly the same. Five possibilities!
Oh, but now you want to thrown in an idempotent operator (unit) of tree formation - which is the empty set if you're thinking of sets - and all these possibilities generalize into *one* possibility, where there are four sets, Neither A Nor B, B Only, C Only, and B And C Both. The same tree situation is where B Only = C Only = empty, the "B is a subtree" situation is where "B Only = empty" but "C Only != empty", and so on. Or, if you want to look at it this way, I have eight possibilities, since I have eight ways of setting "B Only", "C Only", and "B And C Both" to "empty," some of which may be uninteresting in any given situation. (by the way, this is now the world operator for linear logic)
Oh, but now you tell me that you had it wrong before, that the tree formation operator is associative but not commutative. Okay, well now I can't generalize to just one situation, because now there are constraints, and I have to talk about what is to the "left" and the "right" of something else - if "C Only" is nonempty, then either B is a substring of C, or B is off to the left of C and maybe overlaps, or B is off to the right of C and maybe overlaps. (by the way, this is now the world operator for ordered logic)
Oh, and now you want *two* AC operators, each with their own unit (bunched logic)? It's not clear how to enumerate all the cases there, much less to do so in general given whatever harebrained bunch of tree formation operators you're liable to throw at me next... |
|
|
| (no subject) |
[Oct. 9th, 2009|12:50 am] |
When I last mentioned researchy things, I wrote a little comment about how you could probably encode sequent calculus left rules as essentially forward-chaining rules in a metalogic without concurrent/permutative equality.
Jason asked: Do you believe the encoding in 4.1 to be definitely adequate? Do you have a sketch of a proof, if so? While I haven't done all the work to say "oh yes definitely," I wrote up a more extensive note on why it's probably the case. Still want to extend that note to describe how you'd do the same proof in CLF (hint: replace all the shifts - upshifts or downshifts - with monadbrackets) and what the consequences for adequacy would be (hint: permutive equalities in kind of weird places restricted in what seem to me like arbitrary ways).
[Edit 11:45 Oct 9] Updated the note with CLFey notes, including actual Celf code (thank you Anders).
[Edit 3:12 Oct 9] Updated again to fix a bug and some printing errors. Also have decided to style these Unicode fixed-width notes as "Request For Logic" - so this is RFL #2. |
|
|
| (no subject) |
[Oct. 3rd, 2009|05:58 pm] |
I was re-reading Mismatch by Alessio Guglielmi. I wrote up my own version as a set of quick notes. It's basically an academic rant with two thoughts at the end for solving a problem that I hadn't actually realized Jeff Polakow already encountered.
What's missing at the end is something I haven't really worked out enough in my head: what Jason discovered about being able to represent hybrid Πα:w. ↓β. A@α -> B@(β·α) as linear logic A -o B - then you just get to use the good old linear logic you're used to in the meta-encoding! That's awesome - though I'm a little dubious it works out exactly right in ordered/bunched logic, due to the fact that these logics don't really an unambiguous way of internalizing the judgment stroke and the horizontal line in inference rules. |
|
|
| The riot that started itself |
[Sep. 24th, 2009|11:19 pm] |
From a brief amount of wandering up and down Forbes with Tschantz earlier, listening to sounds out of my window, and reading Twitter, it seems relatively clear that what's happening in Oakland tonight is mostly a milder version of the Super Bowl riots, combined with a vastly more intense response. You get a small seed of an event (a dozen anarchists or five frat boys + a dumpster) to run around do something and then everyone wants to come out and see what all the fuss is about, and pretty soon you have a crowd that needs controlled.
However, usually the frat boys at least need to light something on fire first. But this time, merely gathering at the Schenely Park Drive Bridge is enough to get the police out - you've got Very Important People (TM) nearby and Craploads Of Riot Police Who Weren't Doing Anything Anyway And Are Not Amused (Super Bowl victories put the cops in a good mood too, as they too are Steelers fans!). This means that without even having anything happen you already have spectators waiting for something to happen. Oh! And you've got Eager Media Types Who Want Teargassed Too Like That CNN Guy (TM), which means that more people come by so that they have something to look at, waiting for something to happen. And it's really easy for bored spectators to try to make something happen (Twitter reports that some of the Pitt spectators were throwing things at cops).
There is something oddly refreshing about the insane police presence in Oakland, in that theoretical "people should not fear their government, government should fear their people" sense. Well, congrats - they're obviously more scared of us than we are of them this time around - and the group I just referred to (kinda inaccurately) as "we" consists almost entirely of bored Pitt undergrads.
And PS there is a place in Purgatory reserved for whoever broke Pamela's.
[Update] I found a police scanner website which is kind of the best thing ever. The police said "intel" suggested people were massing near the Hot Metal Bridge. The "intel" was probably (or at least could easily have been, based on what I was reading) Twitter, which paints this really wonderful picture of police and civilians on the streets talking on the radio and Twittering, and then other police reading Twitter and talking on the radio and other civilians listening to the radio and Twittering.
[Update 2 - 12:28AM] Oh frabjous day!!! On the police scanner, they're saying that it WAS "Twitter intel," that the "Twitter intel's been pretty good so far," and the best part is that according to the police at the Hot Metal Bridge no one is at the Hot Metal Bridge. Twitter user resistg20 made this tweet at around midnight - either they were trying to regroup and failed (because it was always just Pitt students anyway) or else they were trying to throw the police off of the students in the Pitt dorms and were wildly successful. Either way, WIN.
[Update 3 - 12:56AM] 2 tweets that make me love the internet:- SCANNER JUST SAID : BE ADVISED WE'RE BEING MONITORED BY ANARCHISTS THROUGH SCANNER #G20
- #g20 #resistg20 DO NOT TWEET YOUR LOCATIONS! POLICE ARE MONITORING TWITTER.
|
|
|
| (no subject) |
[Aug. 25th, 2009|12:51 pm] |
Hey, if you are in Mike Doyle's congressional district (if you go to school at CMU and voted here for the last election, the answer is "yes", by the way) you should fill out this really short survey on health care reform. Seriously, it's a congressman using the Internet to try to understand our opinions. At the very least we should do it just for that. |
|
|
| Breaking Even at the Rivers Casino |
[Aug. 20th, 2009|09:04 am] |
After some delicious Kaya last night, Rachel and I went with MPA to the new Rivers Casino. My reason for doing so was SCIENCE: Rachel and I go to Dave and Busters on occasion to trade money for dopamine in a sophisticated manner that involves trivia and skee-ball and those little coin flippy machines. Which, at that level of abstraction/cynicism, is basically what slot machines do. (The RadioLab episode "Stochasticity" has a heartbreaking story of how this works to catastrophic effect if you're being treated for Parkinson's.) So, the test was to lose n dollars at the casino and n dollars at Dave and Busters and evaluate the relative enjoyment. No one really expected the casino to win, but it seemed worth a try (for SCIENCE!), and beyond that seemed like the correct level of abstraction/cynicism on which to evaluate a casino.
Of course, the casino, like all casinos, was good at getting us in the door: the parking was free (even though there was a baseball game at PNC park next door) and we walked down many flights of stairs and into the big front revolving door. Now, Rivers Casino is really just Rivers Big Warehouse Of Slot Machines, which we knew going in - that's all that they were approved for (shrug). Well, we had initially set n=20, but decided to start by just cleaning up the change in my car, which amounted to four dollars.
First problem: none of the machines actually accept any change. They all accept bills only (well, and "Frequent Player" cards which is just creepy). So we try to turn coins into dollars, but second problem: there's only one line out of the four cashier lines that lets you turn change into dollars, but all this time MPA has been trying to tell me he has four dollars so we trade coins for dollars. Then we try to put the dollars into various machines (including the penny slots, which eat one penny per round if you do it right). Third problem: the machines only take five dollar bills. Not only does that represent one quarter of our maximum combined n - I didn't come to this hyperactive blinking light room to sit down and play one machine some absurd number of times (expected value much higher than 500).
So there we were, walking from machine to machine and putting a dollar bill in and - BAM, the machine blinks and flashes and gives us the dollar bill back. At some point we decided that this had either been the most (we broke even!) or least (we didn't, strictly speaking, ever play slots) successful episode of slot machining we could have expected. In retrospect, we should have gotten a complementary beverage so we could claim to come out strictly ahead, but we cut our (metaphorical only!) losses and left. Rivers Casino did not want our money. Literally! We even tried to give them our money in multiple forms!
But man, that's a big old fancy warehouse full of blinking lights, ya'll. |
|
|
| UID Fail |
[Aug. 16th, 2009|01:25 am] |
So, in my quest for a reasonable way to manage the archives of the CMU PL Reading Group ("Concert"), I threw together a PHP system that reads out papers from a group on CiteULike, sorts them by date (sympathetic to the idea that we might read a paper more than once, or more than one paper on a given day), and gives a listing of read papers (warning: this link will probably break before too long).
In entering non-existant papers into CiteULike, I have run into a few curious corner cases, but this one takes the cake. Simon Peyton Jones, along with Washburn and Weirich, wrote a paper on "Wobbly Types" that got rejected to POPL 05. According to Jones,After thinking about it a lot more we greatly simplified the type system, and wrote "Simple unification-based type inference for GADTs" above. However, the original version has been cited quite a bit, so we made it into a Penn technical report, available from this page. ... which is where it gets interesting, because they list it as technical report MS-CIS-05-26. But it's not! As you can clearly see here, that "unique identifier" belongs to "Dynamic Translation as a Systems Service" by Marc L. Corliss, Vlad Petric, and E Christopher Lewis. Luckily, I guess, that paper was published in a workshop paper that wasn't really cited, so the namespace conflict doesn't really come into play, but it definitely exists. |
|
|
| Whole Foods, free markets, and PR |
[Aug. 15th, 2009|06:45 pm] |
Wouldn't fit in a Twitter, but: I actually agree with Lanny Davis here. That said, I have shopped at Whole Foods maybe twice (at least once) in the past one or two years, and the reason for this is that I'm not really interested in paying extra for food when 1) there are really obvious convenient alternatives and 2) the premium is going to the pockets of people who seem to be interested in using said money in their pockets to fight unions and equitable approaches to healthcare.
The way I see it, that's not a boycott, that's a decision. A boycott, insofar as I understand boycotts, is a protest, you expect someone to change their ways or you want to make a big fuss to right some wrong. It's not that the management of Whole Foods is doing anything wrong! They have every right to be libertarians on any issue they want, and more power to them. If I go back to eating beef I'll probably buy it from them (see point #1 above about substitutability), and if everything wasn't really quite expensive I'd see no problem in buying whatever from them (see point #2 above about the premium). There's noting to protest!
I have been impressed, I guess you could say, at the success of the PR job that, in my view, convinced a lot of people that the crunchy-granola image Whole Foods projected meant that the extra money they were spending on that apple that was sold for less right down the road at Trader Joe's, Giant Eagle, or pick-your-local-wholesale-market was morally as-good-as-being donated to the Obama campaign or something. I guess people who bought the PR and feel like they have been lied to feel like they have something to protest, hence the boycott mentality, but I only have limited amounts of sympathy for people who have happily paid above market prices for goods based on what marketing told them.
I guess it's like if I had bought my Apple computer thinking that the extra cost was because their of the company's decades of commitment to environmental causes and was devastated to learn that it was actually because of their kinda-monopolistic vertically integrated control over their operating system. Or something, I dunno. |
|
|
| (no subject) |
[Aug. 13th, 2009|02:14 pm] |
So our new building, GHC, shares an acronym with the Glorious Haskell Compiler. What would it be like to go to grad school in other compilers?- MLton - you aren't allowed to publish intermediate results, and your thesis may take 8 years and 400 pages, but it will probably win awards.
- SML-NJ - you frequently publish, but the feedback you get from reviewers is usually cryptic if not weirdly apologetic
- .NET - You can write papers however you want, but they will be automatically translated into Esperanto.
- Agda - All work is done under the direct supervision of your thesis committee; you must frequently ask then for advice and then wait while they confer and tell you want their current expectations are
- Prolog - everything is fine, except that all scientific communication happens in iambic pentameter and/or limerick.
Other proposals? |
|
|