Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.



Internal Language of Categories with Strong Natural Number Object
Posted:
Oct 13, 2011 8:07 AM


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 appears:
"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 lambdacalculus equationally."
It's the thenunsolved uncovering of this hidden structure that they were alluding to.
2. THE BACKGROUND 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 composition.
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 MarieFrance 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.
3. THE INTEGRAL OPERATOR 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))
4. DIFFERENTIABILITY AND THE DIFFERENTIAL OPERATOR 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 requires (a) a determination of when an arrow g: N > A is differentiable (b) the formulation for "rules of differentiation" for differentiable arrows
5. RULES OF DIFFERENTIATION The nontrivial element here is that a given arrow g: N > A can be a composition 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 mdifferentiable, then d_m k: A > A Then, one has the
CHAIN RULE: if l: N > B is differentiable with m = dl: B > B if k: B > A is mdifferentiable 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, itself.



