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.
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded