Jason (jcreed) wrote,

Read the chapter on higher-order unification in the handbook of automated reasoning. It's practically in a footnote that yeah, by the way, occasionally eccentric wackos deal with systems where not every type is guaranteed to be inhabited. Sheesh.

Started to go through and TeX up an account of pattern unification with irrelevance around, trying to start from Pientka-Pfenning's account of evars as relative-validity modal variables. The only question that stares me in the face is how to make sure equality and typechecking are still decidable. You can't just raise u :: (A_1, ..., A_n |- B) and u[M_1 ; ... ; M_n ; .] to x : A_1 -> ... -> A_n -> B and x M_1 ... M_n, can you? In any event, I think I had a minor revelation a day or two ago while meditating on the open-world assumption that in fact the right answer to \a\b X 2 = \a\b Y 1 is (X := \a Z, Y := \b Z), since the more complicated terms that might be substituted for X and Y (like cd o (ac 1) and cd o (bc 1)) in the appropriate signatures (like ac : a -> c, bc : b -> c, cd : c -:> d) are obtainable up to definitional equality by substituting (Z := cd o W) for W : c Also: more jazz, more B5.

  • (no subject)

    After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

  • (no subject)

    Went to a series of maker-y talks hosted by Pivotal. The last one, by the woman who runs Genspace, "New York City's Community Biolab" was pretty…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded