Random math burbling

Jan 11, 2007 22:23

I talked to John today, and realized that my denotational semantics for my little language makes no sense. I'm only half-annoyed by this, because it means that I'll have to learn domain theory properly in order to fix it, and to learn domain theory I need to get comfortable with category theory, because domain theory is a PITA without the language of categories to keep things well-organized. And category theory is something I've been telling myself I should properly learn for, er, ever since I first started here.

As an additional motivation, I talked with jcreed last night, and he showed me his incredibly cool explanation of all possible logical connectives (except conjunction and disjunction). It is clearly begging for a treatment using the language of operads, which means that he is cooking up a way to integrate the judgmental approach to defining logics with the categorical. Since these are the only two methods I know to keep myself from designing broken logics, having some way of sanity checking in both directions would be very keen. It would also mean that I could write a paper that only jcreed, John Baez, and Jean-Yves Girard could understand, which would be awesome (if damaging to future career prospects).

Also, a picture of a smiling baby for that sad and tiny minority of people who don't care about formal logic:



Previous post Next post
Up