Jason (jcreed) wrote,
Jason
jcreed

Last advisor meeting I had Frank was speaking wistfully about the possibility that the positive connectives in linear logic might still have a chance at being encodable in HLF somehow, since what he, quote, "really cares about" is metatheory for CLF.

I discredited the chances of such a thing working, since I'd long ago convinced myself that (a) getting any positive connectives to work right in a labelled setting would be a pain and (b) that they'd turn out to be bunched logic rather than linear logic anyway.

Just to re-convince myself of (b) I sat down and worked out why if you encode linear disjunction as, say, the Church encoding (as Frank was specifically pushing me to think about the church encoding of tensor)

(i) A v B = ∀α (A -o α) & (B -o α) -o α

then you get the typical bunched-logic distributivity properties like

(ii) A v (B & C) = (A v B) & (A v C)

While I was able to get a proof, I was perplexed that when I tried to derive an HLF sequent left rule from the church encoding (i), I kept getting

G, α : w, Ai[α] |- C[α * q]
---------------------------
 G, A1 v A2[p] |- C[p * q]


which (a) is really weird as a left rule for having a conclusion that is at some nontrivial world expression, rather than a world metavariable and (b) seems to disallow equivalences like (ii).

The awesome thing is that I made a mistake! That inference rule is appropriate for the Church encoding of disjunction where the second-order quantifier ∀ only ranges over negative atoms, not over all propositions. This (together with focusing discipline, of course) accounts for demanding a particular world on the right, and for how it can exist side-by-side with "real" disjunction despite apparently sharing the same right rules. (in fact, its right rules are slightly different)

Also, a second-order quantifier ranging over only negative atoms feels much more "predicative" in some sense even compared to one ranging over monotypes. I like it a lot, and I think it might be a really useful stepping-stone idea at least in working out metatheory over positive connectives in linear logic programming.

Also also, this corroborates my existing belief that base-type polymorphism is a useful concept.
Tags: linear logic, math
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