{"id":1643,"date":"2012-01-03T09:44:37","date_gmt":"2012-01-03T14:44:37","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/?p=1643"},"modified":"2012-01-03T09:44:37","modified_gmt":"2012-01-03T14:44:37","slug":"categorical-computation-characterized-by-closed-cartesian-categories","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2012\/01\/03\/categorical-computation-characterized-by-closed-cartesian-categories\/","title":{"rendered":"Categorical Computation Characterized By Closed Cartesian Categories"},"content":{"rendered":"

One of my favorite categorical structures is a thing called a closed cartesian category<\/em>, or CCC for short. Since I’m a computer scientist\/software engineer, it’s a natural: CCCs are, basically, the categorical structure of lambda calculus – and thus, effectively, a categorical model of computation. However, before we can talk about the CCCs, we need – what else? – more definitions.<\/p>\n

Cartesian Categories<\/h3>\n

A cartesian category<\/em> C (note not<\/em> cartesian closed<\/em> category) is a category:<\/p>\n

    \n
  1. With a terminal object t, and<\/li>\n
  2. forall a, b in Obj(C), the objects and arrows of the categorical product a times b in C.<\/li>\n<\/ol>\n

    So, a cartesian category is a category closed with respect to product. Many of the common categories are cartesian: the category of sets, and the category of enumerable sets, And of course, the meaning of the categorical product in set? Cartesian product of sets.<\/p>\n

    Categorical Exponentials<\/h3>\n

    To get from cartesian categories to cartesian closed<\/em> categories, we also need to define categorical exponentials<\/em>. Like categorical product, the value of a categorical exponential is not required<\/em> to included in a category. The exponential is a complicated definition, and it’s a bit hard to really get your head around, but it’s well worth the effort. If categorical products are the categorical generalization of set products, then the categorical exponential is the categorical version of a function space. It gives us the ability to talk about structures that are the generalized version of “all functions from A to B”.<\/p>\n

    Given two objects x and y from a category C, their categorical exponential<\/em> xy<\/sup>, if it exists in the category, is defined by a set of values:<\/p>\n

      \n
    • An object x^y,<\/li>\n
    • An arrow mbox{eval}_{y,x}: x^y times y rightarrow x, called an evaluation map<\/em>.<\/li>\n
    • forall z in Obj(C), an operation Lambda_C: (z times y rightarrow x) rightarrow (z rightarrow x^y). (That is, an operation mapping from arrows to arrows.)<\/li>\n<\/ul>\n

      These values must have the following properties:<\/p>\n

        \n
      1. forall f : z times y rightarrow x, g : z rightarrow x^y:\n
          \n
        • mbox{val}_{y,x} circ (Lambda_C(f)times 1_y)<\/li>\n
        • forall f : z times y rightarrow x, g : z rightarrow x^y: Lambda_C(mbox{eval}_{y,x} circ (z times 1_y) = z<\/li>\n<\/ul>\n<\/li>\n<\/ol>\n

          To make that a bit easier to understand, let’s turn it into a diagram.<\/p>\n

          \"exponent.jpg\"<\/p>\n

          As I alluded to earlier, you can also think of it as a generalization of a function space.x^y is the set of all functions from y to x. The evaluation map is simple description in categorical terms of an operation that applies a function from a to b (an arrow) to a value from a, resulting in an a value from b.<\/p>\n

          So what does the categorical exponential mean? I think it’s easiest to explain in terms of sets and functions first, and then just step it back to the more general case of objects and arrows.<\/p>\n

          If X and Y are sets, then X^Y is the set of functions from Y to X.<\/p>\n

          Now, look at the diagram:<\/p>\n

            \n
          1. The top part says, basically, that g is a function from Z to to X^Y: so g takes a member of Z, and uses it to select a function from Y to X.<\/li>\n
          2. The vertical arrow says:\n
              \n
            1. given the pair (z,y), f(z,y) maps (z,y) to a value in X.<\/li>\n
            2. given a pair (z,y), we’re going through a function. It’s almost like currying:\n
                \n
              1. The vertical arrow going down is basically taking g(z,y), and currying it to g(z)(y).<\/li>\n
              2. Per the top part of the diagram, g(z) selects a function from y to x. (That is, a member of X^Y.)<\/li>\n
              3. So, at the end of the vertical arrow, we have a pair (g(z), y).<\/li>\n<\/ol>\n<\/li>\n
              4. The “eval” arrow maps from the pair of a function and a value to the result of applying the function to the value.<\/li>\n<\/ol>\n

                Cartesian Closed Categories<\/h3>\n

                Now – the abstraction step is actually kind of easy: all we’re doing is saying that there is a structure<\/em> of mappings from object to object here. This particular structure has the essential properties of what it means to apply a function to a value. The internal values and precise meanings of the arrows connecting the values can end up being different things, but no matter what, it will come down to something very much like function application.<\/p>\n

                With exponentials and products, we can finally say what the cartesian closed categories (CCCs). A Cartesian closed category<\/em> is a category that is closed with respect to both products and exponentials.<\/p>\n

                Why do we care? Well, the CCCs are in a pretty deep sense equivalent to the simply typed lambda calculus. That means that the CCCs are deeply tied to the fundamental nature of computation. The structure<\/em> of the CCCs – with its closure WRT product and exponential – is an expression of the basic capability of an effective computing system. So next, we’ll take a look at a couple of examples of what we can do with the CCCs as a categorical model of computation.<\/p>\n","protected":false},"excerpt":{"rendered":"

                One of my favorite categorical structures is a thing called a closed cartesian category, or CCC for short. Since I’m a computer scientist\/software engineer, it’s a natural: CCCs are, basically, the categorical structure of lambda calculus – and thus, effectively, a categorical model of computation. However, before we can talk about the CCCs, we need […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[76,32],"tags":[122,132],"class_list":["post-1643","post","type-post","status-publish","format-standard","hentry","category-category-theory","category-lambda-calculus","tag-category-theory-2","tag-computation-2"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-qv","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1643","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=1643"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1643\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=1643"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=1643"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=1643"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}