January 28th, 2007

beartato phd

(no subject)

Got some work done today, but not as much as I should have.

Round about 10pm I went to a little jazz show at AEΠ, which is in fact I think some sort of fraternity rush event, but damn if I care about that. These kids were pretty fuckin' tight. I have never before heard "so what" and (what if memory serves correctly was) "mr. pc" with so much funk punched into them. Also "well you needn't" and "st. thomas" sounded very nice, and they played a metric cussload of awesome blues. Ran into friend-of-relaxatorium's-from-Boom-Pam-concert whose name is Annika or something I think, and gustavolacerda.
beartato phd

(no subject)

Here is a spanish joke for keithlard, since he posts them from time to time, got from language log: (sorry if you've heard it before :)

Un señor con una esposa muy habladora lee en el periódico un estudio científico que asegura que las mujeres usan cada día unas 20.000 palabras, mientras que a ellos les bastan 7.000; el hombre enseña la noticia, feliz de poder demostrar que ella es un loro. “¿Lo ves?”.“¿Y no será porque tenemos que repetir mucho lo que decimos?”, dice ella. “¿Cómo?”, responde él.
beartato phd

(no subject)

I think I finally finished a proof I've been working on occasionally for the last couple weeks. It's not very long, but it's one of the trickiest induction hypotheses I've ever had to come up with. I think the only one that beats it is the crazy labelled deduction callcc nonsense I did some time ago.

It's up on my drafts page as "terminating untyped hereditary substitution". For a quick summary: hereditary substitution works because, although it hereditarily carries out β-reductions, sometimes it throws its hands up and rejects the substitution currently being carried out. This is why it can terminate, even on ill-typed terms, and indeed it will always terminate if you rig it up with a type index.

Now imagine doing things in spine form, but leave off the type index entirely. However, make sure that reduction of a lambda against an empty spine is rejected. It turns out substitution still terminates on all terms, be they well-typed or not! The proofs work by inferring some sort of quasi-typey things from the terms involved, and using them as the induction measure.

I don't know what this result is good for, but it makes me happy to know the answer. At least assuming I didn't make a mistake somewhere...

Also today was practice with n1h2k. We got through more songs than usual, I think, due to effective "let's just get through this list of songs that, seriously, we should all know by know" motivation.