Jason (jcreed) wrote,

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.

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded