October 10th, 2003

beartato phd

(no subject)

Oh my god the listening exercises for japanese are long and painful. I really should not put them off until the last day next time.

Good news is I think I have a way around the non-well-founded induction; I believe (inasmuch as hazy 3am ceiling-staring is to be trusted to generate correct proofs) that the objects unification pulls out in my case are guaranteed to have the right type anyway, so I don't have to recursively call the typechecker on something that isn't necessarly smaller.
beartato phd

(no subject)

Bleh. I think this is one of the most ugly type declarations I have ever made:
c--x:(Π-w:o.a w).Π-z:o.Π[i]y:(a·(d+·(*;x z))).a·(d+·(*;y))

Nonetheless, it serves as a useful counterexample to the approach I was trying earlier. Trying to typecheck
Y Y : a· (d+ · (*; Y Y))
where
Y = λ w . c- · (w;w;*)
leads to an infinite loop.

There had better be a workaround along the lines I was thinking last night, or else I'm kinda hosed.
beartato phd

(no subject)

My left hand hurts like hell, but it was for a good cause. Music with dave and victoria was really good tonight. I could just hear things without too much effort, and respond to them, and improvy suchlike things. Dave reminded me of the alternation between F#m7 and G#m7/F# that Coltrane's "Favorite Things" uses. With the right voicing it sounds really nice. I also had some fun after everyone else left with a swing (1-1-1-5)/8 rhythm thing arpeggiating up AEAC and CGCE.

Research is chugging along, still, I think, towards completion. As opposed to up a blind alley.