August 7th, 2003

beartato phd

(no subject)

A google search for the ("Statman-Plotkin") lambda definability conjecture turned up a couple messages from mailing list archives that I found amusing historically. One from 1989 explains where the name "logical relations" comes from, and gives some hope as to the conjecture's provability, and Two, from 1995, points out that it is old news that the conjecture is false. I love seeing the workings of mathematics exposed by these kinds of records...
beartato phd

(no subject)

Went to the ConCert meeting in the morning. Karl talked about meta-theorem proving in twelf. Good to review such things with real examples.

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.