I have been playing with a very small variation on the Schalk–de Paiva construction, and it has turned into a rather larger question than I expected. The experiment is almost embarrassingly simple:
Take lineale-valued sets, and replace relations by structure-preserving functions.
That is essentially the whole idea behind a new preprint, Functional Lineale-valued Sets.
Why bother? The original construction, usually called FP-Set, is a remarkably uniform way of producing models of linear logic. You take a set, put values from a lineale between its elements, and use relations as morphisms. With suitable choices of the lineale, you get familiar linear logic models such as phase spaces, coherence spaces, or hypercoherences. Also a whole host of other models that people did not seem to have played much with.
But relations do a lot of the work in the construction. So I wanted to ask a slightly impolite question:
What happens if we take the relations away?
The tensor comes from the lineale. The internal hom comes from residuation. Negation comes from the choice of a dualizing element. Modal structure comes from a storage operator. Even the conditions giving duplicable objects are conditions on the values in the lineale.
In other words, the sets are not providing the linear structure. The lineale is. Most of the structure is "imported" from the codomain, which is a familiar situation in mathematics.
What the functions give us is something different: ordinary categorical structure. Products and coproducts are computed on the underlying sets. Equalizers and coequalizers are available. With a complete lineale, the resulting category is complete and cocomplete.
This is quite different from the relational construction, where the relational notion of morphism is closely tied to the way the structure is built. So the little experiment seems to separate two things which are rather thoroughly entangled in the usual presentation:
the linear structure comes from the values, while the ordinary categorical structure comes from the functions.
This also raises the question of whether there is a linear analogue of the familiar theory of H-sets and Q-sets. For readers who have not met them: an H-set or Q-set is, roughly, a set in which equality is replaced by a degree of similarity. Instead of asking whether two elements are equal, we assign a value measuring how similar, or how equal, they are. These structures grew out of the study in the frame-valued case, and are closely connected with sheaves and topos theory.
This is precisely why they are tempting here. We already have a lineale supplying values between elements, so why not use those values to describe a linear version of “being the same”? And if the resulting objects behaved like their classical H-set/Q-set counterparts, perhaps we could recover some of the beautiful categorical constructions that come with them.
There is a natural way to do this. The off-diagonal values describe similarity between elements, while the diagonal values describe their extent. One can then write down conditions resembling symmetry, transitivity, boundedness and a local identity condition.
At first sight these conditions look nicely linear. But this is where things get more interesting. When you examine what the conditions actually say, most of the apparently linear behaviour has a rather cartesian origin. The local identity condition, in particular, forces the extents to be idempotent. So there is a curious phenomenon:
the conditions look linear in form, but cartesian structure is hiding in their provenance.
And this seems to matter. The tempting next step would be to imitate the familiar tripos-to-topos story and try to build a topos-like category from these linear H-sets, or LinSets. But the local identity condition gets in the way. The problem is not with the doctrine. For a quantale, the usual powerset construction gives a perfectly good linear analogue of the predicate doctrine, and the Frobenius property obtains. The problem appears when we try to build the objects on top of that doctrine.
In the ordinary H-set story, the predicate itself supplies the identity relation. In the functional linear setting, identities are already ordinary functions, and the lineale-valued predicate does not have to be an identity. Requiring it to play that role introduces precisely the idempotence condition that pushes us back towards the cartesian world.
So at the moment I see several possible ways forward. Perhaps one should develop a genuinely functional version of linear H-sets, accepting that some of the familiar universal properties will have to change. Perhaps there are useful conditions under which functions and functional relations coincide. Or perhaps the moral is more radical: a linear completion should not necessarily be expected to look like a topos.
There is also a nice comparison with Dialectica constructions. In a Dialectica category, we have two sorts of data: witnesses and counterexamples. A map evaluates one against the other in the lineale. Here those two sides have been collapsed into one set. So LinSet can be viewed as an extreme case of the Dialectica idea: there is no longer a separate witness side and counterexample side. There is just the evaluation structure on a single set.
And that small change seems to move the crucial assumptions around.
This is why I am sending this one out as a conversation starter rather than as a finished theory. I would particularly like to hear from people who know the H-set and Q-set literature, people who know the linear logic side, and people who have thought about functional relations and topos constructions.
Have I isolated something useful here, or have I simply moved the difficulty somewhere else?
I would be delighted by either reaction: I want to work on this with you or no, this is wrong, and here is why.
No comments:
Post a Comment