Jason (jcreed) wrote,

I think I finally finished a proof I've been working on occasionally for the last couple weeks. It's not very long, but it's one of the trickiest induction hypotheses I've ever had to come up with. I think the only one that beats it is the crazy labelled deduction callcc nonsense I did some time ago.

It's up on my drafts page as "terminating untyped hereditary substitution". For a quick summary: hereditary substitution works because, although it hereditarily carries out β-reductions, sometimes it throws its hands up and rejects the substitution currently being carried out. This is why it can terminate, even on ill-typed terms, and indeed it will always terminate if you rig it up with a type index.

Now imagine doing things in spine form, but leave off the type index entirely. However, make sure that reduction of a lambda against an empty spine is rejected. It turns out substitution still terminates on all terms, be they well-typed or not! The proofs work by inferring some sort of quasi-typey things from the terms involved, and using them as the induction measure.

I don't know what this result is good for, but it makes me happy to know the answer. At least assuming I didn't make a mistake somewhere...

Also today was practice with n1h2k. We got through more songs than usual, I think, due to effective "let's just get through this list of songs that, seriously, we should all know by know" motivation.
Tags: math, music, work

  • (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