Jason (jcreed) wrote,
Jason
jcreed

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

  • 0 comments