Jason (jcreed) wrote,

Some very useful/interesting meetings/things today.

At lunch Tobias Nipkow talked about verified decision procedures for various theories stemming from quantifier elimination procedures. The thing I took away from it was this lovely notion of "virtual substitutions" which remind me faintly of "leftist substitutions" --- they're kind of substitutions, but kind of not. In his case, you might substitute infinite or infinitesimally-different-from-known-things elements for variables in a theory of a linear order, and you don't leave this exotic objects lying around really, but they collide with atomic propositions and do something there --- I quickly change x < ∞ to top, and x > ∞ to bottom, for instance, before the language of terms catches on that I've diddled with it temporarily. Come to think of it, it's reminiscent of hereditary substitution even more, just in that once you reach the variable, you're not necessarily done with the process of substitution.

After that Anders and I talked unification for a couple hours. I think we went through almost verbatim (with him proposing and me counterexample-producing) all the major failed ideas I had about invariants for the placeholder-based HOU algorithm I came up with, leading right up to the one that worked. He still had some remaining ideas, but I feel good having transmitted the knowledge that I had gained by banging my head against the wall all those months.

David Baelde gave a talk about Bedwyn. Neat stuff, though I am having a continued crisis of faith about what it means to have inductive types in a logic.

Went out to dinner with people kinda late, talked a bit about co-Twelf and termination metrics.
Tags: math, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded