February 27th, 2008

beartato phd

(no subject)

Book club last night was fun: Jenny Guth hosted. We ostensibly talked about Sirens of Titan, and in fact veered off into discussions of countable ordinals, and the bottom-scrapings of the internet.

Today in λ-calculus we gazed deeper into the darkest heart of Stirling's basic definition of the tree-matching game. I tried to unravel it in terms of things I understand better (i.e. a purely contextual definition of the λ-calculus itself, and taking the special case of knowing that there are only first-order constants to avoid this "forbidden constant" nonsense entirely) and had some success. At least I am beginning to see the subtle polarity reasons why you want two substitution lookup tables.