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 comma 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 finite 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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).
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 21st 2018

    At natural deduction it says

    natural deduction with computation rules gives a formulation of computation. See computational trinitarianism for discussion of this unification of concepts.

    But I don’t see anything at these links to help explain the role of the C in FIEC (formation-introduction-elimination-computation). Philosophers call the satisfaction of computation rules ’harmony’, and there’s some reflection on why this is desirable, and of course arguments against.

    There should presumably be perspectives on this from the three corners of the trinity of trinitarianism. What can we say from the perspectives of computing and of category theory?

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 21st 2018

    E.g., in the case of category theory, one will want to talk about universal properties. In the case of product, we know this is right adjoint to duplication.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 21st 2018

    I see Mike said some useful things here.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 21st 2018

    Right. From the perspective of computation, the computation rules are what allow you to compute. And from the perspective of category theory, they implement universal properties. A (left) universal property is in general a representation of a functor, i.e. an isomorphism between a functor FF and a representable functor hom(X,)\hom(X,-). The introduction rule is the map hom(X,)F\hom(X,-) \to F (or its Yoneda reduct, an element of F(X)F(X)); the elimination rule is the map Fhom(X,)F \to \hom(X,-); the computation rule says that the composite Fhom(X,)FF \to \hom(X,-) \to F is the identity; and the uniqueness rule says that the composite hom(X,)Fhom(X,)\hom(X,-) \to F \to\hom(X,-) is the identity.

    • CommentRowNumber5.
    • CommentAuthorSam Staton
    • CommentTimeFeb 22nd 2018

    My understanding is that the universal properties give you equations, such as beta/eta equations. But it is another thing to build (compute?) a normal form, which typically requires orienting the equations, such as beta reduction and eta expansion. Perhaps this is what Mike meant by “implement”. I am not sure whether “computation” refers to the equations or to their oriented forms.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 22nd 2018

    Re #5, does this point to the reason for looking to bicategories to represent computation, as in the work John Baez and Mike Stay were doing (and no doubt many others).

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 22nd 2018

    Re #4, thanks, Mike. So could one do some counterfactual ’trinitarian’ history where the computer scientist sees the need for universal properties? And another where the category theorist foresees the need for formation-introduction-elimination-computation?

    I see at representability determines functoriality it claims that the lemma there

    gives an explanation for why the “dogma” of introduction and elimination rules is so effective in practice.

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 22nd 2018
    • (edited Feb 22nd 2018)

    Another thing, the page speaks of “this lemma”, but nowhere is anything titled ’Lemma’. Presumably it’s the final two sentences of section 3.

    [edit: this should have been on the other thread, but has been acted on.]

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 22nd 2018

    Re #7, I guess so.

    Re #5, that’s true, there is a difference there. Maybe the thing to say is that the “computation rules” (including uniqueness rules) can “often” be oriented to determine an operational notion of computation?