Internal Language of Categories with Strong Natural Number Object

Discussion in 'Math Research' started by Rock Brentwood, Oct 13, 2011.

  1. Buried in the theory of Closed Cartesian Categories (CCC) with strong
    natural number objects is an analogue of the differential and integral
    calculus, complete with its own analogue of the "rules for
    differentiation" as well as an analogue of the "Fundamental Theorem of
    Calculus". Some of this structure will be unfolded here.

    1. THE ISSUE
    In Scott and Lambek ("Introduction to Higher Order Categorical Logic",
    Cambridge Studies in Advanced Mathematics, 7, 1986) the comment

    "We would have preferred to state Theorem 11.3 for strong natural
    numbers objects in Lawvere's sense. Unfortunately, we do not yet know
    how to handle the corresponding notion in typed lambda-calculus

    It's the then-unsolved uncovering of this hidden structure that they
    were alluding to.

    First, the context of the remark...

    It is in a discussion of the evolution and history of the Curry-
    Howard(-DeBruijn) correspondence. Lawvere's name came up in the
    remark, since he was mentioned as one of those who (like Gentzen) had
    early on reinstated the standing of the logical connectives as first-
    class citizens, revoking the tendency in the earlier mathematics and
    logic literature to reduce everything to the conditional and negation.
    This eventually tied in with the appearance of CCC's into the mix by
    way of the Rosetta stone:
    true <-> Terminal Object 1
    A and B <-> Product A x B
    if A then B <-> Exponential B^A

    The introduction by Church of the "Church numerals", over time,
    evolved into the notion of the "weak natural number object" N, whose
    defining features were the admission the following:
    * Arrows O: 1 -> N, S: N -> N
    * Existence of iterators g: N -> A for each p: 1 -> A, h: A -> A
    such that g.S = h.g and g.O = p where I'm using ().() to denote

    A strong natural number object has each p and h associated with a
    unique solution g.

    As Scott and Lambek mentioned, Goedel's "functionals of finite type"
    foreshadowed this notion of what eventually came to be called
    "prerecursive categories" (by Marie-France Thibault).

    The "internal language" of such a category, C, is obtained by way of
    the natural functor {C}: C -> Set, given for any small category C with
    terminal object 1 by:
    * {C}: A |-> C(1, A) = morphism class of 1->A arrows in C
    * {C}f: p in C(1, A) |-> f.p in C(1, B) if f: A -> B.

    The authors' Theorem 11.3 is the construction of the equivalent
    representation of the CCC with weak natural number object via its
    internal language. They constructed a typed lambda calculus with a
    product type, "surjective pairing" and an "iterator" and the
    equivalence result.

    (Surjective pairing is the property that any element c of type A x B
    is expressible as c = (Lc, Rc) where L: A x B -> A and R: A x B -> B
    are the projections associated with the product).

    So, that's the context of the above remark and the open problem it
    alludes to.

    A little thought reveals the minimum that is required to resolve the
    problem alluded to by Scott and Lambek.

    First, each h: A -> A and p: 1 -> A must be associated with a unique
    g: N -> A such that
    g.O = p
    g.S = h.g.

    To clarify further discussion, I will use the following notion to
    denote the "elements" of the "type" {C}A, where {C}: C -> Set is the
    natural functor for the category C:
    *p: A where p: 1 -> A
    &a: 1 -> A where a: A
    such that
    &*p = p, and *&a = a.
    Define 0 = *O, and define function application by
    f: A -> B, a: A ==> fa = *(f.&a): B

    Then the conditions on g can be stated equivalently by:
    g0 = a, g(Sn) = h(gn), where n: N.
    These conditions are analogous to those which characterize the
    definite integral. Therefore, denote the solution by:
    g = integral_a h.

    Thus, a CCC with strong natural number object has an "integral"
    operation --
    * if h: A -> A and a: A then integral_a h: N -> A
    * (integral_a h) 0 = a
    * for all n: N, (integral_a h)(Sn) = h(integral_a h (n))

    Let g = integral_a h. To get uniqueness requires that both a and h can
    be extracted from g. Part of this is already given to us:
    a = g0
    The remainder requires that we be able to solve the equation
    g.S = (_).g.
    Let the solution, if it exists, be denoted dg. Not all arrows g: A ->
    A need have such solutions. Therefore, let those arrows which do have
    a solution be called "differentiable".

    Thus, a CC with strong natural number object also has a "differential"
    operation --
    * if g: N -> A is differentiable, then dg: A -> A
    * for all n: N, g(Sn) = dg(gn).
    Thus, from g can be reconstructed a = g0 and h = dg. This leads to the
    following result.

    The Fundamental Theorem:
    if g: N -> A is differentiable, then g = integral_{g0} dg.

    So, in order to arrive at a resolution to Scott and Lambek's problem
    (a) a determination of when an arrow g: N -> A is differentiable
    (b) the formulation for "rules of differentiation" for differentiable

    The non-trivial element here is that a given arrow g: N -> A can be a
    g = k.l, where k: B -> A, l: N -> B,
    and suppose that g = integral_a h.

    If l is differentiable, with dl = m, and if l0 = b, we can write:
    a = g0 = k(l0) = kb
    h(k(ln)) = h(gn) = g(Sn) = k(l(Sn)) = k(m(ln))
    In particular, for n = 0,
    h(kb) = k(mb).

    So now, this shows we need to be able to obtain h = d_m k: A -> A as
    the (unique) solution to k.m = (_).k, where k: B -> A and m: B -> B.
    Thus, the need to "differentiate" has to generlize beyond the
    successor arrow S: N -> N to arbitrary arrows m: B -> B:
    if k: B -> A, m: B -> B and k is m-differentiable, then d_m k: A -> A
    Then, one has the

    if l: N -> B is differentiable with m = dl: B -> B
    if k: B -> A is m-differentiable
    then d(k.l) = d_m k.

    I won't carry out this unfolding all the way (much less prove any
    equivalence result), but this line of arguments takes the matter far
    enough to make it clear that the structure hidden in the internal
    language of the CCC with strong number object is nothing less than a
    categorical analogue of the the differential and integral calculus,
    Rock Brentwood, Oct 13, 2011
    1. Advertisements

Ask a Question

Want to reply to this thread or ask your own question?

You'll need to choose a username for the site, which only take a couple of moments (here). After that, you can post your question and our members will help you out.