May 10th, 2006

beartato phd

(no subject)

Been feeling increasingly sick today since about noonish. Finding it kind of hard to sustain much of an attention span through stabby stomach pain, but I read enough of [Miller Nadathur Pfenning Scedrov '89] to kind of grasp that the point of hereditary Harrop formulae is that they are the sublanguage of sequents where it's safe to always focus on the right if at all possible. (i.e. if you don't have an atomic proposition there) At least I hope that's right, because that's the conclusion I came to.
beartato phd

(no subject)

Feeling less sick. Found a crazy paper by Lambek connecting coherence theorems to cut elimination theorems. It's very old (1968) so I'm kind of suprised I hadn't heard of it. I guess there's not a huge overlap between the syntactic people (the ones who love cut elimination) and the categorical-semantic people (the ones who love coherence theorems) so it's sort of unlikely to be anyone's favorite paper.

I also got some progress on figuring out what the categorical semantics of my little system is. It's looking like I don't need to add too much extra junk to the existing local cartesian closed structure that needs to be there already for dependent types. I mainly need a monoid object M × M → M ← 1 with a suitable action, and maybe a couple other isomorphisms that have to hold. The action follows noticing that Hom(Γ, M), the hom-set of generalized elements of M, inherits a monoid structure for every particular Γ, and the condition is then that this monoid acts *Γ on the objects of the slice category C/Γ. I have a feeling there is a snappy category-theory way of saying this without explicitly naming the Γs, but damned if I know what it is. The snappiest I can get is saying that it's a functor Hom(Γ, M) → End(C/Γ). The only other condition I feel pretty confident about goes like this: since we live in an LCCC, there is for every Γ a right adjoint ∀ to the pullback functor along the projection Γ × M → Γ. Now ∀ takes types over Γ × M to types over Γ. This type constructor (which is what you'd use to interpret world quantification) definitely ought to be compatible with the monoid action: I think what I need to require is some canonical isomorphism (∀ f) *Γ p ≅ ∀ (f *Γ×M (p ∘ π1)) for any world p : Γ → M and type f : X → Γ × M.

Played some music in Morewood later, saw a lot of people walking back and forth with boxes. I wonder if they're students moving in for the summer, or hired. student-age staff installing the microfridges for the freshmen or something. I did see a lot of microfridges.