Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: affine logic

Bottom of Page

1 to 16 of 16

  1.  
    • 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 15th 2016

    there is a notion of categorical model of affine logic where we only require a natural family of maps A→IA\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 II is terminal, or — slightly more generally — by (symmetric) monoidal categories equipped with a family A→IA\to I of arrows (for all objects AA), which is natural in AA.

    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 II is forced to be terminal as soon as we require I→II\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 II 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⊢BA\vdash B by CC and then cut with ⋅⊢C\cdot\vdash C:

    ⋮ ⋅⊢CA⊢B A,C⊢B A⊢B \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⊢BA\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→IA\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→IA\to I and A→A⊗AA\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 17th 2016

    I think compatibility of weakening with cuts on sequents with unary domain is naturality. That is, this:

    ⋮ D⊢CA⊢B A,C⊢B A,D⊢B \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 DD, and that’s naturality. But if DD is replaced by an empty context or a context of length >1\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 kk (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?

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2023

    Touched wording, hyperlinking and formatting.

    And added references.

    diff, v10, current

  16. Added link to antithesis interpretation

    Anonymouse

    diff, v11, current

1 to 16 of 16

  1.