Last time I left the dangling problem that my thesis had something to say about the combination of substructural types with dependency, but only for (focusing-)negative types. I want to now summarize the thinking I did in the few years or so after I graduated, which crystallized into a decent story for how positive types worked as well.
If you want a better, longer version of this part of the story, check out anything Pfenning has written on the subject, for example these OPLSS notes. But I'll try to give a very high-level picture of what focusing is, and how it informs what I wanted to figure out about linear logic.
Historically what focusing was when it was discovered — and it's still a pretty reasonably close-central part of What It Really Is as far as I'm concerned even knowing what I know now — is an optimization technique for proof search. It is, in a way, a complement to an even simpler-to-explain optimization that was well-known before, which is simply that some rules for some logical connectives are invertible.
For example, the sequent right rule for $\lol$, \[ \Gamma, A \prov B \over \Gamma \prov A \lol B \] has the property that if the bottom line of the rule is true, then so is the top — and since the rule, by definition, says that if the top holds, then the bottom, that means merely that we have an if-and-only-if between the top and bottom. This is a proof search optimization because whenever we are trying to find a proof for $\Gamma \prov A \lol B$, we can always safely decide that the proof we're looking for ends with the $\lol$ right rule, and continue trying to prove $\Gamma, A \prov B$ as a subgoal: we never have to wonder if we were supposed to pick some other rule first, so we can prune away from our proof search all the searching that we might have otherwise done for proofs that don't end with $\lol$-right.
It's pretty easy to prove that this if-and-only-if holds, by using the cut-admissibility property of linear logic, \[ \Gamma \prov A \qquad \Delta, A \prov C \over \Gamma, \Delta \prov C \] and the identity property \[ \over A \prov A \] for if we have a derivation of $\Gamma \prov A \lol B$, then we just construct a derivation $A\lol B, A \prov B$ using identity and the left rule for $\lol$, and cut the two together to get $\Gamma, A \prov B$.
Similarly, we find that rules like the left rule for $\tensor$ \[\Gamma, A, B \prov C \over \Gamma, A \tensor B \prov C\] and the left rule for $\oplus$ \[\Gamma, A \prov C \qquad \Gamma, B \prov C \over \Gamma, A \oplus B \prov C\] and the right rule for $\&$ \[\Gamma \prov A \qquad \Gamma\prov B \over \Gamma \prov A \& B\] are invertible. Generally we tend to find that the commonest situation is that for every connective, one of the left or right sequent rule for it is invertible, but not the other.
This suggests that there are two underlying kinds of propositions, the positive (those whose left rules are invertible) and the negative (those whose right rules are invertible). What focusing is, is a further optimization on top of "eagerly decompose invertible rules": it tells us that when we start decomposing a positive connective, we should eagerly keep decomposing all the subpropositions of it, as long as they still positive connectives. And likewise when we start decomposing a negative connective, we should keep decomposing negative connectives until we hit something that isn't negative.
What this means is that a proposition made of a bunch of positive connectives only (or negative connectives only) behaves nicely as if it were a single $n$-ary logical connective that can itself be given first-class well-behaved sequent left and right rules, while a mixture of negative and positive connectives usually can't. For example, $A \tensor (B \oplus C)$ can be construed as a single connective, by saying that its left rule is \[\Gamma, A, B \prov D \qquad \Gamma, A, C \prov D \over \Gamma, A \tensor (B \oplus C) \prov D\] and its right rules are \[\Gamma \prov A \qquad \Delta \prov B \over \Gamma, \Delta \prov A \tensor (B \oplus C) \] \[\Gamma \prov A \qquad \Delta \prov C \over \Gamma, \Delta \prov A \tensor (B \oplus C) \] Note that these rules are obviously sound with respect to ordinary linear logic proof rules, but they're not obviously complete. The right rules tell us we need to commit to a division of the context into $\Gamma, \Delta$ and a choice of $B$ or $C$ at the same time. Trying to prove $A \tensor (B \oplus C)$ in linear logic as usual, we have the freedom to interleave those choices with other decompositions elsewhere in the sequent.
The punchline of focusing is that these sorts of mega-connective rules are complete, and the higher-level moral of the story is that paying attention to whether propositions are positive or negative is crucial to understanding what they mean and how they compose.
| Positive Propositions | $P::=$ | $\dns N \celse P \tensor P \celse 1 \celse P \oplus P \celse 0 \celse \cdots$ |
| Negative Propositions | $N::=$ | $\ups P \celse N \& N \celse \top \celse P \lol P \celse \cdots$ |
Last time, I talked about realizing that a substructural proposition was not a thing of kind type but more like a thing of kind \[w \to \rtype\] for $w$ being an abstract monoid structure.
What I realized was necessary to explain what positive substructural propositions were was refining the unpolarized type $w$ into positive and negative versions of it. In this paper that I wrote with Frank, (the so-called "ill-fated paper", since we could never seem to get reviewers that didn't viscerally dislike the idea of "constructive semantics") we called them worlds (positive) and frames (negative) but this is a little confusing, since I was calling the unpolarized things 'worlds' to start with. So let's say that we have two types, $w^+$, the type of resources, (which might equally well be called 'positive worlds') and $w^-$ the type of frames (or 'negative worlds').
Given the existence of those things, I can say that what a positive substructural proposition is, is something of kind \[ w^+ \to \rtype \] and what a negative substructural proposition is, is something of kind \[ w^- \to \rtype \] The algebra on these pals is only slightly more elaborate than before. The type $w^+$ still has a monoid structure $(\tensor, 1)$ on it, and there's additionally an operation \[\lol : w^+ \to w^- \to w^-\] and a relation \[\tri : w^+ \to w^- \to \rtype\] and the requirement that there's an "adjunction" isomorphism \[ (\alpha \tensor \beta) \tri \phi \cong \alpha \tri (\beta \lol \phi) \] for any $\alpha, \beta : w^+$ and any $\phi : w^-$.
I have to confess here that if you read ill-fated paper, you'll see that things weren't actually this clean at all; I'm sneaking in some features of a later version of this idea. In the original, negative propositions were translated "at a positive world $w^+$" and negatives were translated at... a continuation taking a positive world and returning a destination-language proposition. The reason for this confusion is that I was still hampered by trying to translate into negative propositions in the destination language, which required dualizing more things than necessary.
A much nicer way of doing things, which I wrote down a few years later in some detail, is to translate everything into positive propositions in the destination language. When we do this, we get simple semantics-clause-esque explanations of logical connectives, consistent with the "what a (positive/negative) proposition is is a ..." claims above.
Take the logical connective $\lol$: It's suppose to take a positive proposition $P$ and a negative proposition $N$ and yield a negative proposition $P \lol N$. We therefore assume $P : w^+ \to \rtype$ and $N : w^- \to \rtype$ and define $P \lol N : w^+ \to \rtype$ as \[(P \lol N)(\alpha) = \exists (\beta : w^+) . \exists (\phi : w^-) . (\alpha = \beta \lol \phi) \land P(\beta) \land N(\phi) \] Similarly, for $P_1 \tensor P_2$, we can make an almost identical looking definition except for the different polarities involved: \[(P_1 \tensor P_2)(\alpha) = \exists (\beta_1 : w^+) . \exists (\beta_2 : w^+) . (\alpha = \beta_1 \tensor \beta_2) \land P_1(\beta_1) \land P_2(\beta_2) \] And since polarity-shift connectives exist in this syntax, we need to provide an explanation for them, as well: We say \[(\ups P)(\phi) = \forall (\alpha : w^+) . P(\alpha) \imp (\alpha \tri \phi)\] and \[(\dns N)(\alpha) = \forall (\phi : w^-) . N(\phi) \imp (\alpha \tri \phi)\]
These definitions may seem a bit opaque and weird, but the big end-of-the-day touchstone theorem you can prove about them I think is pretty cool: that they constitute a constructive semantics of linear logic, that is, a translation of it into vanilla (i.e. no linearity) focused first-order intuitionistic proof theory, in such a way that you not only accurately model when a linear logic proposition is provable, but also the set of its focused proofs.
And having said that, I think I've almost set myself up for explaining what the original tweet was talking about next post, or perhaps the post after that...
(Prev: "Everything I've Learned About Logic in the Last Decade or So, Part 2")
(Next: "Everything I've Learned About Logic in the Last Decade or So, Part 4")