Jason (jcreed) wrote,

So last night I had this insighty-seeming idea, but I've yet to make it pay off. I've been struggling with the conflict between two approaches to getting labelled deduction to work with dependent types; one seems suitable for representing bunched logic, the other for linear logic. I thought I could get away with just pursuing the latter approach in order to get the example I want to work (the representation of the cut elimination theorem for linear logic) but the thing that showed up during my advisor meeting makes me think that certain "bunched"-like features are actually required.

The difference between the two is that in the "bunched" style, hypotheses in the context are decorated with resource expressions, and in the "linear" style, they are decorated with merely resource variables, sort of a special case of the former. However, if the whole system is in this special case, the cut principle is different, and the left/elimination rules for additive conjunction are different. So lately I've been focussing on the meaning of additive conjunction in the two systems.

The idea I had last night was that linear &, with respect to bunched ^, has a property that is kind of like intuitionistic logic with respect to classical logic on the conclusion side of the turnstile. The commitment to one choice or the other is like the commitment to one intuitionistic disjunct or the other. Bunched logic lets you keep both conjuncts around, and classical logic both disjuncts. This bolstered my feeling that linear & ought to be something kind of like @A ^ @B for some possibilityish modality @, by analogy with the modal translation of intuitionistic into classical logic, or else maybe ^ is representable as #(A & B) for some operation # that throws away information kind of like double-negation does.

These are really just hazy intuitions, though; setting up a system that actually satisfies cut elimination is being really hard. There's so many places, in the usual game of pushing around the bubble-in-the-wallpaper of proof obligation, for the bubble to hide.

Better stop before I reach Girard-like levels of crazy metaphors...
Tags: 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