# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDavid_Corfield
• CommentTimeAug 13th 2016

I started a stub at affine logic as I saw the link requested in a couple of places.

• CommentRowNumber2.
• CommentAuthorJonasFrey
• CommentTimeAug 14th 2016

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.

• CommentRowNumber3.
• CommentAuthorDavid_Corfield
• CommentTimeAug 16th 2016

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?

• CommentRowNumber4.
• CommentAuthorJonasFrey
• CommentTimeAug 16th 2016

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?

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeAug 16th 2016

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.

• CommentRowNumber6.
• CommentAuthorJonasFrey
• CommentTimeAug 16th 2016
• (edited Aug 16th 2016)

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.

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeAug 16th 2016

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?

• CommentRowNumber8.
• CommentAuthorJonasFrey
• CommentTimeAug 17th 2016

I agree on the thing about cutting sequents with unary domain, and have amended the article.

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeAug 17th 2016

Thanks!

• CommentRowNumber10.
• CommentAuthorDavid_Corfield
• CommentTimeAug 18th 2016

Is it worth saying why ’affine’? Girard tries to do so here but I can’t say I’m much the wiser from that:

I see there are also ’affine types’ here:

Affine type systems ensure that every variable is used at most once by allowing exchange and weakening, but not contraction.

• CommentRowNumber11.
• CommentAuthorTodd_Trimble
• CommentTimeAug 18th 2016
• (edited Aug 18th 2016)

My understanding is that the name comes from the archetypal model, viz. the symmetric monoidal category of affine spaces and affine maps over a field $k$ (fourth example here). We had a discussion about this back in January, here and here.

• CommentRowNumber12.
• CommentAuthorDavid_Corfield
• CommentTimeAug 18th 2016

Thanks, Todd. I added something to that effect.

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeAug 18th 2016

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).

• CommentRowNumber14.
• CommentAuthorDavid_Corfield
• CommentTimeAug 18th 2016

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?