Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I started a stub at affine logic as I saw the link requested in a couple of places.
there is a notion of categorical model of affine logic where we only require a natural family of maps $A\to I$ without the tensorial unit being terminal. i added that to the article.
Categorically, affine logic is modeled either by (symmetric) monoidal categories whose tensorial unit $I$ is terminal, or — slightly more generally — by (symmetric) monoidal categories equipped with a family $A\to I$ of arrows (for all objects $A$), which is natural in $A$.
So the first of these is known as a semicartesian category, and the second has a name?
I don’t know of a special name for the weaker definition. But I just saw that Mike added a remark saying that $I$ is forced to be terminal as soon as we require $I\to I$ to be the identity. This is in particular the case if the natural transformation is monoidal. Now I think that this (symmetric?) monoidality sounds like a reasonable requirement anyway. Maybe it corresponds to the preservation of semantics of certain natural cut-elimination rules?
I was just thinking this morning about what the type theory would look like for the case where $I$ isn’t terminal. The best way I can think of to do it is that there is an operation of “weakening by nothing” that is not the identity. So for instance when you weaken $A\vdash B$ by $C$ and then cut with $\cdot\vdash C$:
$\array{ \arrayopts{\rowlines{solid}} \array {\arrayopts{\rowlines{solid}} \vdots \\ \cdot\vdash C} \qquad \array{ \arrayopts{\rowlines{solid}} A\vdash B \\ A,C \vdash B } \\ A\vdash B }$the resulting $A\vdash B$ is not the same as the one you started with, but it’s been “weakened by nothing”. Since that kind of cut generally gets eliminated to the identity, your way of phrasing it in terms of cut-elimination also makes sense.
I like your intuition of “weakening by nothing” that ought to yield the identity. I’m not so sure anymore now that it’s about cuts – compatibility of weakening with cuts seems to correspond to naturality, not monoidality of the transformation.
Anyway, I now think that mere naturality of $A\to I$ – as I initially proposed – is too weak and doesn’t give a good notion of model. In the case of the example that I gave in the article (with empty relations), the result of weakening any proof/relation would yield an empty relation, which would intuitively mean that all information is lost when adding a dummy argument.
What confused me is the comparison to the situation that of a symmetric monoidal category with natural transformations $A\to I$ and $A\to A\otimes A$ satisfying the axioms of commutative comonoids. I think in this setting the category is automatically cartesian, and we don’t have to require the monoidality of the transformations explicitly.
I think compatibility of weakening with cuts on sequents with unary domain is naturality. That is, this:
$\array{ \arrayopts{\rowlines{solid}} \array {\arrayopts{\rowlines{solid}} \vdots \\ D\vdash C} \qquad \array{ \arrayopts{\rowlines{solid}} A\vdash B \\ A,C \vdash B } \\ A,D\vdash B }$reduces to a single weakening by $D$, and that’s naturality. But if $D$ is replaced by an empty context or a context of length $\gt 1$, then I think you get monoidality as well.
Do you want to edit the entry to downplay the merely-natural version?
I agree on the thing about cutting sequents with unary domain, and have amended the article.
Thanks!
Thanks, Todd. I added something to that effect.
Alternatively, it could be considered just an intuitive analogy to how an affine map of vector spaces can “use its argument” zero or one times, but no more (i.e. it can’t square the components of its argument, or multiply two of them together).
Maybe that explanation sits better with Girard’s here
What is affine in “affine logic” ? Take the viewpoint of denotational semantics and consider the intuitionistic version of linear logic, in terms of coherent spaces or Banach spaces. Then the weakening rule introduces fake dependencies, eg constant functions, and when we
combine it with additive features, we get more generally affine functions. That’s it.
Did he coin the term?
1 to 16 of 16