I have just put up a new preprint, Polynomials with Predicates: a Dialectica Reading. It started from a fairly simple observation: if you take a Dialectica object and forget its predicate, what remains looks very much like a polynomial.
But the more I looked at the comparison, the more I thought the interesting story was actually the other way around.
Polynomial functors give us a useful language for seeing the shape of structures that Dialectica has been carrying for a long time. They do not replace the Dialectica construction, because they forget precisely the part that makes it logical: the predicate saying which witnesses withstand which challenges.
And the comparison becomes particularly interesting when we look at dependence and sequencing.
Witnesses, challenges, and shape
A Dialectica object consists of witnesses, challenges, and a relation saying which witness withstands which challenge. There is an obvious interaction pattern here. A witness is chosen; a challenge is presented; and the predicate tells us whether the witness swins the challenge.
If we forget the predicate, the witnesses become the positions of a polynomial and the challenges become its directions. The forward map on witnesses and backward map on challenges are exactly the shape of a polynomial morphism. So a polynomial is, in this sense, the shape of a Dialectica object.
It records who chooses what and what may depend on what. It does not record whether the resulting interaction succeeds. That distinction is important throughout the paper.
A familiar collection of connectives
Once we look only at the shape, most of the polynomial operations on monomials line up with Dialectica linear logic connectives. But this is not a correspondence that starts with the recent polynomial literature.
The main Dialectica connectives go back to the original Dialectica construction in the late 1980s. The ordinary tensor, additive conjunction, and implication already appear there, together with their characteristic witness/challenge asymmetry.
Then, in 1993, Blass introduced another tensor in which the challenge to one component may depend on the witness chosen in the other. The pre-existing cross-product of the Girard Dialectica construction gives the corresponding two-sided dependence.
So there is a first chain:
ordinary tensor → Blass tensor → cross product
where the successive steps allow more dependence of challenges on witnesses. But there is another chain, going in the opposite direction. Instead of making challenges depend on witnesses, we can make witnesses depend on challenges:
ordinary tensor → ◁ → par.
The middle operation is the one I want to emphasize. The two chains are not independent: linear negation swaps witnesses and challenges, so it swaps the chains term by term, and ◁ is the dual of Blass's tensor — which is how one could have known the connective was there before anyone wrote it down.
Sequencing is not new
The operation ◁ says that the witness for the second component may be chosen in response to a challenge to the first. In plain language:
first play A, see how A is challenged, and then choose how to play B.
This is precisely the sort of dependence one expects from sequential composition. But I want to stress something that could easily be obscured by the polynomial terminology.
This sequential understanding is not new in this paper.
The sequential construction already appeared in the Dialectica models of state, and in particular in my 2014 paper Linear Logic Model of State Revisited. The sequential modality and the distinction between parallel and sequential use were already there.
The present paper is not discovering sequencing by looking at polynomial substitution. Rather, polynomial substitution gives us a particularly clean way of recognizing the shape of a sequential Dialectica connective that was already present.
This is one reason I like the comparison. It tells us that the polynomial operation is not the source of the logical idea. The logical idea was already there; the polynomial viewpoint makes its shape easier to see.
The history of ordered contexts is older still
There is another piece of history that belongs here. The ordered-context story is not something that has been invented to justify the current categorical terminology either. The relevant orders are the series-parallel orders: start with a point, combine things side by side, and combine things in sequence. The work of Béchet, de Groote and Retoré in 1997 gives the relevant axiomatization of the inclusion between these orders.
This matters because the later categorical picture is not introducing an arbitrary notion of “before”. There is already a well-understood combinatorial structure behind the ordered contexts. The linear-logic models of state paper put this order into the logic; the present paper puts the corresponding dependence into the shape of the Dialectica object.
From the two chains to interchange
Once the two tensors are seen together, something rather nice happens. We have the ordinary, parallel tensor and the sequential tensor ◁. There is a natural map from parallel to sequential combination: a witness chosen for the second component independently can simply be regarded as a sequential strategy that ignores the challenge to the first.
More importantly, there is the middle interchange law
(A ◁ B) ⊗ (C ◁ D) → (A ⊗ C) ◁ (B ⊗ D).
In words, two processes that each have an internal order can be run side by side and then resequenced. This is exactly where the series-parallel story comes back in. The point is not that we have discovered yet another useful natural transformation. The point is that the old ordered-context structure tells us that this is the right transformation to look for. Once the two monoidal structures share a unit, the middle interchange contains the other ways of adding order as special cases.
So the categorical statement that the Dialectica construction carries a normal duoidal structure is really organizing several pieces of older logic and category theory into one picture.
Then reuse follows
There is a final consequence that I particularly like. The usual exponential modality ! corresponds to reuse in parallel. Its challenges are finite multisets: the order in which things are reused is irrelevant.
The sequential modality † corresponds to reuse in sequence. Its challenges are words: now order matters. Again, neither of these ideas is new. They already occur in the earlier Dialectica models of state. What the present organization shows is how they fit together.
Because the two tensors are related by the natural map above, the comonoid structure for the ordinary tensor gives a comonoid structure for the sequential tensor as well. In particular:
whatever may be reused in parallel may also be reused in sequence.
What had appeared as another structural requirement in the models of state becomes a consequence of the relationship between the two tensors. That is, for me, the real mathematical payoff of the paper.
So what do polynomials contribute?
Not the logic. Not the predicate. Not the idea of sequencing. What they contribute is a good way of exposing the shape of dependence.
The two chains
challenges depend on witnesses
and
witnesses depend on challenges
make a collection of Dialectica connectives much easier to organize. They also make visible the intermediate operation ◁ and its relationship with polynomial substitution.
But the predicate still matters. Two Dialectica objects can have exactly the same interaction pattern and therefore exactly the same polynomial shape, while differing completely in which witnesses withstand which challenges.
That is why the title of the paper says Polynomials with Predicates. The polynomial tells us the shape.The predicate tells us what that shape means.
And the historical point is worth making explicit: the main Dialectica connectives appeared in 1989; Blass's tensor followed in 1993; the series-parallel analysis appeared in 1997; and the sequential Dialectica construction was already present in 2014. The polynomial viewpoint comes later.
What is new here is not the invention of these structures, but the way of putting these pieces together and seeing the polynomial structure underneath them. For me, that is the useful lesson of the comparison: sometimes a new vocabulary is most valuable not because it gives us a new construction, but because it lets us recognize the structure that was there before.
(Hermann and Marcelo from work on Linear Logic Model of State, 1996)
No comments:
Post a Comment