Reading a Statman-Dowek paper (CMU-CS-92-152, amused me that it's exactly ten years before the big ol' ConCert tech report, down to the same tech report number) on finite completeness for lambda-models. Really good stuff. Also got a copy of the Schmidt-Schauß paper from CADE'03, which is apparently not online anywhere. Lame! But a good paper judging it by its content. There's this lemma showing that, under the right circumstances, two terms always behave the same if you feed them to another term just in case they always behave the same if you contrarily feed another term to each of them. This leads to a lovely corollary that if only you could decide λ-definability for finite models (the Statman-Plotkin conjecture), then higher-order matching would be decidable. Sadly, as pointed out, the hypothesis fails. Thanks a heap, Loader! Well, I guess it's not his fault --- he only proved it does. Since I'm a good Platonist, I guess he can't be held responsible for its falsehood.
Made some burgers for dinner. Then sally called asking if I was hungry. I've had very bad timing lately, eating just before others want to eat.
Watched some "Family Guy" at
techstep's house. Man, what a great show.