Jason (jcreed) wrote,
Jason
jcreed

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.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 2 comments